Weak alternating automata and tree automata emptiness
-----------------------------------------------------

Automata on infinite words and trees are used for specification and
verification of nonterminating programs.  The verification and
the satisfiability problems of specifications can be reduced to the
nonemptiness problem of such automata.   
In a weak 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 automata is easier than reasoning
about automata with no restricted structure.  
In particular, the nonemptiness problem for weak alternating automata
over a singleton alphabet can be solved in linear time.   
Known translations of alternating automata to weak alternating
automata involve determinization, and therefore involve a double
exponential blow-up.  
In this paper we describe simple and efficient translations, which
circumvent the need for determinization, of parity and Rabin
alternating word automata to weak alternating word automata. Beyond
the independent interest of such translations, they give rise to a
simple algorithm for deciding the nonemptiness of nondeterministic
parity and Rabin tree automata. In particular, our algorithm for Rabin
automata runs in time $O(n^{2k+1} \cdot k!)$, where $n$ is the number
of states in the automaton and $k$ is the number of pairs in the
acceptance condition. This improves the known $O((nk)^{3k})$ bound for
the problem.