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 journalArticle

26 Citations (Scopus)

Abstract

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
Volume73
DOIs
Publication statusPublished - Mar 2014

Fingerprint 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