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.

翻译：我们报告了COOL-MC——一个针对不动点逻辑的模型检测工具，该工具在模型的分支类型（非确定性、基于博弈、概率等）以及公式中使用的下一步模态方面具有参数化特性。该工具实现了余代数逻辑中开发的通用模型检测算法，可轻松适应具体的实例逻辑。除标准模态μ-演算外，COOL-MC目前支持交替时间、分级、概率和单调变体的μ-演算，并且能够毫不费力地扩展新的实例逻辑。模型检测过程通过多项式归约到奇偶博弈求解来实现，或者通过一种局部模型检测算法直接以延迟方式计算公式的外延，从而可能避免构建完整的奇偶博弈。我们基于有代表性的基准测试集对COOL-MC进行了评估。