Games, probability, and the quantitative μ-calculus qMμ

A. K. McIver, C. C. Morgan

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contribution

30 Citations (Scopus)

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.

Original languageEnglish
Title of host publicationLogic for Programming, Artificial Intelligence, and Reasoning - 9th International Conference, LPAR 2002, Proceedings
EditorsMatthias Baaz, Andrei Voronkov
Place of PublicationBerlin; Heidelberg
PublisherSpringer, Springer Nature
Pages292-310
Number of pages19
Volume2514
ISBN (Print)3540000100, 9783540000105
Publication statusPublished - 2002
Event9th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2002 - Tbilisi, Georgia
Duration: 14 Oct 200218 Oct 2002

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2514
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other9th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2002
CountryGeorgia
CityTbilisi
Period14/10/0218/10/02

Fingerprint Dive into the research topics of 'Games, probability, and the quantitative μ-calculus qMμ'. Together they form a unique fingerprint.

Cite this