Hausmann, Daniel ;
Schröder, Lutz
GameBased Local Model Checking for the Coalgebraic muCalculus
Abstract
The coalgebraic mucalculus is a generic framework for fixpoint logics with varying branching types that subsumes, besides the standard relational mucalculus, such diverse logics as the graded mucalculus, the monotone mucalculus, the probabilistic mucalculus, and the alternatingtime mucalculus. In the present work, we give a local model checking algorithm for the coalgebraic mucalculus using a coalgebraic variant of parity games that runs, under mild assumptions on the complexity of the socalled onestep satisfaction problem, in time p^k 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 both NP and coNP, improving the complexity in all mentioned nonrelational cases. If onestep satisfaction can be solved by means of small finite games, we moreover obtain standard parity games, ensuring quasipolynomial run time. This applies in particular to the monotone mucalculus, the alternatingtime mucalculus, and the graded mucalculus with grades coded in unary.
BibTeX  Entry
@InProceedings{hausmann_et_al:LIPIcs:2019:10937,
author = {Daniel Hausmann and Lutz Schr{\"o}der},
title = {{GameBased Local Model Checking for the Coalgebraic muCalculus}},
booktitle = {30th International Conference on Concurrency Theory (CONCUR 2019)},
pages = {35:135:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959771214},
ISSN = {18688969},
year = {2019},
volume = {140},
editor = {Wan Fokkink and Rob van Glabbeek},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2019/10937},
URN = {urn:nbn:de:0030drops109373},
doi = {10.4230/LIPIcs.CONCUR.2019.35},
annote = {Keywords: Model checking, mucalculus, coalgebraic logic, graded mucalculus, probabilistic mucalculus, parity games}
}
20.08.2019
Keywords: 

Model checking, mucalculus, coalgebraic logic, graded mucalculus, probabilistic mucalculus, parity games 
Seminar: 

30th International Conference on Concurrency Theory (CONCUR 2019)

Issue date: 

2019 
Date of publication: 

20.08.2019 