Logics for probabilistic programming (Extended Abstract)

Publisher Website
Google Scholar
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}&sgr;p of PROB-DL denotes “with measure ≥&sgr;, formula p holds after executing program a.” In Section 3, we show that PROB-DL has a complete and consistent axiomatization, (using techniques derived from Parikh's [1978] completeness proof for the propositional dynamic logic). Section 4 presents a probabilistic quantified boolean logic (PROB-QBF) which also has applications to probabilistic programming.

This publication has 0 references indexed in Scilit: