Complexity of the Coalgebraic µ-calculus

The extension of a modal logic with fixpoints in many cases increases the complexity of the decision problem from PSPACE to EXPTIME. Here, we give a general and formal account of this observation on the basis of coalgebraic logics that provide a uniform semantic umbrella for a wide range of typically non-normal modal logics. We establish that – under mild conditions that are satisfied for a large number of examples – the µ-calculus associated with a modal logic is decidable in EXPTIME. This is established by providing a general tableau-calculus that reduces the satisfiability problem to the existence of winning strategies in parity games. By instantiating these results with concrete examples, we not only obtain the known EXPTIME bounds for the modal and the graded µ-calculus, but also new complexity bounds for the extension of probabilistic and monotone modal logic and coalition logic with fixpoint operators. 2 Syntax & Semantics We fix a modal similarity type Λ, that is, a set Λ of modal operators with associated arities, and a denu-merable set V of propositional variables. Throughout, we will deal with formulas in negation normal form only and abbreviate Λ = { ♥ | ♥ ∈ Λ} and similarly V = {p | p ∈ V}. The arity of ♥ ∈ Λ is the same as that of ♥. The set F(Λ) of Λ-formulas is given by the grammar A,B:: = x | A ∨B | A ∧B | ♥(A1,..., An) | µp.A | νp.