The satisfiability problem of the modal mu-calculus is decidable in exponential time.
This well-known fact can be proven using (possibly) non-wellfounded tableaux.
In my talk I will demonstrate how the tableaux-based proof can be generalised to
a proof of ExpTime-decidability of a family of coalgebraic fixpoint logics, ie., coalgebraic logics extended with least and greatest fixpoint operators.
Our decidability result yields, as concrete applications,
previously unknown complexity bounds for the probabilistic
mu-calculus and for an extension of coalition logic with fixpoints.
This is joint work with Corina Cirstea and Dirk Pattinson