Browsing by Author "Strahlberger, Aaron"

Filter results by typing the first few letters
Now showing 1 - 1 of 1
  • 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.