THE COMPLEXITY OF ENRICHED µ-CALCULI
Piero A. Bonatti, Carsten Lutz, Aniello Murano, Moshe Y. Vardi · 2006
The fully enriched µ-calculus is the extension of the propositional µ-calculus with inverse programs, graded modalities, and nominals. While satisfiability in several expressive fragments of the fully enriched µ-calculus is known to be decidable and EXPTIME-complete, it has recently been proved that the full calculus is undecidable. In this paper, we study the fragments of the fully enriched µ-calculus that are obtained by dropping at least one of the additional constructs. We show that, in all fragments obtained in this way, satisfiability is decidable and EXPTIME-complete. Thus, we identify a family of decidable logics that are maximal (and incomparable) in expressive power. Our results are obtained by introducing two new automata models, showing that their emptiness problems are EXPTIME-complete, and then reducing satisfiability in the relevant logics to these problems. The automata models we introduce are two-way graded alternating parity automata over infinite trees (2GAPTs) and fully enriched automata (FEAs) over infinite forests. The former are a common generalization of two incomparable automata models from the literature. The latter extend alternating automata in a similar way as the fully enriched µ-calculus extends the standard µ-calculus.