A probabilistic dynamic logic. (English) Zbl 0537.68036

This paper defines a formal logic PrDL whose syntax derives from Pratt’s first-order dynamic logic and whose semantics is an extension of Kozen’s for probabilistic programs. An axiom system for PrDL is given and shown to be complete relative to an extension of first-order analysis. For discrete probabilities it is shown that first-order analysis actually suffices. Some precursors of this paper are J. H. Reif’s propositional version [12th ACM Symp. Theory of Computing, 8-13 (1980)] and L. Ramshaw’s semiformal system based on the Floyd-Hoare inductive assertion method [Ph. D. thesis (1981), Stanford University].
Reviewer: H.Nishimura


68Q65 Abstract data types; algebraic specification
03B48 Probability and inductive logic
68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: DOI


[1] Cook, S.A., Soundness and completeness of an axiom system for program verification, SIAM J. comput., 7, 1, (1978) · Zbl 0374.68009
[2] Feldman, Y.A., A decidable propositional probabilistic dynamic logic, ()
[3] Fischer, M.J.; Ladner, R.E., Propositional dynamic logic of regular programs, J. comput. system sci., 18, 2, (April 1979)
[4] Gaifman, H., Concerning measures in first order calculi, Israel J. math., (March 1964)
[5] Halmos, P.R., Measure theory, (1950), Van Nostrand-Reinhold Princeton, N. J · Zbl 0117.10502
[6] Harel, D., ()
[7] Hoover, D.N., Probability logic, Ann. of math. logic, 14, (1978) · Zbl 0776.60048
[8] Hart, S.; Sharir, M.; Pnueli, A., Termination of probabilistic concurrent programs, () · Zbl 0511.68009
[9] Kozen, D.; Kozen, D., Semantics of probabilistic programs, (), J. comput. system sci., 22, 328-350, (1981), Also appeared · Zbl 0476.68019
[10] Kozen, D., A probabilistic PDL, () · Zbl 0575.03013
[11] Lehman, D.; Rabin, M.O., On the advantages of free choice: A symmetric and fully distributed solution to the dining philosophers problem, (), 133-138
[12] Martin, D.A., Descriptive set theory, ()
[13] Moschovakis, Y.N., Descriptive set theory, (1980), North-Holland Amsterdam · Zbl 0433.03025
[14] Pnueli, A., The temporal logic of programs, () · Zbl 0607.68022
[15] Pratt, V.R., Semantical considerations on floyd-Hoare logic, ()
[16] Rabn, M.O., Probabilistic algorithms, ()
[17] Rabin, M.O., Probabilistic algorithms in finite fields, Technical report MIT/LCS/TR-213, (1979)
[18] Ramshaw, L.H., Formalizing the analysis of algorithms, (), Also technical report, XEROX PARC
[19] Reif, J.H., Logics for probabilistic programming, () · Zbl 0772.94019
[20] Rogers, H., Theory of recursive functions and effective computability, (1967), McGraw-Hill New York · Zbl 0183.01401
[21] Shoenfield, J.R., Mathematical logic, (1967), Addison-Wesley Reading, Mass · Zbl 0155.01102
[22] Scott, D.; Krauss, P., Assigning probabilities to logical formulas, () · Zbl 0202.29905
[23] Sharir, M.; Pnueli, A.; Hart, S., The probabilistic verification of programs. I. correctness analysis of sequential programs, (December 1981), manuscript
[24] Tiomkin, M.L., Propositional probabilistic dynamic logic; vague functions and probabilistic and fair looping, (September 1981), manuscript
[25] Yao, A., Probabilistic computations: toward a unified measure of complexity, ()
[26] Zadeh, L.A., Fuzzy logic and its applications to approximate reasoning, () · Zbl 0361.68126
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.