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.

Search Nedrilad ::

Custom Search