10.4230/LIPICS.STACS.2008.1352
Fischer, Diana
Diana
Fischer
Grädel, Erich
Erich
Grädel
Kaiser, Lukasz
Lukasz
Kaiser
Model Checking Games for the Quantitative µ-Calculus
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
2008
Article
Games
logic
model checking
quantitative logics
Albers, Susanne
Susanne
Albers
Weil, Pascal
Pascal
Weil
2008
2008-02-06
2008-02-06
2008-02-06
en
urn:nbn:de:0030-drops-13525
10.4230/LIPIcs.STACS.2008
978-3-939897-06-4
1868-8969
10.4230/LIPIcs.STACS.2008
LIPIcs, Volume 1, STACS 2008
25th International Symposium on Theoretical Aspects of Computer Science
2013
1
27
301
312
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Albers, Susanne
Susanne
Albers
Weil, Pascal
Pascal
Weil
1868-8969
Leibniz International Proceedings in Informatics (LIPIcs)
2008
1
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
12 pages
193961 bytes
application/pdf
Creative Commons Attribution-NoDerivs 3.0 Unported license
info:eu-repo/semantics/openAccess
We investigate quantitative extensions of modal logic and the modal
$mu$-calculus, and study the question whether the tight connection
between logic and games can be lifted from the qualitative logics
to their quantitative counterparts. It turns out that, if the
quantitative $mu$-calculus is defined in an appropriate way
respecting the duality properties between the logical operators,
then its model checking problem can indeed be characterised by a
quantitative variant of parity games. However, these quantitative
games have quite different properties than their classical
counterparts, in particular they are, in general, not positionally
determined. The correspondence between the logic and the games
goes both ways: the value of a formula on a quantitative transition
system coincides with the value of the associated quantitative
game, and conversely, the values of quantitative parity games are
definable in the quantitative $mu$-calculus.
LIPIcs, Vol. 1, 25th International Symposium on Theoretical Aspects of Computer Science, pages 301-312