Towards a UTP-style framework to deal with probabilities
Citation:
Riccardo Bresciani, Andrew Butterfield, Towards a UTP-style framework to deal with probabilities, Dublin, Ireland, TCD-CS Technical Reports, August, 2011Download Item:
Abstract:
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.
Sponsor
Grant Number
Science Foundation Ireland (SFI)
03/CE2/1303
Science Foundation Ireland (SFI)
08/RFP/CMS1277
Author's Homepage:
http://people.tcd.ie/butrfeldDescription:
PUBLISHEDDublin, Ireland
Author: BUTTERFIELD, ANDREW; BRESCIANI, RICCARDO
Publisher:
TCD-CS Technical ReportsType of material:
ReportCollections
Availability:
Full text availableKeywords:
Computer ScienceMetadata
Show full item recordLicences: