Results on the quantitative μ-calculus qMμ

The μ-calculus is a powerful tool for specifying and verifying transition systems, including those with both demonic (universal) and angelic (existential) choice; its quantitative generalization qMμ extends to include probabilistic choice. We make two major contributions to the theory of such systems. The first is to show that for a finite-state system, the logical interpretation of qMμ, via fixed points in a domain of real-valued functions into [0, 1], is equivalent to an operational interpretation given as a turn-based gambling game between two players. The second contribution is to show that each player in the gambling game has an optimal memoryless strategy-that is, a strategy which is independent of the game's history, and with which a player can achieve his optimal expected reward however his opponent chooses to play. Moreover, since qMμ is expressive enough to encode stochastic parity games, our result implies the existence of memoryless strategies in that framework, as well. As an additional feature, we include an extensive case study demonstrating the aforementioned duality between games and logic. Among other things, it shows that the use of algorithmic verifi-cation techniques is mathematically justified in the practical computation of probabilistic system properties.