Game Development Reference

In-Depth Information

M
is such that if update(
s, o
)=
s
,

above for all
s

∈

M
, and update :
M

×O →

then post
σ
(
s
)

s
for
σ
=
μ
(
s
) (note that such an
s
exists by the above

remark). The automaton
A
defines the observation-based strategy
α
such

that
α
(
π
)=
σ
where
σ
=
μ
(
s
) and
s
= update(
m
I
,
obs(
π
)) for all
π

∩

o

⊆

L
+

(where the update function is extended to sequences of observations in the

usual way, i.e., update(
m, o
1
...o
n
)=update(update(
m, o
1
)
,o
2
...o
n
)).

∈

For reachability games, the information contained in the fixpoint of winning

positions is not su
cient to extract a surely-winning strategy. Intuitively, a

surely-winning strategy needs to stay in the winning set (as in safety games),

and moreover should ensure some kind of progress with respect to the target

set
T
to guarantee that
T
is eventually reached. The notion of progress can

be formalised by a number rank(
s
) associated to each cell
s
such that Player

1 can enforce to reach the target from cell
s
within at most rank(
s
) rounds.

In a reachability game with perfect information, the rank of a location

in the set of winning positions
W
is the least
i
such that

W
i
. From

∈

a location

∈

W
with rank
r>
0, a surely-winning strategy can play an

Σ such that post
σ
(

W
r−
1
.

action
σ
∈

{

}

)

⊆

In a game with imperfect information, knowing the rank of the cells in the

antichain
q
win
may still not be su
cient to obtain a surely-winning strategy.

Consider the game
G
in Figure 6.5, with reachability objective Reach(

{

2
}

)

and observations

{

0
,
1
}

and

{

2
}

. Since Cpre(

{{

2
}}

)=

{{

1
}}

(by playing

action
b
) and Cpre(

{{

1
}

,

{

2
}}

)=

{{

0
,
1
}}

(by playing action
a
), the fixed-

point computed by the antichain algorithm is

{{

2
}

,

{

0
,
1
}}

. However, from

{

0
,
1

}

, after playing
a
, Player 1 reaches the cell

{

1

}

which is not in the

fixed-point (however, it is subsumed by the cell

). Intuitively, the

antichain algorithm has forgotten which action is to be played next from

{

{

0
,
1

}

1

}

. Note that playing
a
again (and thus forever) is not winning.

This example illustrates the fact that the rank of a cell
s
is not necessarily

the same as the rank of a cell
s
⊆ s
. Therefore, for the purpose of strategy

construction, the fixpoint computation needs to store the rank associated

with a cell, and refine the rule of eliminating the cells that are subsumed

by larger cells to take ranks into account (Berwanger et al. [2009]). In fact,

it can be shown that for some family of reachability games with imperfect

information, the fixpoint computed in the antichain representation (without

rank) is of polynomial size while any finite-memory surely-winning strategy

is of exponential size (Berwanger et al. [2008]).

Search Nedrilad ::

Custom Search