Decidability of finite probabilistic propositional dynamic logics (Q809069)

In finite Probabilistic Propositional Dynamic Logic (PPDL) language, the basic dynamic construct is \(<\alpha >\lambda \phi\), interpreted as follows: the probability that the program \(\alpha\) will terminate in a state satisfying the formula \(\phi\) is \(\lambda\). The present paper considers three basic versions of PPDL: (1) Deterministic PPDL (DPPDL), where programs \(\alpha\) are only deterministic regular expressions, Boolean combinations of propositional variables \(\phi\) are allowed, and for estimating \(\lambda\), first-order formulas of real closed fields can be used; (2) Rational PPDL \((PPDL>r)\), where \(\lambda\) is greater than a rational constant r; (3) Positive PPDL \((PPDL>0)\), like \(PPDL>r\), for \(r=0\). Clearly, probabilistic estimations of (3) are a special case of (2), and those of (2) are a special case of (1). The present paper considers some natural variation and extension properties for them. Section 2 gives the basic formal definitions and the results concerning the (un)decidability of different PPDLs. In Section 3 there is proved that \(PPDL>0\) is reducible to standard Propositional Dynamic Logic (PDL), reminding a similar result for the extension \(PDL+GA\) (programs with global assignments). Section 4 proves that all PPDLs without nesting of probability estimations have the finite model property. The proof idea is to use the fact that a regular program is a limit of finite programs. Section 5 considers some DPPDL extensions and decidability results for them. In Section 6 undecidability results for \(PPDL>r\) are analysed, while the Appendix contains the undecidability proof for D. Kozen's PPDL that allows Boolean combinations of inequalities.