Operational versus weakest pre-expectation semantics for the probabilistic guarded command language

Friedrich Gretz*, Joost Pieter Katoen, Annabelle McIver

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

43 Citations (Scopus)


This paper proposes a simple operational semantics of pGCL, Dijkstra's guarded command language extended with probabilistic choice, and relates this to pGCL's wp-semantics by McIver and Morgan. Parametric Markov decision processes whose state rewards depend on the post-expectation at hand are used as the operational model. We show that the weakest pre-expectation of a pGCL-program w.r.t. a post-expectation corresponds to the expected cumulative reward to reach a terminal state in the parametric MDP associated to the program. In a similar way, we show a correspondence between weakest liberal pre-expectations and liberal expected cumulative rewards. The verification of probabilistic programs using wp-semantics and operational semantics is illustrated using a simple running example.

Original languageEnglish
Pages (from-to)110-132
Number of pages23
JournalPerformance Evaluation
Publication statusPublished - Mar 2014


  • Expectation transformer semantics
  • Expected rewards
  • Markov decision process
  • Operational semantics


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

Cite this