Logics for Probabilistic Programming (Extended Abstract)

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.”

Authors

• John H. Reif

Keywords

No keywords are indexed for this paper.