Generic Model Checking for Modal Fixpoint Logics in COOL-MC
Authors:
Daniel Hausmann,
Merlin Humml,
Simon Prucker,
Lutz Schröder,
Aaron Strahlberger
Abstract:
We report on COOL-MC, a model checking tool for fixpoint logics that is parametric in the branching type of models (nondeterministic, game-based, probabilistic etc.) and in the next-step modalities used in formulae. The tool implements generic model checking algorithms developed in coalgebraic logic that are easily adapted to concrete instance logics. Apart from the standard modal $μ$-calculus, CO…
▽ More
We report on COOL-MC, a model checking tool for fixpoint logics that is parametric in the branching type of models (nondeterministic, game-based, probabilistic etc.) and in the next-step modalities used in formulae. The tool implements generic model checking algorithms developed in coalgebraic logic that are easily adapted to concrete instance logics. Apart from the standard modal $μ$-calculus, COOL-MC currently supports alternating-time, graded, probabilistic and monotone variants of the $μ$-calculus, but is also effortlessly extensible with new instance logics. The model checking process is realized by polynomial reductions to parity game solving, or, alternatively, by a local model checking algorithm that directly computes the extensions of formulae in a lazy fashion, thereby potentially avoiding the construction of the full parity game. We evaluate COOL-MC on informative benchmark sets.
△ Less
Submitted 3 November, 2023; v1 submitted 2 November, 2023;
originally announced November 2023.
