Generic Model Checking for Modal Fixpoint Logics in COOL-MC

TL;DR

COOL-MC is a versatile model checking tool for various fixpoint logics, supporting multiple model types and logic variants through generic algorithms, with efficient solving methods and extensibility.

Contribution

It introduces a parametric, coalgebraic framework for model checking diverse fixpoint logics, enabling easy extension and efficient solving techniques.

Findings

Supports multiple logic variants including probabilistic and monotone μ-calculus.

Employs polynomial reductions to parity games and local algorithms for efficiency.

Successfully evaluated on benchmark sets demonstrating effectiveness.

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 $\mu$-calculus, COOL-MC currently supports alternating-time, graded, probabilistic and monotone variants of the $\mu$-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.