In this paper we consider Milner's calculus CCS enriched by a probabilistic choice operator.
The calculus is given operational semantics based on probabilistic transition systems. We
define operational notions of preorder and equivalence as probabilistic extensions of the
simulation preorder and the bisimulation equivalence respectively. We extend existing
category-theoretic techniques for solving domain equations to the probabilistic case and give
two denotational semantics for the calculus. The first, ‘smooth’, semantic model arises as a
solution of a domain equation involving the probabilistic powerdomain and solved in the
category CONT⊥ of continuous domains. The second model also involves an appropriately
restricted probabilistic powerdomain, but is constructed in the category CUM of complete
ultra-metric spaces, and hence is necessarily ‘discrete’. We show that the domain-theoretic
semantics is fully abstract with respect to the simulation preorder, and that the metric
semantics is fully abstract with respect to bisimulation.
Metric semantics for concurrency
