A Measured Collapse of The Modal \mu-Calculus Alternation Hierarchy
=====================================================================

The \mu-calculus model-checking problem has been of great interest in
the context of concurrent programs. Beyond the need to use symbolic
methods in order to cope with the state-explosion problem, which is
acute in concurrent settings, several concurrency related problems are
naturally solved by evaluation of \mu-calculus formulas. The
complexity of a naive algorithm for model checking a \mu-calculus
formula f is exponential in the alternation depth d of f. Recent
studies of the \mu-calculus and the related area of parity games have
led to algorithms exponential only in d/2. No symbolic version,
however, is known for the improved algorithms, sacrificing the main
practical attraction of the \mu-calculus.

The \mu-calculus can be viewed as a fragment of first-order fixpoint
logic. One of the most fundamental theorems in the theory of fixpoint
logic is the Collapse Theorem, which asserts that, unlike the case for
the \mu-calculus, the fixpoint alternation hierarchy over finite
structures collapses at its first level; that is, every formula in
fixpoint logic can be expressed as a least-fixpoint formula. In this
paper we show that the Collapse Theorem of fixpoint logic holds for a
measured variant of the \mu-calculus, which we call \mu^#-calculus.
While \mu-calculus formulas represent characteristic functions, i.e.,
functions from the state space to {0,1}, formulas of the
\mu^#-calculus represent measure functions, which are functions from
the state space to some measure domain.  We prove a Measured-Collapse
Theorem: every formula in the \mu-calculus is equivalent to a
least-fixpoint formula in the \mu^#-calculus. We show that the
Measured-Collapse Theorem provides a logical recasting of the improved
algorithm for \mu-calculus model-checking, and describe how it can be
implemented symbolically using Algebraic Decision Diagrams. Thus, we
describe, for the first time, a symbolic \mu-calculus model-checking
algorithm whose complexity matches the one of the best known
enumerative algorithm.