EXPTIME Tableaux for the Coalgebraic mu-Calculus

Corina Cirstea; Clemens Kupke; Dirk Pattinson

doi:10.2168/LMCS-7(3:3)2011

Corina Cirstea ; Clemens Kupke ; Dirk Pattinson - EXPTIME Tableaux for the Coalgebraic mu-Calculus

lmcs:784 - Logical Methods in Computer Science, August 11, 2011, Volume 7, Issue 3 - https://doi.org/10.2168/LMCS-7(3:3)2011

EXPTIME Tableaux for the Coalgebraic mu-CalculusArticle

Authors: Corina Cirstea ; Clemens Kupke ; Dirk Pattinson

The coalgebraic approach to modal logic provides a uniform framework that captures the semantics of a large class of structurally different modal logics, including e.g. graded and probabilistic modal logics and coalition logic. In this paper, we introduce the coalgebraic mu-calculus, an extension of the general (coalgebraic) framework with fixpoint operators. Our main results are completeness of the associated tableau calculus and EXPTIME decidability for guarded formulas. Technically, this is achieved by reducing satisfiability to the existence of non-wellfounded tableaux, which is in turn equivalent to the existence of winning strategies in parity games. Our results are parametric in the underlying class of models and yield, as concrete applications, previously unknown complexity bounds for the probabilistic mu-calculus and for an extension of coalition logic with fixpoints.

https://doi.org/10.2168/LMCS-7(3:3)2011

Source: arXiv.org:1105.2246

Volume: Volume 7, Issue 3

Secondary volumes: Selected Papers of the 23rd International Workshop on Computer Science Logic and the 18th Annual Conference of the EACSL (CSL 2009)

Published on: August 11, 2011

Imported on: April 26, 2010

Keywords: Computer Science - Logic in Computer Science, Mathematics - Logic, F.4.1, F.3.1, F.1.1

Licence: arXiv.org - Non-exclusive license to distribute

Funding:

Source : OpenAIRE Graph

Coalgebraic Modal Logic: Fixpoints and Nested Modalities; Funder: UK Research and Innovation; Code: EP/F031173/1

Classifications

Mathematics Subject Classification 2020¹

Sources:

[1] zbMATH Open.

Bibliographic References

16 Documents citing this article

Ezra Schoen;Clemens Kupke;Jurriaan Rot;Ruben Turkenburg, 2024, A Categorical Approach to Coalgebraic Fixpoint Logic, Radboud Repository (Radboud University), pp. 23-43, 10.1007/978-3-031-66438-0_2, https://hdl.handle.net/2066/311036.

Daniel Hausmann;Merlin Humml;Simon Prucker;Lutz Schröder;Aaron Strahlberger, 2023, Generic Model Checking for Modal Fixpoint Logics in COOL-MC, Lecture notes in computer science, pp. 171-185, 10.1007/978-3-031-50524-9_8.

Oliver Görlitz;Daniel Hausmann;Merlin Humml;Dirk Pattinson;Simon Prucker;Lutz Schröder, 2023, COOL 2 – A Generic Reasoner for Modal Fixpoint Logics (System Description), Lecture notes in computer science, pp. 234-247, 10.1007/978-3-031-38499-8_14, https://doi.org/10.1007/978-3-031-38499-8_14.

Sebastian Enqvist;Valentin Goranko, 2022, The Temporal Logic of Coalitional Goal Assignments in Concurrent Multiplayer Games, ACM Transactions on Computational Logic, 23, 4, pp. 1-58, 10.1145/3517128, https://doi.org/10.1145/3517128.

Daniel Hausmann;Lutz Schröder, 2021, Quasipolynomial Computation of Nested Fixpoints, Lecture notes in computer science, pp. 38-56, 10.1007/978-3-030-72016-2_3, https://doi.org/10.1007/978-3-030-72016-2_3.

Göttlinger, Merlin;Schröder, Lutz;Pattinson, Dirk, 2021, The Alternating-Time μ-Calculus With Disjunctive Explicit Strategies, DROPS (Schloss Dagstuhl – Leibniz Center for Informatics), 10.4230/lipics.csl.2021.26, https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.26.

Daniel Hausmann;Lutz Schröder, 2020, NP Reasoning in the Monotone $$\mu $$-Calculus, arXiv (Cornell University), pp. 482-499, 10.1007/978-3-030-51074-9_28, http://arxiv.org/abs/2002.05075.

Daniel Hausmann;Lutz Schröder, 2019, Optimal Satisfiability Checking for Arithmetic $$\mu $$-Calculi, Lecture notes in computer science, pp. 277-294, 10.1007/978-3-030-17127-8_16, https://doi.org/10.1007/978-3-030-17127-8_16.

Sebastian Enqvist;Helle Hvid Hansen;Clemens Kupke;Johannes Marti;Yde Venema, 2019, Completeness for Game Logic, UvA-DARE (University of Amsterdam), 10.1109/lics.2019.8785676.

Clemens Kupke, 2018, Coalgebraic Logics & Duality, pp. 6-12, 10.1007/978-3-030-00389-0_2, https://inria.hal.science/hal-02044643.

Lutz Schröder;Yde Venema, 2018, Completeness of Flat Coalgebraic Fixpoint Logics, ACM Transactions on Computational Logic, 19, 1, pp. 1-34, 10.1145/3157055.

Valentin Goranko;Antti Kuusisto;Raine Rönnholm, 2017, Game-Theoretic Semantics for ATL+ with Applications to Model Checking, arXiv (Cornell University), 276, pp. 104554, 10.1016/j.ic.2020.104554, http://arxiv.org/abs/1702.08405.

Ichiro Hasuo;Shunsuke Shimizu;Corina Cîrstea, 2016, Lattice-theoretic progress measures and coalgebraic model checking, ACM SIGPLAN Notices, 51, 1, pp. 718-732, 10.1145/2914770.2837673.

Valentin Goranko;Antti Kuusisto;Raine Rönnholm, 2016, Game-Theoretic Semantics for Alternating-Time Temporal Logic, arXiv (Cornell University), 19, 3, pp. 1-38, 10.1145/3179998, http://arxiv.org/abs/1602.07667.

Daniel Marsden, 2013, Coalgebras with Symmetries and Modelling Quantum Systems, Lecture notes in computer science, pp. 205-219, 10.1007/978-3-642-40206-7_16.

Oliver Friedmann;Martin Lange, 2010, A Solver for Modal Fixpoint Logics, Electronic Notes in Theoretical Computer Science, 262, pp. 99-111, 10.1016/j.entcs.2010.04.008, https://doi.org/10.1016/j.entcs.2010.04.008.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 3809 times.

This article's PDF has been downloaded 703 times.