Towards a UTP-style framework to deal with probabilities - BUTTERFIELD, ANDREW; BRESCIANI, RICCARDO (TCD-CS Technical Reports, 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 programs 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 formulation allows us to de?ne a generic choice construct, that covers conditional, probabilistic and non-deterministic choice. We introduce the concept of probabilistic re?nement 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.
PUBLISHED
Dublin, Ireland
Keywords: Computer Science