[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]
|
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.
|