COOL 2 – A Generic Reasoner for Modal Fixpoint Logics (System Description)

Görlitz O, Hausmann D, Humml M, Pattinson D, Prucker S, Schröder L (2023)

Publication Type: Conference contribution

Publication year: 2023

Journal

Lecture Notes in Computer Science Springer Verlag

Publisher: Springer Science and Business Media Deutschland GmbH

Book Volume: 14132 LNAI

Pages Range: 234-247

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

Event location: Rome IT

ISBN: 9783031384981

DOI: 10.1007/978-3-031-38499-8_14

Abstract

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.

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)

Involved external institutions

University of Gothenburg / Göteborgs universitet SE Sweden (SE) Australian National University (ANU) AU Australia (AU)

How to cite

APA:

Görlitz, O., Hausmann, D., Humml, M., Pattinson, D., Prucker, S., & Schröder, L. (2023). COOL 2 – A Generic Reasoner for Modal Fixpoint Logics (System Description). In Brigitte Pientka, Cesare Tinelli (Eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp. 234-247). Rome, IT: Springer Science and Business Media Deutschland GmbH.

MLA:

Görlitz, Oliver, et al. "COOL 2 – A Generic Reasoner for Modal Fixpoint Logics (System Description)." Proceedings of the Proceedings of the 29th International Conference on Automated Deduction, CADE-29, Rome Ed. Brigitte Pientka, Cesare Tinelli, Springer Science and Business Media Deutschland GmbH, 2023. 234-247.

BibTeX: Download