Operational versus weakest precondition semantics for the probabilistic guarded command language

Friedrich Gretz*, Joost Pieter Katoen, Annabelle McIver

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contribution

5 Citations (Scopus)

Abstract

This paper proposes a simple operational semanticsof pGCL, Dijkstra's guarded command language extended withprobabilistic choice, and relates this to pGCL's wp-semantics byMcIver and Morgan. Parameterised Markov decision processeswhose state rewards depend on the post-expectation at handare used as operational model. We show that the weakest pre-expectationof a pGCL-program w.r.t. a post-expectation correspondsto the expected cumulative reward to reach a terminalstate in the parameterised MDP associated to the program. In asimilar way, we show a correspondence between weakest liberalpre-expectations and liberal expected cumulative rewards.

Original languageEnglish
Title of host publicationProceedings - 2012 9th International Conference on Quantitative Evaluation of Systems, QEST 2012
Place of PublicationPiscataway, NJ
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
Pages168-177
Number of pages10
ISBN (Print)9780769547817
DOIs
Publication statusPublished - 2012
Event2012 9th International Conference on Quantitative Evaluation of Systems, QEST 2012 - London, United Kingdom
Duration: 17 Sep 201220 Sep 2012

Other

Other2012 9th International Conference on Quantitative Evaluation of Systems, QEST 2012
CountryUnited Kingdom
CityLondon
Period17/09/1220/09/12

Fingerprint Dive into the research topics of 'Operational versus weakest precondition semantics for the probabilistic guarded command language'. Together they form a unique fingerprint.

  • Cite this

    Gretz, F., Katoen, J. P., & McIver, A. (2012). Operational versus weakest precondition semantics for the probabilistic guarded command language. In Proceedings - 2012 9th International Conference on Quantitative Evaluation of Systems, QEST 2012 (pp. 168-177). [6354645] Piscataway, NJ: Institute of Electrical and Electronics Engineers (IEEE). https://doi.org/10.1109/QEST.2012.21