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进行了评估。