Tags:Implementation, Modal Logic, Reasoning, Tool and µ-Calculus
Abstract:
There is a wide range of modal logics for which Kripke frames, or transition systems, do not provide adequate semantics. These logics typically involve 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 are easily instantiated to particular, concretely given logics. This paper presents COOL 2, an implementation of fixpoint logics on the basis of the generic reasoning algorithms for coalgebraic logics. In concrete instances, we obtain a reasoner for the aconjunctive and alternation free fragments of the graded µ-calculus and the alternating-time µ-calculus. We evaluate the tool on standard benchmark sets for fixpoint-free graded modal logic as well as on a dedicated set of benchmarks for the graded µ-calculus.
COOL 2 - a Generic Reasoner for Modal Fixpoint Logics