Cited By
View all- Zhu HHe JQin SBrooke P(2015)Denotational semantics and its algebraic derivation for an event-driven system-level languageFormal Aspects of Computing10.1007/s00165-014-0309-827:1(133-166)Online publication date: 1-Jan-2015
A UTP semantics of pGCL as a homogeneous relation
Pages 191 - 205
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.
References
[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)
[2]
Butterfield, A. (ed.): UTP 2008. LNCS, vol. 5713, pp. 22-41. Springer, Heidelberg (2010)
[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)
[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)
[5]
Dunne, S., Stoddart, B. (eds.): UTP 2006. LNCS, vol. 4010, pp. 236-256. Springer, Heidelberg (2006)
[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)
[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)
[8]
He, J.: A probabilistic BPEL-like language. In: Qin {22}, pp. 74-100
[9]
He, J., Sanders, J. W.: Unifying probability. In: Dunne and Stoddart {5}, pp. 173- 199
[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 Applications
[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)
[12]
Hoare, C. A. R., He, J.: Unifying Theories of Programming. Prentice Hall International Series in Computer Science (1998)
[13]
Kozen, D.: Semantics of probabilistic programs. J. Comput. Syst. Sci. 22(3), 328- 350 (1981)
[14]
Kozen, D.: A probabilistic pdl. J. Comput. Syst. Sci. 30(2), 162-178 (1985)
[15]
McIver, A., Morgan, C.: Abstraction, Refinement And Proof For Probabilistic Systems (Monographs in Computer Science). Springer, Heidelberg (2004)
[16]
McIver, A., Morgan, C.: Abstraction and refinement in probabilistic systems. SIGMETRICS Performance Evaluation Review 32(4), 41-47 (2005)
[17]
Morgan, C., McIver, A.: A probabilistic temporal calculus based on expectations. Technical Report PRG-TR-13-97, Oxford University Computing Laboratory (1997)
[18]
Morgan, C., McIver, A., Seidel, K., Sanders, J. W.: Refinement-oriented probability for CSP. Formal Asp. Comput. 8(6), 617-647 (1996)
[19]
Ndukwu, U., McIver, A.: An expectation transformer approach to predicate abstraction and data independence for probabilistic programs. CoRR (2010)
[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)
[21]
Oliveira, M., Cavalcanti, A., Woodcock, J.: A UTP semantics for Circus. Formal Asp. Comput. 21(1-2), 3-32 (2009)
[22]
Qin, S. (ed.): UTP 2010. LNCS, vol. 6445, pp. 188-206. Springer, Heidelberg (2010)
[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)
- A UTP semantics of pGCL as a homogeneous relation
Recommendations
A UTP semantics for Circus
AbstractCircus specifications define both data and behavioural aspects of systems using a combination of Z and CSP constructs. Previously, a denotational semantics has been given to Circus; however, a shallow embedding of Circus in Z, in which the mapping ...
Mechanical reasoning about families of UTP theories
The Unifying Theories of Programming (UTP) of Hoare and He is a general framework in which the semantics of a variety of specification and programming languages can be uniformly defined. In this paper we present a semantic embedding of the UTP into the ...
Theoretical and Practical Approaches to the Denotational Semantics for MDESL based on UTP
AbstractThe hardware description language Verilog has been standardized and widely used in industry. Multithreaded Discrete Event Simulation Language (MDESL) is a Verilog-like language and it contains a rich variety of interesting features such as the ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
June 2012
357 pages
ISBN:9783642307287
Sponsors
- INTECS: INTECS S.p.A.
- FME: Formal Methods Europe
- EATCS: European Association for Theoretical Computer Science
- BNL: Banca Nazionale del Lavoro S.p.A.
Publisher
Springer-Verlag
Berlin, Heidelberg
Publication History
Published: 15 June 2012
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 14 Dec 2024
Other Metrics
Citations
Cited By
View all- Zhu HHe JQin SBrooke P(2015)Denotational semantics and its algebraic derivation for an event-driven system-level languageFormal Aspects of Computing10.1007/s00165-014-0309-827:1(133-166)Online publication date: 1-Jan-2015