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