Operational Versus Weakest Precondition Semantics for the Probabilistic Guarded Command Language
Friedrich Gretz, Joost-Pieter Katoen, Annabelle K. McIver · 2012
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.