Logics for probabilistic programming (Extended Abstract)
John H. Reif · 1980
This paper introduces a logic for probabilistic programming+ PROB-DL (for probabilistic dynamic logic; see Section 2 for a formal definition). This logic has “dynamic” modal operators in which programs appear, as in Pratt's [1976] dynamic logic DL. However the programs of PROB-DL contain constructs for probabilistic branching and looping whereas DL is restricted to nondeterministic programs. The formula {a}σp of PROB-DL denotes “with measure ≥σ, formula p holds after executing program a.”