A probabilistic PDL
type: Item
instance of: scholarly article
title: A probabilistic PDL
zbMATH Open document ID: 0575.03013
DOI: 10.1016/0022-0000(85)90012-1
author: Dexter Kozen
published in: Journal of Computer and System Sciences
publication date: 1985-01-01T00:00:00Z
review text: The paper gives a probabilistic analog of propositional dynamic logic (PDL), so called PPDL, in order to analyze the properties of probabilistic programs (in the same sense in which PDL intends for the analysis of standard ones). The main result is a ''small model property'' of PPDL stating roughly that if a PPDL formula F has a model, it has small finite ones. Then a polynomial-space algorithm is proposed deciding upon validity of formulas involving ''well-structured'' probabilistic programs. The last part illustrates the usage of some proposed deductive calculus (for PPDL) in an example of simple random walk.
Mathematics Subject Classification ID: 03B48
Mathematics Subject Classification ID: 68Q65
Mathematics Subject Classification ID: 60G07
Mathematics Subject Classification ID: 60G50
Mathematics Subject Classification ID: 03C13
Mathematics Subject Classification ID: 68W99
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 03B45
zbMATH DE Number: 3918337
zbMATH Keywords: analysis of probabilistic algorithms
zbMATH Keywords: probabilistic analog of propositional dynamic logic
zbMATH Keywords: probabilistic programs
zbMATH Keywords: small model property
zbMATH Keywords: deductive calculus
MaRDI profile type: Publication
full work available at URL: 0022-0000(85)90012-1
OpenAlex ID: W2000108089
cites work: Propositional dynamic logic of regular programs
cites work: Q5726943
cites work: Semantics of probabilistic programs
cites work: Reasoning with time and chance
cites work: Q5581642
cites work: Decidability of finite probabilistic propositional dynamic logics
cites work: Q3347262
cites work: Q4098445
cites work: Q5620935
description: scientific article; zbMATH DE number 3918337