×

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)
PDF BibTeX Cite
Full Text: DOI
References:
[1] Feldman, Y.A., A decidable propositional probabilistic dynamic logic, (), 298-309
[2] Feldman, Y.A.; Harel, D., A probabilistic dynamic logic, (), 181
[3] Fischer, M.J.; Ladner, R.E., Propositional dynamic logic of regular programs, J. comput. system sci., 18, No.2, (1979) · Zbl 0408.03014
[4] Halmos, P.R., Measure theory, (1950), Van Nostrand Princeton, N.J · Zbl 0117.10502
[5] Halpern, J.; Reif, J., Propositional dynamic logic of deterministic, well-structured programs, (), 322
[6] Kozen, D., Semantics of probabilistic programs, J. comput. system. sci., 22, 328, (1981) · Zbl 0476.68019
[7] Lehmann, D.; Shelah, S., Reasoning with time and chance, (Oct. 1982), manuscript
[8] Liu, C.L., Introduction to combinatorial mathematics, (1968), McGraw-Hill New York · Zbl 0188.03801
[9] {\scJ. A. Makowsky and M. L. Tiomkin}, Probabilistic propositional dynamic logic, manuscript. · Zbl 0732.03022
[10] {\scR. Parikh and A. Mahoney}, A theory of probabilistic programs, manuscript. · Zbl 0558.68010
[11] Pnueli, A., On the extremely fair treatment of probabilistic algrithms, (Nov. 1982), manuscript
[12] Ramshaw, L., Formalizing the analysis of algorithms, ()
[13] Reif, J., Logics for probabilistic programming, ()
[14] Revuz, D., Markov chains, (1975), North-Holland Amsterdam · Zbl 0332.60045
[15] Schaefer, H.H., Topological vector spaces, () · Zbl 0217.16002
[16] 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.