A Probabilistic Theory of Designs Based on Distributions

  • Riccardo Bresciani
  • Andrew Butterfield
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7681)


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.


Healthiness Condition Probabilistic Choice Probabilistic Program Homogeneous Relation Nondeterministic Choice 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [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
  2. [BB12]
    Bresciani, R., Butterfield, A.: A UTP Semantics of pGCL as a Homogeneous Relation. In: Derrick, J., Gnesi, S., Latella, D., Treharne, H. (eds.) IFM 2012. LNCS, vol. 7321, pp. 191–205. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  3. [But10]
    Butterfield, A. (ed.): UTP 2008. LNCS, vol. 5713. Springer, Heidelberg (2010)zbMATHGoogle Scholar
  4. [CS09]
    Chen, Y., Sanders, J.W.: Unifying Probability with Nondeterminism. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 467–482. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  5. [DS06]
    Dunne, S., Stoddart, B. (eds.): UTP 2006. LNCS, vol. 4010. Springer, Heidelberg (2006)zbMATHGoogle Scholar
  6. [Hal50]
    Halmos, P.R.: Measure Theory. University Series in Higher Mathematics. D. Van Nostrand Company, Inc., Princeton (1950)zbMATHGoogle Scholar
  7. [He10]
    He, J.: A probabilistic bpel-like language. In: Qin [Qin10], pp. 74–100Google Scholar
  8. [Heh84]
    Hehner, E.C.R.: Predicative programming part i,&,ii. Commun. ACM 27(2), 134–151 (1984)MathSciNetzbMATHCrossRefGoogle Scholar
  9. [HJ98]
    Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice Hall International Series in Computer Science (1998)Google Scholar
  10. [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
  11. [HS06]
    He, J., Sanders, J.W.: Unifying probability. In: Dunne and Stoddart [ds06], pp. 173–199Google Scholar
  12. [MM04]
    McIver, A., Morgan, C.: Abstraction, Refinement and Proof For Probabilistic Systems. Monographs in Computer Science. Springer (2004)Google Scholar
  13. [Qin10]
    Qin, S. (ed.): UTP 2010. LNCS, vol. 6445. Springer, Heidelberg (2010)zbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Riccardo Bresciani
    • 1
  • Andrew Butterfield
    • 1
  1. 1.Foundations and Methods GroupTrinity College DublinDublinIreland

Personalised recommendations