Towards a UTP-style framework to deal with probabilities
Riccardo Bresciani, Andrew Butterfield Å · 2011
We present an encoding of the semantics of the probabilistic guarded command language (pGCL) in the Unifying Theories of Programming (UTP) framework. Our contribution is a UTP encoding that captures pGCL pro- grams as predicate-transformers, on predicates over probability distributions on before- and after-states: these predicates capture the same information as the models traditionally used to give semantics to pGCL; in addition our formu- lation allows us to define a generic choice construct, that covers conditional, probabilistic and non-deterministic choice. We introduce the concept of prob- abilistic refinement in this framework. This technical report gives a rigourous presentation of our framework, along with a variety of proofs and examples (including the well-known Monty Hall problem), that help to explain it.