Logics for probabilistic programming

Journal Article

© 1980 ACM. 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."

Full Text

Duke Authors

Cited Authors

  • Reif, JH

Published Date

  • January 1, 1980

Published In

Volume / Issue

  • 1980-April /

Start / End Page

  • 8 - 13

International Standard Serial Number (ISSN)

  • 0737-8017

Digital Object Identifier (DOI)

  • 10.1145/800141.804647

Citation Source

  • Scopus