There is a wide range of modal logics whose semantics goes beyond relational structures, and instead involves, e.g., probabilities, multi-player games, weights, or neighbourhood structures. Coalgebraic logic serves as a unifying semantic and algorithmic framework for such logics. It provides uniform reasoning algorithms that are easily instantiated to particular, concretely given logics. The COOL 2 reasoner provides an implementation of such generic algorithms for coalgebraic modal fixpoint logics. As concrete instances, we obtain in particular reasoners for the aconjunctive and alternation-free fragments of the graded $\mu$-calculus and the alternating-time $\mu$-calculus. We evaluate the tool on standard benchmark sets for fixpoint-free graded modal logic and alternating-time temporal logic (ATL), as well as on a dedicated set of benchmarks for the graded $\mu$-calculus.

翻译：存在一类广泛的模态逻辑，其语义超出关系结构范畴，涉及概率、多玩家博弈、权重或邻域结构等。余代数逻辑为这类逻辑提供了统一的语义与算法框架，并通过易于实例化到具体逻辑的通用推理算法实现。COOL 2推理器实现了上述用于余代数模态不动点逻辑的通用算法。作为具体实例，我们获得了分数阶μ演算和交替时间μ演算的非合取与无交错片段的推理器。该工具在无不动点的分数阶模态逻辑与交替时间时态逻辑的标准基准测试集，以及专为分数阶μ演算设计的基准测试集上进行了评估。