A probabilistic PDL

ABSTRACT

In this paper we give a probabilistic analog PPDL of Propositional Dynamic Logic. We prove a small model property and give a polynomial space decision procedure for formulas involving well-structured programs. We also give a deductive calculus and illustrate its use by calculating the expected running time of a simple random walk program.

REFERENCES

• 1: Feldman, Y.A., "A Decidable Propositional Probabilistic Dynamic Logic," this proceedings.
• 2: Yishai A. Feldman , David Harel, A probabilistic dynamic logic, Proceedings of the fourteenth annual ACM symposium on Theory of computing, p.181-195, May 05-07, 1982, San Francisco, California, United States [doi>10.1145/800070.802191]
• 3: Fischer, M.J. and R.E.Ladner, "Propositional Dynamic Logic of Regular Programs," J. Comput. Syst. Sci. 18:2 (1979).
• 4: Halpern and Reif, "Propositional Dynamic Logic of Deterministic, Well-structured Programs," 22nd Symp. on Foundations of Computer Science, 1981, p. 322.
• 5: Kozen, D., "Semantics of Probabilistic Programs," JCSS 22 (1981), p. 328.
• 6: Lehmann, D., and S. Shelah, "Reasoning with Time and Chance," manuscript, Oct. 1982.
• 7: Makowsky, J.A. and M.L. Tiomkin, "Probabilistic Propositional Dynamic Logic," manuscript.
• 8: Parikh, R. and A. Mahoney, "A Theory of Probabilistic Programs," manuscript.
• 9: Pnueli, A., "On the Extremely Fair Treatment of Probabilistic Algorithms," manuscript, Nov. 1982.
• 10: Lyle Harold Ramshaw, Formalizing the analysis of algorithms., 1979
• 11: John H. Reif, Logics for probabilistic programming (Extended Abstract), Proceedings of the twelfth annual ACM symposium on Theory of computing, p.8-13, April 28-30, 1980, Los Angeles, California, United States [doi>10.1145/800141.804647]
• 12: Revuz, D., Markov chains, North-Holland, 1975.
• 13: Schaefer, H.H., Topological Vector Spaces, Springer-Verlag Graduate Texts in Mathematics 3, 1971.
• 14: Sharir, Pnueli, and Hart, "Probabilistic Verification of Programs: I. Correctness Analysis of Sequential Programs," manuscript, Dec. 1981.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Logics of programs

General Terms:
Theory