Results on the quantitative mu-calculus qMu

TL;DR

This paper establishes the equivalence between the logical and operational interpretations of the quantitative mu-calculus (qMu) for finite-state systems, demonstrating its practical utility and extending game-theoretic results.

Contribution

It introduces a game-based semantics for qMu, proving equivalence with logical interpretation and extending Everett's game results to nested qMu formulas.

Findings

Logical and game-based interpretations are equivalent for finite-state qMu.

Fixed-point and strategy existence are proven for all nested qMu formulas.

The approach provides a practical tool for specifying probabilistic transition systems.

Abstract

The mu-calculus is a powerful tool for specifying and verifying transition systems, including those with both demonic and angelic choice; its quantitative generalisation qMu extends that to probabilistic choice. We show that for a finite-state system the logical interpretation of qMu, 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 logical interpretation provides direct access to axioms, laws and meta-theorems. The operational, game- based interpretation aids the intuition and continues in the more general context to provide a surprisingly practical specification tool. A corollary of our proofs is an extension of Everett's singly-nested games result in the finite turn-based case: we prove well-definedness of the minimax value, and existence of fixed memoriless strategies, for all qMu games/formulae, of arbitrary (including alternating) nesting structure.