Generic Model Checking for Modal Fixpoint Logics in COOL-MC
summary
COOL-MC is a model checker for coalgebraic μ-calculi that is parametric in branching type and modal operators and implements both a lazy local solver that builds game graphs on the fly and a reduction-based path that does polynomial reductions to parity games and uses external PG solvers (currently PG Solver). Claims: model checking is in NP ∩ coNP and quasi‑polynomial; tool supports alternating‑time, graded, probabilistic and monotone μ‑calculi; benchmarks show lazy solving explores tiny fractions of some models and wins there but is slower on engineered hard cases, and symbolic tools like MCMAS still outperform in ATL.
AI-written summary · about