Operational versus weakest precondition semantics for the probabilistic guarded command language

Friedrich Gretz; Joost Pieter Katoen; Annabelle McIver

doi:10.1109/QEST.2012.21

Operational versus weakest precondition semantics for the probabilistic guarded command language

Friedrich Gretz^*, Joost Pieter Katoen, Annabelle McIver

^*Corresponding author for this work

Department of Computing

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

6 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 language	English
Title of host publication	Proceedings - 2012 9th International Conference on Quantitative Evaluation of Systems, QEST 2012
Place of Publication	Piscataway, NJ
Publisher	Institute of Electrical and Electronics Engineers (IEEE)
Pages	168-177
Number of pages	10
ISBN (Print)	9780769547817
DOIs	https://doi.org/10.1109/QEST.2012.21
Publication status	Published - 2012
Event	2012 9th International Conference on Quantitative Evaluation of Systems, QEST 2012 - London, United Kingdom Duration: 17 Sep 2012 → 20 Sep 2012

Other

Other	2012 9th International Conference on Quantitative Evaluation of Systems, QEST 2012
Country	United Kingdom
City	London
Period	17/09/12 → 20/09/12

Access to Document

10.1109/QEST.2012.21

Link to publication in Scopus

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

@inproceedings{f15b01147e7d4cfdb03f3cbbbc37b287,

title = "Operational versus weakest precondition semantics for the probabilistic guarded command language",

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.",

author = "Friedrich Gretz and Katoen, {Joost Pieter} and Annabelle McIver",

year = "2012",

doi = "10.1109/QEST.2012.21",

language = "English",

isbn = "9780769547817",

pages = "168--177",

booktitle = "Proceedings - 2012 9th International Conference on Quantitative Evaluation of Systems, QEST 2012",

publisher = "Institute of Electrical and Electronics Engineers (IEEE)",

address = "United States",

}

Gretz, F, Katoen, JP & 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., 6354645, Institute of Electrical and Electronics Engineers (IEEE), Piscataway, NJ, pp. 168-177, 2012 9th International Conference on Quantitative Evaluation of Systems, QEST 2012, London, United Kingdom, 17/09/12. https://doi.org/10.1109/QEST.2012.21

Operational versus weakest precondition semantics for the probabilistic guarded command language. / Gretz, Friedrich; Katoen, Joost Pieter; McIver, Annabelle.

Proceedings - 2012 9th International Conference on Quantitative Evaluation of Systems, QEST 2012. Piscataway, NJ : Institute of Electrical and Electronics Engineers (IEEE), 2012. p. 168-177 6354645.

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

TY - GEN

T1 - Operational versus weakest precondition semantics for the probabilistic guarded command language

AU - Gretz, Friedrich

AU - Katoen, Joost Pieter

AU - McIver, Annabelle

PY - 2012

Y1 - 2012

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84870761374&partnerID=8YFLogxK

U2 - 10.1109/QEST.2012.21

DO - 10.1109/QEST.2012.21

M3 - Conference proceeding contribution

SN - 9780769547817

SP - 168

EP - 177

BT - Proceedings - 2012 9th International Conference on Quantitative Evaluation of Systems, QEST 2012

PB - Institute of Electrical and Electronics Engineers (IEEE)

CY - Piscataway, NJ

ER -