Generic Model Checking for Modal Fixpoint Logics in COOL-MC - VMCAI'24

Explore a comprehensive presentation on COOL-MC, a versatile model checking tool for fixpoint logics. Delve into the tool's parametric nature, allowing for various branching types in models and next-step modalities in formulae. Discover how COOL-MC implements generic model checking algorithms from coalgebraic logic, easily adaptable to specific instance logics. Learn about its support for standard modal µ-calculus, as well as alternating-time, graded, probabilistic, and monotone variants. Understand the model checking process, which utilizes polynomial reductions to parity game solving or a local model checking algorithm for lazy computation of formula extensions. Examine the tool's performance through informative benchmark evaluations and gain insights into its extensibility for new instance logics.