Game Development Reference
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 )
W 0 ←
reach 1 ( T )
reach 0 ( W 0 )
( W 0 ,W 1 )
Buchi-win ( G )
W 1 ,W 1 )
( W 0 ,W 1 )
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
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
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