On the Universal and Existential Fragments of the $\mu$-Calculus
================================================================
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 switches 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 the
existential fragments.