Cost analysis of games, using program logic

Summary form only given. Recent work in probabilistic programming semantics has provided a relatively simple probabilistic extension to predicate transformers, making it possible to treat small imperative probabilistic programs containing both demonic and angelic nondeterminism. That work in turn has extended to provide a probabilistic basis for the modal μ-calculus of Kozen (1983), and leads to a quantitative μ-calculus. Standard (non-probabilistic) μ-calculus can be interpreted either ´normally´, over its semantic domain, or as a two-player game between an ´angel´ and a ´demon´ representing the two forms of choice. Stirling (1995) has argued that the two interpretations correspond. Quantitative p-calculus too can be interpreted both ways, with the novel interpretation being the second: a probabilistic game involving an angel and a demon. Each player seeks a strategy to maximise (resp. minimise) the game´s ´outcome´, with the steps in the game now being stochastic. That suggests a connection with Markov decision processes, in which players compete for high (resp. low) ´rewards´ over a Markov transition system. In this paper we explore that connection, showing how for example discounted Markov decision processes (MDP´s) and terminating MDP´s can be written as quantitative p-formulae. The ´normal´ interpretation of those formulae (i.e. over the semantic domain) then seems to give a much more direct access to existence theorems than the presentation usually associated with MDP´s. Our technical contribution is to explain the coding of MDP´s as quantitative p-formulae, to discuss the extension of the latte in incorporate ´rewards´, and to illustrate the resulting reformulation of several existence theorems. In an appendix we give an algebraic characterisation of the new quantitative-with-reward form of the calculus.