Reasoning about probabilistic sequential programs in a probabilistic logic

Publication Type:
Journal Article
Acta Informatica, 2003, 39 (5), pp. 315 - 389
Issue Date:
Filename Description Size
Thumbnail2008004833OK.pdf455.72 kB
Adobe PDF
Full metadata record
We introduce a notion of strong monotonicity of probabilistic predicate transformers. This notion enables us to establish a normal form theorem for monotone probabilistic predicate transformers. Three other healthiness conditions, namely, conjunctivity, disjunctivity and continuity for probabilistic predicate transformers are also examined, and they are linked to strong monotonicity. A notion of probabilistic refinement index is proposed, and it provides us with a continuous strength spectrum of refinement relations which may be used to describe more flexible refinement between probabilistic programs. A notion of probabilistic correctness is introduced too. We give a probabilistic weakest-precondition, choice and game semantics to the contract language, and present a probabilistic generalization of the winning strategy theorem.
Please use this identifier to cite or link to this item: