Oxford logo
[KN98a] M. Kwiatkowska and G. Norman. A Fully Abstract Metric-Space Denotational Semantics for Reactive Probabilistic Processes. In Proc. 3rd Workshop on Computation and Approximation (Comprox III), volume 13 of Electronic Notes in Theoretical Computer Science, Elsevier Science. September 1998. [ps.gz] [pdf] [bib]
Downloads:  ps.gz ps.gz (158 KB)  pdf pdf (380 KB)  bib bib
Notes: ENTCS is available at www.sciencedirect.com/science/journal/15710661.
Abstract. We consider the calculus of Communicating Sequential Processes (CSP) extended with action-guarded probabilistic choice and provide it with an operational semantics in terms of a suitable extension of Larsen and Skou's reactive probabilistic transition systems. We show that a testing equivalence which identifies two processes if they pass all tests with the same probability is a congruence for a subcalculus of CSP including external and internal choice and the synchronous parallel. Using the methodology of de Bakker and Zucker introduced for classical process calculi, we derive a metric-space semantic model for the calculus and show it is fully abstract.