## Axioms for probability and nondeterminism

*Michael Mislove*,
*Joël
Ouaknine*, and *James Worrell*
This paper studies a simple calculus for finite-state processes
featuring both nondeterministic and probabilistic choice. We present
a domain model and an operational semantics for our calculus. The
denotational model uses the probabilistic powerdomain of Jones and
Plotkin, combined with a geometrically convex variant of the Plotkin
powerdomain. The operational model defines transition rules under
which a process makes transitions to probability distributions over
states. We prove a full abstraction result that shows two processes
have the same denotation if and only if they are probabilistically
bisimilar. We also show that the expected laws for probability and
nondeterminism are sound and complete with respect to the denotational
model.

*Proceedings of EXPRESS 03*, ENTCS 96, 2004. 22 pages.

PDF
© 2004 Elsevier Science B.V.

Imprint / Data Protection