文章基本信息

标题：Model Checking Games for the Quantitative µ-Calculus
本地全文：下载
作者：Diana Fischer ; Erich Gr{\"a}del ; Lukasz Kaiser 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2008
卷号：1
页码：301-312
DOI：10.4230/LIPIcs.STACS.2008.1352
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：Games; logic; model checking; quantitative logics