Bonatti, Piero A. and Lutz, Carsten and Murano, Aniello and Vardi, Moshe Y. - The Complexity of Enriched Mu-Calculi

lmcs:993 - Logical Methods in Computer Science, September 22, 2008, Volume 4, Issue 3
The Complexity of Enriched Mu-Calculi

Authors: Bonatti, Piero A. and Lutz, Carsten and Murano, Aniello and Vardi, Moshe Y.

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.


Source : oai:arXiv.org:0809.0360
DOI : 10.2168/LMCS-4(3:11)2008
Volume: Volume 4, Issue 3
Published on: September 22, 2008
Submitted on: January 7, 2007
Keywords: Computer Science - Logic in Computer Science,Computer Science - Computation and Language,F.3.1,F.4.1


Share

Consultation statistics

This page has been seen 87 times.
This article's PDF has been downloaded 42 times.