Abstract J.I. den Hartog, E.P. de Vink and J.W. de Bakker
Metric semantics and full abstraction
for action refinement and probabilistic choice

This paper provides a case-study in the field of metric semantics
for probabilistic programming. Both an operational and a
denotational semantics are presented for an abstract process
language Lpr, which features action refinement and probabilistic
choice. The two models are constructed in the setting of complete
ultrametric spaces, here based on probability measures of compact
support over sequences of actions. It is shown that the standard
toolkit for metric semantics works well in the probabilistic
context of Lpr, e.g.\ in establishing the correctness of the
denotational semantics with respect to the operational one. In
addition, it is shown how the method of proving full abstraction
---as proposed recently by the authors for a nondeterministic language
with action refinement--- can be adapted to deal with the
probabilistic language Lpr as well.