The Weakness of Self-Complementation
====================================

Model checking is a method for the verification of systems with
respect to their specifications.  Symbolic model-checking, which
enables the verification of large systems, proceeds by evaluating
fixed-point expressions over the system's set of states. Such
evaluation is particularly simple and efficient when the expressions
do not contain alternation between least and greatest fixed-point
operators; namely, when they belong to the alternation-free
\mu-calculus (AFMC). Not all specifications, however, can be
translated to AFMC, which is exactly as expressive as weak monadic
second-order logic (WS2S). Rabin showed that a set T of trees can be
expressed in WS2S if and only if both T and its complement can be
recognized by nondeterministic B\"uchi tree automata. For the "only
if" direction, Rabin constructed, given two nondeterministic Buchi
tree automata U and U' that recognize T and its complement, a WS2S
formula that is satisfied by exactly all trees in T. Since the
translation of WS2S to AFMC is nonelementary, this construction is not
practical. Arnold and Niwinski improved Rabin's construction by a
direct translation of U and U' to AFMC, which involves a
doubly-exponential blow-up and is therefore still impractical. In this
paper we describe an alternative and quadratic translation of U and U'
to AFMC. Our translation goes through weak alternating tree automata,
and constitutes a step towards efficient symbolic model checking of
highly expressive specification formalisms.