# zbMATH — the first resource for mathematics

A probabilistic PDL. (English) Zbl 0575.03013
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.
Reviewer: A.Stolboushkin

##### MSC:
 03B48 Probability and inductive logic 68Q65 Abstract data types; algebraic specification 60G07 General theory of stochastic processes 60G50 Sums of independent random variables; random walks 03C13 Model theory of finite structures 68W99 Algorithms in computer science 68Q60 Specification and verification (program logics, model checking, etc.) 03B45 Modal logic (including the logic of norms)
Full Text:
##### References:
  Feldman, Y.A., A decidable propositional probabilistic dynamic logic, (), 298-309  Feldman, Y.A.; Harel, D., A probabilistic dynamic logic, (), 181  Fischer, M.J.; Ladner, R.E., Propositional dynamic logic of regular programs, J. comput. system sci., 18, No.2, (1979) · Zbl 0408.03014  Halmos, P.R., Measure theory, (1950), Van Nostrand Princeton, N.J · Zbl 0117.10502  Halpern, J.; Reif, J., Propositional dynamic logic of deterministic, well-structured programs, (), 322  Kozen, D., Semantics of probabilistic programs, J. comput. system. sci., 22, 328, (1981) · Zbl 0476.68019  Lehmann, D.; Shelah, S., Reasoning with time and chance, (Oct. 1982), manuscript  Liu, C.L., Introduction to combinatorial mathematics, (1968), McGraw-Hill New York · Zbl 0188.03801  {\scJ. A. Makowsky and M. L. Tiomkin}, Probabilistic propositional dynamic logic, manuscript. · Zbl 0732.03022  {\scR. Parikh and A. Mahoney}, A theory of probabilistic programs, manuscript. · Zbl 0558.68010  Pnueli, A., On the extremely fair treatment of probabilistic algrithms, (Nov. 1982), manuscript  Ramshaw, L., Formalizing the analysis of algorithms, ()  Reif, J., Logics for probabilistic programming, ()  Revuz, D., Markov chains, (1975), North-Holland Amsterdam · Zbl 0332.60045  Schaefer, H.H., Topological vector spaces, () · Zbl 0217.16002  Sharir, M.; Pnueli, A.; Hart, S., Probabilistic verification of programs. I. correctness analysis of sequential programs, (Dec. 1981), manuscript
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.