Game Development Reference
In-Depth Information
set of locations in which no overflow occurred. The following lemma states
the correctness of the construction.
Lemma 6.4 For all game graphs G and priority functions pr, Player 1
is surely-winning in G for the objective Parity( pr ) if and only if Player 1 is
surely-winning in G for the objective Safe(
pr ) .
T
Proof First, let α be a winning strategy for Player 1 in G for the parity
objective Parity( pr ). We construct a strategy α for Player 1 in the game G
and we show that this strategy is surely-winning for the objective Safe(
pr ).
First, without loss of generality we can assume that α is memoryless. We
define α as follows, for all histories π in G , let ( , c )=Last( π ), and we take
α ( π )= α ( ). We show that α is winning for the objective Safe(
T
pr ). Towards
a contradiction, assume that it is not the case. Then there exists a strategy
β of Player 2 such that outcome( G )=( 0 ,c 0 )( 1 ,c 1 ) ... ( n ,c n ) ...
leaves T
T
pr . Let 0 ≤ k 1 <k 2 be such that ( k 2 ,c k 2 ) is the first location where
a counter (say c p ) reaches the value ( p is the odd priority associated with
this counter), and k 1 is the last index where this counter has been reset ( k 1 is
equal to 0 if the counter has never been reset). As c p overflows, we know that
the subsequence ( k 1 ,c k 1 )( k 1 +1 ,c k 1 +1 ) ... ( k 2 ,c k 2 ) visits n p + 1 locations
with priority p . As there are n p locations with priority p in G , we know
that there is at least one location with priority p which is repeating in the
subsequence. Let i 1 and i 2 be the two indexes associated with such a repeating
location. Between i 1 and i 2 , there is no visit to an even priority smaller than
p . Because Player 1 is playing a memoryless strategy in G , Player 2 can spoil
the strategy of Player 1 by repeating his sequence of choices between i 1 and
i 2 . This contradicts our hypothesis that α is a winning strategy in G for the
parity objective Parity( pr ).
Second, let us consider the case where Player 1 is not surely-winning in G
for the objective Parity( pr ). By determinacy, we know tha t Player 2 has a
surely-winning strategy β for the parity objective Parity( pr ). Using a similar
argument as above we can construct a st rat egy β for Player 2 for surely-
winning the reachability objective Reach( T
pr ). By determinacy, this shows
that Player 1 is not surely-winning in G for the objective Safe( T
pr ).
Note that since Buchi and co-Buchi objectives are parity objectives (see
Exercise 6.1), the above reduction to safety games applies and yields a game
G of quadratic size, thus a quadratic-time algorithm for solving Buchi and
co-Buchi games.