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