Game Development Reference
q in ( q in ,b,q 1 ,q 2 ) ∈ Δ
q 2 ( q 2 ,b,q 5 ,q 6 ) ∈ Δ
( q 1 ,a,q 3 ,q 4 ) ∈ Δ
Figure 2.10 A run of a PTA has to respect the transition relation
} ∗ . This is
the transitions, ( ρ ( u ) ,t ( u ) ,ρ ( u 0) ,ρ ( u 1))
Δ for all u
0 , 1
illustrated in Figure 2.10.
The acceptance condition of a PTA is defined via the priority mapping.
From games and ω -automata we already know that a sequence of states is
accepting if the maximal priority that appears infinitely often is even. We
extend this to trees by defining a run to be accepting if the state sequence
on each infinite path through the run is accepting, i.e., if on each infinite
path the maximal priority that occurs infinitely often is even.
As usual, a tree is accepted if there is an accepting run on this tree. The
language of trees accepted by
). We call a language of
infinite trees regular if it can be accepted by a parity tree automaton.
Before we come to the properties of PTAs, we make some remarks on other
acceptance conditions and give some examples:
is denoted by T (
• As for games or ω -automata we can define, e.g., tree automata with Muller
or Buchi acceptance conditions.
The expressive power of Muller tree automata and parity tree automata is
the same. To transform Muller automata into parity automata one can
use the LAR construction presented in the previous section.
One can show that Buchi tree automata are weaker than parity tree
automata. The language of all trees over
such that on each path
there are finitely many b cannot be accepted by a Buchi tree automaton
but by a PTA. The PTA can easily be obtained by running the parity
word automaton from Figure 2.5 on every branch of the tree using the
transitions ( q 0 ,a,q 0 ,q 0 ), ( q 0 ,b,q 1 ,q 1 ), ( q 1 ,a,q 0 ,q 0 ), and ( q 1 ,b,q 1 ,q 1 ). A
proof that a Buchi tree automaton cannot accept this language can be
found in Thomas  and in Chapter 8 of Gradel et al. .
It is rather easy to see that deterministic tree automata are too weak. For
example, the set of all trees t over
such that t contains at least one