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.

Search Nedrilad ::

Custom Search