Oxford logo
[KN96a] M. Kwiatkowska and G. Norman. Probabilistic Metric Semantics for a Simple Language with Recursion. In W. Penczek and A. Szalas (editors), Proc. 21st International Symposium on Mathematical Foundations of Computer Science (MFCS'96), volume 1113 of Lecture Notes in Computer Science, pages 419-430, Springer. September 1996. [ps.gz] [pdf] [bib]
Downloads:  ps.gz ps.gz (80 KB)  pdf pdf (219 KB)  bib bib
Notes: The original publication is available at link.springer.com.
Abstract. We consider a simple divergence-free language RP for reactive processes which includes prefixing, deterministic choice, action-guarded probabilistic choice, synchronous parallel and recursion. We show that the probabilistic bisimulation of Larsen and Skou is a congruence for this language. Following the methodology introduced by de Bakker and Zucker we give denotational semantics to this language by means of a complete metric space of (deterministic) probabilistic trees defined in terms of the powerdomain of closed sets. This new metric, although not an ultra-metric, nevertheless specialises to the metric of de Bakker and Zucker. Our semantic domain admits a full abstraction result with respect to probabilistic bisimulation.