@inproceedings{f66c05b2916a46abbbb33985b0732fd0,

title = "Games, probability, and the quantitative μ-calculus qMμ",

abstract = "The μ-calculus is a powerful tool for specifying and verifying transition systems, including those with demonic (universal) and angelic (existential) choice; its quantitative generalisation qMμ extends that to probabilistic choice.We show for a finite-state system that the straightforward denotational interpretation of the quantitative μ-calculus is equivalent to an operational interpretation given as a turn-based gambling game between two players. Kozen defined the standard Boolean-typed calculus denotationally; later Stirling gave it an operational interpretation as a turn-based game between two players, and showed the two interpretations equivalent. By doing the same for the quantitative real-typed calculus, we set it on a par with the standard calculus, in that it too can benefit from a solid interface linking the logical and operational frameworks. Stirling’s game analogy, as an aid to intuition, continues in the more general context to provide a surprisingly practical specification tool, meeting for example Vardi’s challenge to “figure out the meaning of AFAXp” as a branching-time formula. We also show that memoriless strategies suffice for achieving the minimax value of a quantitative game, when the state space is finite.",

author = "McIver, {A. K.} and Morgan, {C. C.}",

year = "2002",

language = "English",

isbn = "3540000100",

volume = "2514",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer, Springer Nature",

pages = "292--310",

editor = "Baaz, {Matthias } and Andrei Voronkov",

booktitle = "Logic for Programming, Artificial Intelligence, and Reasoning - 9th International Conference, LPAR 2002, Proceedings",

address = "United States",

}