A Fully Abstract Metric-Space Denotational Semantics for Reactive Probabilistic Processes
Marta Kwiatkowska, Gethin Norman · Electronic Notes in Theoretical Computer Science · 1998
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.