A probabilistic dynamic logic (Q792757)

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 \textit{J. H. Reif's} propositional version [12th ACM Symp. Theory of Computing, 8-13 (1980)] and \textit{L. Ramshaw's} semiformal system based on the Floyd-Hoare inductive assertion method [Ph. D. thesis (1981), Stanford University].