## On the Universal and Existential Fragments of the Mu-Calculus

*
Thomas A. Henzinger,
Orna Kupferman, and Rupak Majumdar*

One source of complexity in the mu-calculus is its ability to specify
an unbounded number of switches between universal (AX) and existential
(EX) branching modes. We therefore study the problems of
satisfiability, validity, model checking, and implication for the
universal and existential fragments of the mu-calculus, in which only
one branching mode is allowed. The universal fragment is rich enough
to express most specifications of interest, and therefore improved
algorithms are of practical importance. We show that while the
satisfiability and validity problems become indeed simpler for the
existential and universal fragments, this is, unfortunately, not the
case for model checking and implication. We also show the
corresponding results for the alternation-free fragment of the
mu-calculus, where no alternations between least and greatest fixed
points are allowed. Our results imply that efforts to find a
polynomial-time model-checking algorithm for the mu-calculus can be
replaced by efforts to find such an algorithm for the universal or
existential fragment.

*Theoretical Computer Science* 354:173-186, 2006.
A preliminary version appeared in the
*Proceedings of the
Ninth International Conference on Tools and Algorithms for the
Construction and Analysis of Systems*
(TACAS),
Lecture Notes in Computer Science 2619,
Springer, 2003, pp. 49-64.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 2003, 2006 Springer.