The Complexity of Enriched $µ$-Calculi

Aus International Center for Computational Logic
Version vom 19. März 2015, 18:44 Uhr von Marcel Lippmann (Diskussion | Beiträge)
(Unterschied) ← Nächstältere Version | Aktuelle Version (Unterschied) | Nächstjüngere Version → (Unterschied)
Wechseln zu:Navigation, Suche

Toggle side column

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
  • 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},
}