Generic Model Checking for Modal Fixpoint Logics in COOL-MC

Abstract

We report on COOL-MC, a model checking tool for fixpoint logics that is parametric in the branching type of models (non-deterministic, 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.