A probabilistic dynamic logic

Publisher Website
Google Scholar
Abstract
A logic, Pr(DL), is presented, which enables reasoning about probabilistic programs or, alternatively, reasoning probabilistically about conventional programs. The syntax of Pr(DL) derives from Pratt's first-order dynamic logic and the semantics extends Kozen's semantics of probabilistic programs. An axiom system for Pr(DL) is presented 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. Examples are presented, both of the expressive power of Pr(DL), and of a proof in the axiom system.

This publication has 0 references indexed in Scilit: