Results on the quantitative μ-calculus qMμ

Annabelle McIver*, Carroll Morgan

*Corresponding author for this work

Research output: Contribution to journalArticle

29 Citations (Scopus)

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

Original languageEnglish
Article number3
Pages (from-to)1-43
Number of pages43
JournalACM Transactions on Computational Logic
Volume8
Issue number1
DOIs
Publication statusPublished - 1 Jan 2007

Fingerprint Dive into the research topics of 'Results on the quantitative μ-calculus qMμ'. Together they form a unique fingerprint.

  • Cite this