Games, probability, and the quantitative μ-calculus qMμ

The μ-calculus is a powerful tool for specifying and verifying transition systems, including those with demonic (universal) and angelic (existential) choice; its quantitative generalisation qMμ extends that to probabilistic choice.We show for a finite-state system that the straightforward denotational interpretation of the quantitative μ-calculus is equivalent to an operational interpretation given as a turn-based gambling game between two players. Kozen defined the standard Boolean-typed calculus denotationally; later Stirling gave it an operational interpretation as a turn-based game between two players, and showed the two interpretations equivalent. By doing the same for the quantitative real-typed calculus, we set it on a par with the standard calculus, in that it too can benefit from a solid interface linking the logical and operational frameworks. Stirling’s game analogy, as an aid to intuition, continues in the more general context to provide a surprisingly practical specification tool, meeting for example Vardi’s challenge to “figure out the meaning of AFAXp” as a branching-time formula. We also show that memoriless strategies suffice for achieving the minimax value of a quantitative game, when the state space is finite.