EXPTIME Tableaux for the Coalgebraic mu-Calculus

TL;DR

This paper introduces the coalgebraic mu-calculus, extending the coalgebraic modal logic framework with fixpoint operators, and proves its EXPTIME decidability and tableau completeness, with applications to probabilistic and coalition logics.

Contribution

It develops the coalgebraic mu-calculus, providing a uniform framework for various modal logics with fixpoints, and establishes complexity bounds and tableau completeness results.

Findings

Decidability of the coalgebraic mu-calculus in EXPTIME

Completeness of the tableau calculus for the logic

Application to probabilistic mu-calculus and coalition logic

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.