EXPTIME tableaux for the coalgebraic -calculus

DOI10.2168/LMCS-7(3:3)2011MaRDI QIDQ3224669zbMATH OpenOpenAlexFDO

Authors Clemens Kupke, Dirk Pattinson, Corina Cîrstea

Publication date 2 April 2012

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1105.2246

zbMATH Keywords

\(\mu\)-calculuscoalgebramodal logictableau-based decision procedures

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Modal logic (including the logic of norms) (03B45) Logic in computer science (03B70) Categorical logic, topoi (03G30) Applications of game theory (91A80)

Abstract: 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.

Recommendations

• EXPTIME Tableaux for the Coalgebraic μ-Calculus
• The modal -calculus caught off guard
• Completeness for \(\mu\)-calculi: a coalgebraic approach
• Completeness for coalgebraic fixpoint logic

Cited in

(18)

• Coalgebraic logics \& duality
• Predicate liftings and functor presentations in coalgebraic expression languages
• Quasipolynomial computation of nested fixpoints
• NP reasoning in the monotone \(\mu\)-calculus
• Optimal satisfiability checking for arithmetic \(\mu\)-calculi
• The modal -calculus caught off guard
• EXPTIME Tableaux for the Coalgebraic μ-Calculus
• Deciding the unguarded modal \(\mu\)-calculus
• Subsumption checking in conjunctive coalgebraic fixpoint logics
• A coalgebraic take on regular and -regular behaviours
• The Temporal Logic of Coalitional Goal Assignments in Concurrent Multiplayer Games
• Game-based local model checking for the coalgebraic \(\mu\)-calculus
• COOL 2 – A Generic Reasoner for Modal Fixpoint Logics (System Description)
• Linear-time logics -- a coalgebraic perspective
• Coalgebraic satisfiability checking for arithmetic -calculi
• A categorical approach to coalgebraic fixpoint logic
• The alternating-time -calculus with disjunctive explicit strategies
• Identity-preserving Lax extensions and where to find them

This page was built for publication: EXPTIME tableaux for the coalgebraic \(\mu\)-calculus

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3224669)