Game Development Reference
two directions 0 and 1 into a single transition of a tree automaton as follows:
δ ( q, ( a, γ, 0)) = q
δ ( q, ( a, γ, 1)) = q
( q, ( a, γ ) ,q ,q )
A strat :
for all q
Q , a
Σ, and γ
is obtained by omitting the strategy encoding:
( q, ( a, γ ) ,q ,q ) becomes ( q, a, q ,q ) .
From the explanations above it follows that
indeed accepts the complement
, resulting in the following theorem.
Theorem 2.16 (Rabin ) For a given tree automaton one can con-
struct a tree automaton for the complement language.
The main steps of the construction described in this section are summarised
Characterise acceptance in terms of winning strategies in the membership
Positional determinacy for parity games yields: a tree t is not accepted iff
Spoiler has a positional winning strategy in the membership game.
Construct an automaton that checks if a given strategy of Spoiler is
winning. This construction is based on the determinisation of ω -automata.
Obtain the desired automaton by projection (removing the strategy anno-
This proof scheme was proposed by Gurevich and Harrington  (see also
Thomas ). It is a nice illustration of how determinacy of infinite games
can help to solve problems in automata theory. Note that the positional
determinacy or winning strategies are not used inside the construction
but only to prove the correctness of the construction. The main step in
the construction itself is the use of the determinisation theorem for Buchi
In Muller and Schupp  a different proof is presented that only
relies on the determinacy of the membership game without making any
assumptions on the type of the strategies. From the construction one can
derive a finite memory determinacy result for game graphs that have the
shape of a membership game.
The size of the complement automaton is determined by the complexity
of the determinisation construction for word automata. If
is a PTA with
n states and k priorities, then the Buchi word automaton that has to be