A Fully Abstract Metric-Space Denotational Semantics for Reactive Probabilistic Processes

Abstract Metric-Space Denotational Semantics for Reactive Probabilistic Processes M.Z. Kwiatkowska and G.J. Norman School of Computer Science, University of Birmingham, Edgbaston, Birmingham B15 2TT, UK We consider the calculus of Communicating Sequential Processes (CSP) [8] extended with action-guarded probabilistic choice and provide it with an operational semantics in terms of a suitable extension of Larsen and Skou’s [14] 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 [3] introduced for classical process calculi, we derive a metric-space semantic model for the calculus and show ly abstract.

• Type: Journal
• Year: 1998
• Where: ENTCS
• Authors: Marta Z. Kwiatkowska, Gethin Norman
• Keywords: Action-guarded Probabilistic Choice, ENTCS 1998, Metric-Space Denotational Semantics, Probabilistic