Game-based local model checking for the coalgebraic µ-calculus
Hausmann D, Schröder L (2019)
Publication Type: Conference contribution
Publication year: 2019
Journal
Publisher: Schloss Dagstuhl-Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing
Book Volume: 140
Conference Proceedings Title: Leibniz International Proceedings in Informatics, LIPIcs
Event location: Amsterdam
ISBN: 9783959771214
DOI: 10.4230/LIPIcs.CONCUR.2019.35
Abstract
The coalgebraic µ-calculus is a generic framework for fixpoint logics with varying branching types that subsumes, besides the standard relational µ-calculus, such diverse logics as the graded µ-calculus, the monotone µ-calculus, the probabilistic µ-calculus, and the alternating-time µ-calculus. In the present work, we give a local model checking algorithm for the coalgebraic µ-calculus using a coalgebraic variant of parity games that runs, under mild assumptions on the complexity of the so-called one-step satisfaction problem, in time pk where p is a polynomial in the formula and model size and where k is the alternation depth of the formula. We show moreover that under the same assumptions, the model checking problem is in NP ∩ coNP, improving the complexity in all mentioned non-relational cases. If one-step satisfaction can be solved by means of small finite games, we moreover obtain standard parity games, ensuring quasi-polynomial run time. This applies in particular to the monotone µ-calculus, the alternating-time µ-calculus, and the graded µ-calculus with grades coded in unary.
Authors with CRIS profile
Daniel Hausmann
Lehrstuhl für Informatik 8 (Theoretische Informatik)
Lutz Schröder
Lehrstuhl für Informatik 8 (Theoretische Informatik)
Related research project(s)
How to cite
APA:
Hausmann, D., & Schröder, L. (2019). Game-based local model checking for the coalgebraic µ-calculus. In Wan Fokkink, Rob van Glabbeek (Eds.), Leibniz International Proceedings in Informatics, LIPIcs. Amsterdam, NL: Schloss Dagstuhl-Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing.
MLA:
Hausmann, Daniel, and Lutz Schröder. "Game-based local model checking for the coalgebraic µ-calculus." Proceedings of the 30th International Conference on Concurrency Theory, CONCUR 2019, Amsterdam Ed. Wan Fokkink, Rob van Glabbeek, Schloss Dagstuhl-Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing, 2019.
BibTeX: Download