Game Development Reference

In-Depth Information

graphs, that for every vertex maintains the number of outgoing edges, to

achieve this running time bound.

Theorem 3.2
Reachability and safety games are positionally determined.

The winning sets and positional winning strategies of both players can be

computed in time O
(
m
)
.

In Figure 3.1 we present a divide-and-conquer algorithm for solving re-

peated reachability, and hence also for eventual safety, games. The algorithm

takes a repeated reachability game
G
with the target set
T
as input, and it

returns the pair (
win
0
(
G
)
, win
1
(
G
)) of the winning sets of both players. The

main insight behind the design of this algorithm is that the solution of a

repeated reachability game can be obtained from the solution of a subgame

that is also a repeated reachability game, and that has fewer vertices.

algorithm
Buchi-win
(
G
)

if
reach
1
(
T
)=
V

then
(
W
0
,W
1
)

←

(

∅

,V
)

else

W
0
←

V

\

reach
1
(
T
)

G
←

reach
0
(
W
0
)

G

\

(
W
0
,W
1
)

Buchi-win
(
G
)

←

W
1
,W
1
)

(
W
0
,W
1
)

←

(
V

\

endif

return
(
W
0
,W
1
)

Figure 3.1 A divide-and-conquer algorithm for repeated reachability and

eventual safety games

In a series of exercises we provide the detailed structure of an inductive

correctness proof for the algorithm, and we invite the reader to fill in the

details.

Exercise 3.4
Assume that
reach
1
(
T
)=
V
. Argue that if player 1 follows

a positional
T
-reachability strategy from an arbitrary starting vertex
v

V
,

then a vertex in
T
occurs infinitely many times. Conclude that in this case

win
1
(
G
)=
V
.

∈

V
is a
0-dominion
if it is 1-closed and player 0

has a
D
-trapping strategy that is winning for her from every starting vertex

in
D
; the latter is called a
0-dominion strategy
on
D
. The definitions of

a
1-dominion
and a
1-dominion strategy
are analogous.

We say that a set
D

⊆

Search Nedrilad ::

Custom Search