Formalising Semantics for Expected Running Time of Probabilistic Programs
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.
ITP