A probabilistic dynamic logic

摘要

A logic, PrDL, is presented, which enables formal reasoning about probabilistic programs or, alternatively, reasoning probabilistically about conventional programs. The syntax of PrDL derives from Pratt's first-order dynamic logic and the semantics extends Kozen's semantics of probabilistic programs. An axiom system for PrDL 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 PrDL, and of a proof in the axiom system.