Results on the quantitative μ-calculus <i>qM</i> μ

Abstract

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 verification techniques is mathematically justified in the practical computation of probabilistic system properties.