Results on the quantitative mu-calculus qMu
| dc.creator | McIver, Annabelle | |
| dc.creator | Morgan, Carroll | |
| dc.date | 2003-09-15 | |
| dc.date.accessioned | 2026-07-07T03:20:19Z | |
| dc.date.available | 2026-07-07T03:20:19Z | |
| dc.description | 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. | |
| dc.description | 45 pages, 4 figures | |
| dc.identifier | https://arxiv.org/abs/cs/0309024 | |
| dc.identifier | http://arxiv.org/abs/cs/0309024 | |
| dc.identifier.uri | http://salesiana.dossiersoluciones.com/handle/123456789/31787 | |
| dc.subject | Logic in Computer Science | |
| dc.subject | Computer Science and Game Theory | |
| dc.subject | D.2.4;F.1.2;F.3.1;F.4.1;G.3 | |
| dc.title | Results on the quantitative mu-calculus qMu | |
| dc.type | text |