Article

A UTP semantics of pGCL as a homogeneous relation

Authors:

Riccardo Bresciani,

Andrew ButterfieldAuthors Info & Claims

IFM'12: Proceedings of the 9th international conference on Integrated Formal Methods

Pages 191 - 205

https://doi.org/10.1007/978-3-642-30729-4_14

Published: 15 June 2012 Publication History

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)

Digital Library

[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)

Digital Library

[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)

Digital Library

[8]

He, J.: A probabilistic BPEL-like language. In: Qin {22}, pp. 74-100

Digital Library

[9]

He, J., Sanders, J. W.: Unifying probability. In: Dunne and Stoddart {5}, pp. 173- 199

Digital Library

[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

Digital Library

[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)

Digital Library

[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)

Digital Library

[16]

McIver, A., Morgan, C.: Abstraction and refinement in probabilistic systems. SIGMETRICS Performance Evaluation Review 32(4), 41-47 (2005)

Digital Library

[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)

Digital Library

[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)

Digital Library

Cited By

Zhao HZhu HSheng FHe JBowen J(2025)Theoretical and Practical Approach to the Soundness and Completeness of Operational Semantics based on Denotational Semantics for MDESLFormal Aspects of Computing10.1145/369643237:2(1-51)Online publication date: 3-Mar-2025
https://dl.acm.org/doi/10.1145/3696432
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
https://dl.acm.org/doi/10.1007/s00165-014-0309-8

A UTP semantics of pGCL as a homogeneous relation
1. Theory of computation
  1. Semantics and reasoning

Recommendations

A UTP semantics for Circus
Abstract
Circus 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
Abstract
The 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

cover image Guide Proceedings

IFM'12: Proceedings of the 9th international conference on Integrated Formal Methods

June 2012

357 pages

ISBN:9783642307287

Editors:
John Derrick
Department of Computer Science, University of Sheffield, Regent Court, 211 Portobello Street, Sheffield, UK
,
Stefania Gnesi
Department of Computer Science, Consiglio Nazionale delle Ricerche, Istituto di Scienza e Tecnologie dell'Informazione “A. Faedo”, Via Moruzzi 1, Pisa, Italy
,
Diego Latella
Department of Computer Science, Consiglio Nazionale delle Ricerche, Istituto di Scienza e Tecnologie dell'Informazione “A. Faedo”, Via Moruzzi 1, Pisa, Italy
,
Helen Treharne
Department of Computing, University of Surrey, Via Moruzzi 1, Surrey, UK

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

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 05 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Zhao HZhu HSheng FHe JBowen J(2025)Theoretical and Practical Approach to the Soundness and Completeness of Operational Semantics based on Denotational Semantics for MDESLFormal Aspects of Computing10.1145/369643237:2(1-51)Online publication date: 3-Mar-2025
https://dl.acm.org/doi/10.1145/3696432
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
https://dl.acm.org/doi/10.1007/s00165-014-0309-8

View Options

View options

Figures

Tables

Media

View Table of Conten