Hostname: page-component-8448b6f56d-xtgtn Total loading time: 0 Render date: 2024-04-19T22:54:15.792Z Has data issue: false hasContentIssue false

Domain equations for probabilistic processes

Published online by Cambridge University Press:  04 April 2001

CHRISTEL BAIER
Affiliation:
Fakultät für Mathematik & Informatik, Universität Mannheim, 68131 Mannheim, Germany. Email: baier@pi2.informatik.uni-mannheim.de Current address: Department of Computer Science I, University of Bonn, Römerstr. 164, 53117 Bonn, Germany.
MARTA KWIATKOWSKA
Affiliation:
School of Computer Science, University of Birmingham, Edgbaston, Birmingham B15 2TT, UK. Email: M.Z.Kwiatkowska@cs.bham.ac.uk

Abstract

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.

Type
Research Article
Copyright
2000 Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)