×

Decidability of finite probabilistic propositional dynamic logics. (English) Zbl 0732.03022

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.
Reviewer: N.Curteanu (Iaşi)

MSC:

03B70 Logic in computer science
03B25 Decidability of theories and sets of sentences
03B45 Modal logic (including the logic of norms)
03B48 Probability and inductive logic
68Q55 Semantics in the theory of computing
Full Text: DOI

References:

[1] Feldman, Y. A., A decidable propositional probabilistic logic with explicit probabilities, Inform. Comput., 63, 11 (1984) · Zbl 0592.68031
[2] Feldman, Y. A., Probabilistic Programming Logics, (Ph.D. Thesis (1984), The Weizmann Institute of Science: The Weizmann Institute of Science Rehovot, Israel)
[3] Feldman, Y. A.; Harel, D., A probabilistic dynamic logic, J. Comput. System Sci., 28, 193 (1984) · Zbl 0537.68036
[4] Fisher, M. J.; Ladner, R. E., Propositional dynamic logic of regular programs, J. Comput. System Sci., 18, 194 (1979) · Zbl 0408.03014
[5] Gabbay, D.; Gabbay, D.
[6] Harel, D., First Order Dynamic Logic, (Lecture Notes in Computer Science, Vol. 68 (1979), Springer-Verlag: Springer-Verlag Berlin/New York) · Zbl 0403.03024
[7] Harel, D.; Pnueli, A.; Stavi, J., Propositional dynamic logic of context-free programs, (IEEE 22nd Annual Symposium of Foundations of Computer Science (1983)), 310-321
[8] Kemeny, J. G.; Snell, J. L., (Finite Markov Chains (1960), van Nostrand: van Nostrand Princeton, NJ) · Zbl 0089.13704
[9] Kozen, D., Semantics of probabilistic programs, J. Comput. System Sci., 22, 328 (1981) · Zbl 0476.68019
[10] Kozen, D., A probabilistic PDL, J. Comput. System Sci., 30, 162 (1985) · Zbl 0575.03013
[11] Meyer, A. R.; Winklmann, K., Expressing program looping in regular dynamic logic, Theoret. Comput. Sci., 18, 301 (1982) · Zbl 0478.68031
[12] Neveu, J., Probability Theory (1964) · Zbl 0119.33805
[13] Paz, A., (Introduction to Probabilistic Automata (1971), Academic Press: Academic Press New York) · Zbl 0234.94055
[14] Parikh, R.; Mahoney, A., A theory of probabilistic programs, (Clarke, E.; Kozen, D., Logic of Programs, Proceedings 1983. Logic of Programs, Proceedings 1983, Lecture Notes in Computer Science, Vol. 164 (1984), Springer-Verlag: Springer-Verlag Berlin/New York), 398-402 · Zbl 0558.68010
[15] Pratt, V. R., A practical decision method for propositional dynamic logic: Preliminary report, (Proceedings of 10th STOC (1978)), 326-337 · Zbl 1283.03066
[16] Sharir, M.; Pnueli, A.; Hart, S., Verification of probabilistic programs, SIAM J. Comput., 13, 292 (1984) · Zbl 0533.68012
[17] Tiomkin, M., Extensions of Propositional Dynamic Logic, (Ph.D. Thesis (1983), Technion-Israel Institute of Technology: Technion-Israel Institute of Technology Haifa, Israel) · Zbl 0732.03022
[18] Tiomkin, M.; Makowsky, J. A., (Probabilistic Propositional Dynamic Logic (1983), Department of Computer Science: Department of Computer Science Technion, Haifa), Technical Report # 305
[19] Tiomkin, M.; Makowsky, J. A., Propositional dynamic logic with local assignments, Theoret. Comput. Sci., 36, 71 (1985) · Zbl 0574.03011
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.