Game Development Reference

In-Depth Information

0

1

.

Figure 2.13 A single path through a coding of a positional strategy of

Spoiler

•
Obtain
C
from
A
strat
by omitting the strategy annotation in the labels.

This operation corresponds to a simple projection that removes the Γ

component of the labels. This can be seen as

C

non-deterministically

guessing the strategy for Spoiler.

A
strat
has to check that the plays obtained by

following the thick edges (the strategy of Spoiler) do not satisfy the accep-

tance condition (the strategy is winning for Spoiler). For this task we first

focus on single paths of the tree.

We code these paths by adding to the labels on the path the next direction 0

or 1 taken by the path. In this way we obtain infinite words over Σ

Looking at Figure 2.12,

×

Γ

×{

0
,
1

}

.

This is indicated in Figure 2.13, where a single path from the tree shown in

Figure 2.12 is selected.

Now we construct an
ω
-automaton that checks whether on such paths the

strategy is winning for Spoiler. This
ω
-automaton has to check whether

all plays that can be obtained by following the thick arrows (the strategy of

Spoiler)
along the given path
do not satisfy the acceptance condition of

A

.

We obtain this
ω
-automaton as follows:

•

Construct a non-deterministic Buchi automaton that guesses a play along

the strategy edges of Spoiler and accepts if it does satisfy the acceptance

condition of

A

.

•

Determinise (see Theorem 2.6) and complement this Buchi automaton, and

obtain a deterministic parity word automaton

path

strat
that accepts those

paths of a tree on which Spoiler's strategy is winning.

A

path

strat
in parallel

along all paths of the given tree by merging the transitions of

Now we can run this deterministic parity word automaton

A

path

strat
for the

A

Search Nedrilad ::

Custom Search