Weak Alternating Automata Are Not That Weak
-------------------------------------------
Automata on infinite words are used for specification and verification
of nonterminating programs. Different types of automata induce
different levels of expressive power, of succinctness, and of
complexity. Alternating automata have both existential and
universal branching modes and are particularly suitable for
specification of programs.
In a weak alternating automaton, the state space is partitioned
into partially ordered sets, and the automaton can proceed from a
certain set only to smaller sets. Reasoning about weak alternating
automata is easier than reasoning about alternating automata with no
restricted structure. Known translations of alternating automata to
weak alternating automata involve determinization, and therefore
involve a double-exponential blow-up.
In this paper we describe a quadratic translation, which circumvents
the need for determinization, of Buchi and co-Buchi alternating
automata to weak alternating automata. Beyond the independent interest
of such a translation, it gives rise to a simple complementation
algorithm for nondeterministic Buchi automata.