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 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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
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)
Butterfield, A. (ed.): UTP 2008. LNCS, vol. 5713, pp. 22–41. Springer, Heidelberg (2010)
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)
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)
Dunne, S., Stoddart, B. (eds.): UTP 2006. LNCS, vol. 4010, pp. 236–256. Springer, Heidelberg (2006)
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)
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)
He, J.: A probabilistic BPEL-like language. In: Qin [22], pp. 74–100
He, J., Sanders, J.W.: Unifying probability. In: Dunne and Stoddart [5], pp. 173–199
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 Applications
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)
Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice Hall International Series in Computer Science (1998)
Kozen, D.: Semantics of probabilistic programs. J. Comput. Syst. Sci. 22(3), 328–350 (1981)
Kozen, D.: A probabilistic pdl. J. Comput. Syst. Sci. 30(2), 162–178 (1985)
McIver, A., Morgan, C.: Abstraction, Refinement And Proof For Probabilistic Systems (Monographs in Computer Science). Springer, Heidelberg (2004)
McIver, A., Morgan, C.: Abstraction and refinement in probabilistic systems. SIGMETRICS Performance Evaluation Review 32(4), 41–47 (2005)
Morgan, C., McIver, A.: A probabilistic temporal calculus based on expectations. Technical Report PRG-TR-13-97, Oxford University Computing Laboratory (1997)
Morgan, C., McIver, A., Seidel, K., Sanders, J.W.: Refinement-oriented probability for CSP. Formal Asp. Comput. 8(6), 617–647 (1996)
Ndukwu, U., McIver, A.: An expectation transformer approach to predicate abstraction and data independence for probabilistic programs. CoRR (2010)
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)
Oliveira, M., Cavalcanti, A., Woodcock, J.: A UTP semantics for Circus. Formal Asp. Comput. 21(1-2), 3–32 (2009)
Qin, S. (ed.): UTP 2010. LNCS, vol. 6445, pp. 188–206. Springer, Heidelberg (2010)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bresciani, R., Butterfield, A. (2012). A UTP Semantics of pGCL as a Homogeneous Relation. In: Derrick, J., Gnesi, S., Latella, D., Treharne, H. (eds) Integrated Formal Methods. IFM 2012. Lecture Notes in Computer Science, vol 7321. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-30729-4_14
Download citation
DOI: https://doi.org/10.1007/978-3-642-30729-4_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-30728-7
Online ISBN: 978-3-642-30729-4
eBook Packages: Computer ScienceComputer Science (R0)