Game Development Reference
= V , i.e., that W 0
. Observe that
the set W 0 is 1-closed and that if player 0 follows a positional W 0 -trapping
strategy μ from a vertex in W 0 then no vertex in T is ever reached.
Argue that the set reach 0 ( W 0 ) is 1-closed, and that a positional strategy μ
that is the union of strategy μ (on W 0 ) and a W 0 -reachability strategy
(on reach 0 ( W 0 )
Assume that reach 1 ( T )
W 0 )isa reach 0 ( W 0 )-trapping strategy. Prove that if player 0
follows strategy μ from a starting vertex in reach 0 ( W 0 ) then vertices in T
occur only finitely many times.
Conclude that reach 0 ( W 0 )
win 0 ( G ), that sets W 0 and reach 0 ( W 0 ) are
0-dominions, and that μ and μ are 0-dominion strategies.
reach 0 ( W 0 ) be a repeated reachability game that is obtained
from game G by removing vertices in the set reach 0 ( W 0 ) and edges adjacent
to them. Assume that the game G is positionally determined, and that
there are positional 0-dominion and 1-dominion strategies μ and χ on the
winning sets W 0 = win 0 ( G ) and W 1 = win 1 ( G ) respectively, in game G .
Let G = G
Exercise 3.6 Observe that positional determinacy of game G implies that
reach 0 ( W 0 ) ∪ W 0 = V \ W 1 . Prove that the positional strategy that is the
union of μ and μ is a 0-dominion strategy on V \ W 1 in game G . Conclude
that V \ W 1 ⊆ win 0 ( G ).
Prove that χ is a 1-dominion strategy on W 1 in game G . Conclude that
W 1 ⊆ win 1 ( G ), that repeated reachability and eventual safety games are
positionally determined, and that the algorithm Buchi-win ( G ) is correct.
Theorem 3.3 Repeated reachability and eventual safety games are posi-
Note that the algorithm Buchi-win ( G ) solves two reachability games, and it
makes one recursive call on a repeated reachability game G = G
reach 0 ( W 0 )
whose number of vertices is strictly smaller than that of G . It follows that
its worst-case running time can be characterised by the recurrence:
T ( n ) ≤ T ( n − 1) + O ( m ) ,
T (1) = O (1) ,
where n =
are the numbers of vertices and edges, respectively,
of the game graph, and hence T ( n )= O ( nm ).
and m =
Theorem 3.4 The winning sets and positional winning strategies of both
players in repeated reachability and eventual safety games can be computed
in time O ( nm ) .