The Mu-calculus is a powerful tool for specifying and verifying
transition systems, including those with demonic (universal) and
angelic (existential) choice; its quantitative generalisation qMu ---
a quantitative real-typed calculus --- extends that to include
probabilistic choice by interpreting expressions as real- rather than
Boolean-valued functions of the state. qMu can be used to generate
proof rules for probabilistic temporal logic, and, more generally, is
expressive enough to formalise a wide range of problems from the
theory of Markov Decision Processes.
Kozen defined the standard Boolean-typed calculus denotationally for
the Mu-calculus; later Stirling gave it an operational interpretation
as a turn-based game between two players, and showed that the two
interpretations are equivalent.
In this talk I'll show how the same can be done for qMu so that the
quantitative real-typed calculus corresponds to a two-player gambling
game, thus providing a solid interface linking the logical and
operational frameworks.
|