Alternation Removal in Buchi Automata
=====================================

Alternating automata play a key role in the automata-theoretic
approach to specification, verification, and synthesis of reactive
systems. Many algorithms on alternating automata, and in particular,
their nonemptiness test, involve removal of alternation: a translation
of the alternating automaton to an equivalent nondeterministic one.
For alternating Buchi automata, the best known translation uses the
"breakpoint construction" and involves an O(3^n) state blow-up. The
translation was described by Miyano and Hayashi in 1984, and is widely
used since, in both theory and practice. Yet, the best known lower
bound is only 2^n.

In this paper we develop and present a complete picture of the problem
of alternation removal in alternating Buchi automata. In the lower
bound front, we show that the breakpoint construction captures the
accurate essence of alternation removal, and provide a matching
\Omega(3^n) lower bound. Our lower bound holds already for universal
(rather than alternating) automata with an alphabet of a constant
size.  In the upper-bound front, we point to a class of alternating
Buchi automata for which the breakpoint construction can be replaced
by a simpler n2^n construction.  Our class, of ordered alternating
Buchi automata, strictly contains the class of very-weak alternating
automata, for which an n2^n construction is known.