Generic Model Checking for Modal Fixpoint Logics in COOL-MC

Hausmann D, Humml M, Prucker S, Schröder L, Strahlberger A (2024)

Publication Type: Conference contribution

Publication year: 2024

Journal

Lecture Notes in Computer Science Springer Verlag

Publisher: Springer Science and Business Media Deutschland GmbH

Book Volume: 14499 LNCS

Pages Range: 171-185

Conference Proceedings Title: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

Event location: London GB

ISBN: 9783031505232

DOI: 10.1007/978-3-031-50524-9_8

Abstract

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.

Authors with CRIS profile

Merlin Humml Lehrstuhl für Informatik 8 (Theoretische Informatik) Simon Prucker Lehrstuhl für Informatik 8 (Theoretische Informatik) Lutz Schröder Lehrstuhl für Informatik 8 (Theoretische Informatik) Aaron Strahlberger Lehrstuhl für Informatik 8 (Theoretische Informatik)

Involved external institutions

University of Gothenburg / Göteborgs universitet SE Sweden (SE)

How to cite

APA:

Hausmann, D., Humml, M., Prucker, S., Schröder, L., & Strahlberger, A. (2024). Generic Model Checking for Modal Fixpoint Logics in COOL-MC. In Rayna Dimitrova, Ori Lahav, Sebastian Wolff (Eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp. 171-185). London, GB: Springer Science and Business Media Deutschland GmbH.

MLA:

Hausmann, Daniel, et al. "Generic Model Checking for Modal Fixpoint Logics in COOL-MC." Proceedings of the 25th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2024 was co-located with 51st ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2024, London Ed. Rayna Dimitrova, Ori Lahav, Sebastian Wolff, Springer Science and Business Media Deutschland GmbH, 2024. 171-185.

BibTeX: Download