The Complexity of Enriched $µ$-Calculi
Aus International Center for Computational Logic
The Complexity of Enriched $µ$-Calculi
P. BonattiP. Bonatti, C. LutzC. Lutz, A. MuranoA. Murano, M. VardiM. Vardi
P. Bonatti, C. 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
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
- KurzfassungAbstract
The fully enriched mu-calculus is the extension of thepropositional 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
@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},
}