Browsing by Author "Humml, Merlin"

Filter results by typing the first few letters
Now showing 1 - 2 of 2
  • No Thumbnail Available
    Item
    COOL 2 – A Generic Reasoner for Modal Fixpoint Logics (System Description)
    (2023) Görlitz, Oliver; Hausmann, Daniel; Humml, Merlin; Pattinson, Dirk; Prucker, Simon; Schröder, Lutz
    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 μ -calculus and the alternating-time μ -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 μ -calculus.
  • No Thumbnail Available
    Item
    Generic Model Checking for Modal Fixpoint Logics in COOL-MC
    (2023) Hausmann, Daniel; Humml, Merlin; Prucker, Simon; Schröder, Lutz; Strahlberger, Aaron
    We report on COOL-MC, a model checking tool for fixpoint logics that is parametric in the branching type of models (non-deterministic, 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 -calculus, COOL-MC currently supports alternating-time, graded, probabilistic and monotone variants of the -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.