\Pi_2 \cap \Sigma_2 = AFMC
==========================

The $\mu$-calculus is an expressive specification language in which
modal logic is extended with fixpoint operators, subsuming many
dynamic, temporal, and description logics.  Formulas of $\mu$-calculus
are classified according to their alternation depth, which is the
maximal length of a chain of nested alternating least and greatest
fixpoint operators.  Alternation depth is the major factor in the
complexity of $\mu$-calculus model-checking algorithms. A refined
classification of $\mu$-calculus formulas distinguishes between
formulas in which the outermost fixpoint operator in the nested chain
is a least fixpoint operator ($\Sigma_i$ formulas, where $i$ is the
alternation depth) and formulas where it is a greatest fixpoint
operator ($\Pi_i$ formulas).  The alternation-free $\mu$-calculus
(AFMC) consists of $\mu$-calculus formulas with no alternation between
least and greatest fixpoint operators. Thus, AFMC is a natural closure
of $\Sigma_1 \cup \Pi_1$, which is contained in both $\Sigma_2$ and
$\Pi_2$.  In this work we show that $\Sigma_2 \cap \Pi_2 \equiv$ AFMC.
In other words, if we can express a property $\xi$ both as a least
fixpoint nested inside a greatest fixpoint and as a greatest fixpoint
nested inside a least fixpoint, then we can express $\xi$ also with no
alternation between greatest and least fixpoints.  Our result refers
to $\mu$-calculus over arbitrary Kripke structures.  A similar result,
for directed $\mu$-calculus formulas interpreted over trees with a
fixed finite branching degree, follows from results by Arnold and
Niwinski. Their proofs there cannot be easily extended to Kripke
structures, and our extension involves symmetric nondeterministic
Buchi tree automata, and new constructions for them.