2023/11/02 by Daniel Hausmann, Hausmann, Daniel, Merlin Humml +7 · 1 citation
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.2311.01315
openalex publication_date 2023/11/02 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.