Domain equations for probabilistic processes

Christel BaierChristel Baier, Marta Z. KwiatkowskaMarta Z. Kwiatkowska

Christel Baier, Marta Z. Kwiatkowska
Domain equations for probabilistic processes
Mathematical Structures in Computer Science, 10(6):665--717, 2000

Details
Bibtex

KurzfassungAbstract
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.
Weitere Informationen unter:Further Information: Link
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

@article{BK2000,
  author  = {Christel Baier and Marta Z. Kwiatkowska},
  title   = {Domain equations for probabilistic processes},
  journal = {Mathematical Structures in Computer Science},
  volume  = {10},
  number  = {6},
  year    = {2000},
  pages   = {665--717}
}