A probabilistic PDL (Q1063584)

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.