The Complexity of Enriched µ-Calculi

P. BonattiP. Bonatti, Carsten LutzCarsten Lutz, A. MuranoA. Murano, M. VardiM. Vardi

Download

P. Bonatti, Carsten Lutz, A. Murano, M. Vardi
The Complexity of Enriched µ-Calculi
In Michele Bugliesi and Bart Preneel and Vladimiro Sassone and Ingo Wegener, eds., Proccedings of the 33rd International Colloquium on Automata, Languages and Programming, Part II (ICALP'06), volume 4052 of Lecture Notes in Computer Science, 540-551, 2006. Springer

Details
Bibtex

KurzfassungAbstract
The fully enriched mu-calculus is the extension of the propositional mu-calculus with inverse programs, graded modalities, and nominals. While satisfiability in several expressive fragments of the fully enriched mu-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 mu-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 emptyness problems are ExpTime-complete, and then reducing satisfiability in the relevant logics to this problem. The automata models we introduce are two-way graded alternating parity automata over infinite trees (2GAPT) and fully enriched automata (FEA) 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 mu-calculus extends the standard mu-calculus.
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

The final publication is available at Springer.

@inproceedings{ BoLuMuVa-ICALP06,
  author = {P. {Bonatti} and C. {Lutz} and A. {Murano} and M. {Vardi}},
  booktitle = {Proccedings of the 33rd International Colloquium on Automata, Languages and Programming, Part {II} ({ICALP'06})},
  editor = {Michele {Bugliesi} and Bart {Preneel} and Vladimiro {Sassone} and Ingo {Wegener}},
  pages = {540--551},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  title = {The Complexity of Enriched $\mu$-Calculi},
  volume = {4052},
  year = {2006},
}