DROPS

Document

DOI: 10.4230/LIPIcs.STACS.2008.1352

Model Checking Games for the Quantitative µ-Calculus

Authors: Diana Fischer, Erich Grädel, and Lukasz Kaiser

Published in: LIPIcs, Volume 1, 25th International Symposium on Theoretical Aspects of Computer Science (2008)

Abstract

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.

Cite as

Diana Fischer, Erich Grädel, and Lukasz Kaiser. Model Checking Games for the Quantitative µ-Calculus. In 25th International Symposium on Theoretical Aspects of Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 1, pp. 301-312, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{fischer_et_al:LIPIcs.STACS.2008.1352,
  author =	{Fischer, Diana and Gr\"{a}del, Erich and Kaiser, Lukasz},
  title =	{{Model Checking Games for the Quantitative µ-Calculus}},
  booktitle =	{25th International Symposium on Theoretical Aspects of Computer Science},
  pages =	{301--312},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-06-4},
  ISSN =	{1868-8969},
  year =	{2008},
  volume =	{1},
  editor =	{Albers, Susanne and Weil, Pascal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2008.1352},
  URN =		{urn:nbn:de:0030-drops-13525},
  doi =		{10.4230/LIPIcs.STACS.2008.1352},
  annote =	{Keywords: Games, logic, model checking, quantitative logics}
}

Search Results

Documents authored by Fischer, Diana

Model Checking Games for the Quantitative µ-Calculus

Abstract

Cite as

Thanks for your feedback!

Could not send message