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