Loading...
A UTP semantics of pGCL as a homogeneous relation
Date
2012
Abstract
We present an encoding of the semantics of the probabilis- tic 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 predi- cates 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. As an example we study the Monty Hall game in this framework.
Supervisor
Description
peer-reviewed
Publisher
Springer
Citation
Integrated Formal Methods 2012. Lecture Notes in Computer Science;7321, pp. 191-205
Files
ULRR Identifiers
Funding code
Funding Information
Science Foundation Ireland (SFI)