Game Development Reference
In-Depth Information
a
a
a
( q 1 ,a,q 2 ,q + )
0
a
a
a
b
1
0
( q 2 ,a,q 1 ,q 1
)
a
a
a a
a a
a a
( q + ,a,q + ,q + )
.
0 , 1
a
b
1
0 , 1
( q 1 ,b,q + ,q + )
a a
Figure 2.15 A finitely generated (regular) tree corresponding to the winning
strategy depicted in Figure 2.14
unique transition to use. At the root we choose the transition associated to
the initial state of
. For a given transition Spoiler can choose the left or
the right state. At the corresponding next node in the tree we choose the
transition associated to this state. A compact representation of the resulting
tree is shown on the left-hand side of Figure 2.15. Each transition has two
outgoing edges, one labelled 0 for moving to the left successor in the tree, and
one labelled 1 for moving to the right successor. The transition associated to
the initial state of
A
is marked with the small incoming arrow. This graph
can be seen as a finite automaton that reads names of tree nodes (words over
{ 0 , 1 } ) and outputs the transitions to be used in the run on the accepted
tree. If we only output the label used in the transition, then we obtain the
tree itself, which is shown on the right-hand side of Figure 2.15. It is labelled
a everywhere except every second step to the right from the leftmost path.
Trees that are labelled in a regular way in the sense explained above are
called regular trees .
A
Theorem 2.19 (Rabin [1969]) The emptiness problem for parity tree
automata is decidable. If the language is not empty, then one can construct
a finite representation of a tree in the language.
Using the translation from S2S to tree automata we obtain the decidability
of the theory S2S, or more generally the decidability of the satisfiability for
S2S formulae.
Corollary 2.20 (Rabin [1969])
The satisfiability problem for S2S formulae
is decidable.