Formalising semantics for expected running time of probabilistic programs

Abstract

We formalise two semantics observing the expected running time of pGCL programs. The first semantics is a denotational semantics providing a direct computation of the running time, similar to the weakest pre-expectation transformer. The second semantics interprets a pGCL program in terms of a Markov decision process (MDPs), i.e. it provides an operational semantics. Finally we show the equivalence of both running time semantics. We want to use this work to implement a program logic in Isabelle/HOL to verify the expected running time of pGCL programs. We base it on recent work by Kaminski, Katoen, Matheja, and Olmedo. We also formalise the expected running time for a simple symmetric random walk discovering a flaw in the original proof.