Quantitative µ-Calculus: A Logical and Operational Interpretation

Title: Quantitative µ-Calculus: A Logical and Operational Interpretation

Research Question: How can we develop a quantitative version of the µ-calculus, a powerful tool for specifying and verifying transition systems, that combines both logical and operational interpretations?

Methodology: We propose two complementary interpretations of the quantitative µ-calculus: a logical interpretation based on fixed points and a operational interpretation based on a turn-based gambling game. Both interpretations are applied to a finite-state system.

Results: We prove the equivalence of the two interpretations, providing direct access to axioms, laws, and meta-theorems. The logical interpretation offers a solid interface linking the logical and operational frameworks, benefiting from both. The operational interpretation aids intuition and continues to provide a practical specification tool in more general contexts.

Implications: The quantitative µ-calculus provides a powerful tool for expressing and verifying probabilistic choice in transition systems. The equivalence of the logical and operational interpretations offers a complete and intuitive understanding of the calculus, making it applicable to a wide range of applications.

Link to Article: https://arxiv.org/abs/0309024v1 Authors: arXiv ID: 0309024v1