TY - GEN
T1 - EXPTIME tableaux for the coalgebraic μ-calculus
AU - Cîrstea, Corina
AU - Kupke, Clemens
AU - Pattinson, Dirk
PY - 2009
Y1 - 2009
N2 - 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 μ-calculus, an extension of the general (coalgebraic) framework with fixpoint operators. Our main results are completeness of the associated tableau calculus and EXPTIME decidability. 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 μ-calculus and for an extension of coalition logic with fixpoints.
AB - 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 μ-calculus, an extension of the general (coalgebraic) framework with fixpoint operators. Our main results are completeness of the associated tableau calculus and EXPTIME decidability. 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 μ-calculus and for an extension of coalition logic with fixpoints.
UR - http://www.scopus.com/inward/record.url?scp=70350355242&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-04027-6_15
DO - 10.1007/978-3-642-04027-6_15
M3 - Conference contribution
SN - 3642040268
SN - 9783642040269
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 179
EP - 193
BT - Computer Science Logic - 23rd International Workshop, CSL 2009 - 18th Annual Conference of the EACSL, Proceedings
T2 - 23rd International Workshop on Computer Science Logic, CSL 2009 - 18th Annual Conference of the EACSL
Y2 - 7 September 2009 through 11 September 2009
ER -