A UTP Semantics of pGCL as a Homogeneous Relation

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


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 define a generic choice construct, that covers conditional, probabilistic and non-deterministic choice. As an example we study the Monty Hall game in this framework.


Semantic Model Probabilistic Choice Probabilistic Program Homogeneous Relation Galois Connection 
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. 1.
    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. 2.
    Butterfield, A. (ed.): UTP 2008. LNCS, vol. 5713, pp. 22–41. Springer, Heidelberg (2010)zbMATHCrossRefGoogle Scholar
  3. 3.
    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
  4. 4.
    Deng, Y., van Glabbeek, R.J., Hennessy, M., Morgan, C.: Characterising testing preorders for finite probabilistic processes. Logical Methods in Computer Science 4(4) (2008)Google Scholar
  5. 5.
    Dunne, S., Stoddart, B. (eds.): UTP 2006. LNCS, vol. 4010, pp. 236–256. Springer, Heidelberg (2006)zbMATHCrossRefGoogle Scholar
  6. 6.
    Freitas, L., Woodcock, J., Butterfield, A.: Posix and the verification grand challenge: A roadmap. In: 13th IEEE International Conference on Engineering of Complex Computer Systems, ICECCS 2008, March 31-April 3, pp. 153–162 (2008)Google Scholar
  7. 7.
    Gancarski, P., Butterfield, A.: The Denotational Semantics of slotted-Circus. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 451–466. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  8. 8.
    He, J.: A probabilistic BPEL-like language. In: Qin [22], pp. 74–100Google Scholar
  9. 9.
    He, J., Sanders, J.W.: Unifying probability. In: Dunne and Stoddart [5], pp. 173–199Google Scholar
  10. 10.
    He, J., Seidel, K., McIver, A.: Probabilistic models for the guarded command language. Science of Computer Programming 28(2-3), 171–192 (1997); Formal Specifications: Foundations, Methods, Tools and ApplicationsMathSciNetzbMATHCrossRefGoogle Scholar
  11. 11.
    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
  12. 12.
    Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice Hall International Series in Computer Science (1998)Google Scholar
  13. 13.
    Kozen, D.: Semantics of probabilistic programs. J. Comput. Syst. Sci. 22(3), 328–350 (1981)MathSciNetzbMATHCrossRefGoogle Scholar
  14. 14.
    Kozen, D.: A probabilistic pdl. J. Comput. Syst. Sci. 30(2), 162–178 (1985)MathSciNetzbMATHCrossRefGoogle Scholar
  15. 15.
    McIver, A., Morgan, C.: Abstraction, Refinement And Proof For Probabilistic Systems (Monographs in Computer Science). Springer, Heidelberg (2004)Google Scholar
  16. 16.
    McIver, A., Morgan, C.: Abstraction and refinement in probabilistic systems. SIGMETRICS Performance Evaluation Review 32(4), 41–47 (2005)CrossRefGoogle Scholar
  17. 17.
    Morgan, C., McIver, A.: A probabilistic temporal calculus based on expectations. Technical Report PRG-TR-13-97, Oxford University Computing Laboratory (1997)Google Scholar
  18. 18.
    Morgan, C., McIver, A., Seidel, K., Sanders, J.W.: Refinement-oriented probability for CSP. Formal Asp. Comput. 8(6), 617–647 (1996)zbMATHCrossRefGoogle Scholar
  19. 19.
    Ndukwu, U., McIver, A.: An expectation transformer approach to predicate abstraction and data independence for probabilistic programs. CoRR (2010)Google Scholar
  20. 20.
    Ndukwu, U., Sanders, J.W.: Reasoning about a distributed probabilistic system. In: Downey, R., Manyem, P. (eds.) Fifteenth Computing: The Australasian Theory Symposium (CATS 2009). CRPIT, vol. 94, pp. 35–42. ACS, Wellington (2009)Google Scholar
  21. 21.
    Oliveira, M., Cavalcanti, A., Woodcock, J.: A UTP semantics for Circus. Formal Asp. Comput. 21(1-2), 3–32 (2009)zbMATHCrossRefGoogle Scholar
  22. 22.
    Qin, S. (ed.): UTP 2010. LNCS, vol. 6445, pp. 188–206. Springer, Heidelberg (2010)zbMATHCrossRefGoogle Scholar
  23. 23.
    Sherif, A., Kleinberg, R.D.: Towards a Time Model for Circus. In: George, C.W., Miao, H. (eds.) ICFEM 2002. LNCS, vol. 2495, pp. 613–624. Springer, Heidelberg (2002)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

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

Personalised recommendations