A Probabilistic Theory of Designs Based on Distributions
We present a theory of designs based on functions from the state space to real numbers, which we term distributions. This theory uses predicates, in the style of UTP, based on homogeneous relations between distributions, and is richer than the standard UTP theory of designs as it allows us to reason about probabilistic programs; the healthiness conditions H1–H4 of the standard theory are implicitly accounted for in the distributional theory we present. In addition we propose a Galois connection linkage between our distribution-based model of probabilistic designs, and the standard UTP model of (non-probabilistic) designs.
KeywordsHealthiness Condition Probabilistic Choice Probabilistic Program Homogeneous Relation Nondeterministic Choice
Unable to display preview. Download preview PDF.
- [BB11]Bresciani, R., Butterfield, A.: Towards a UTP-style framework to deal with probabilities. Technical Report TCD-CS-2011-09, FMG, Trinity College Dublin, Ireland (August 2011)Google Scholar
- [He10]He, J.: A probabilistic bpel-like language. In: Qin [Qin10], pp. 74–100Google Scholar
- [HJ98]Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice Hall International Series in Computer Science (1998)Google Scholar
- [Hoa85]Hoare, C.A.R.: Programs are predicates. In: Proceedings of a Discussion Meeting of the Royal Society of London on Mathematical Logic and Programming Languages, pp. 141–155. Prentice-Hall, Upper Saddle River (1985)Google Scholar
- [HS06]He, J., Sanders, J.W.: Unifying probability. In: Dunne and Stoddart [ds06], pp. 173–199Google Scholar
- [MM04]McIver, A., Morgan, C.: Abstraction, Refinement and Proof For Probabilistic Systems. Monographs in Computer Science. Springer (2004)Google Scholar