Game Development Reference
In-Depth Information
a, b
a
{ 2 , 2 }, 2
{ 3 , 3 }, 3
a, b
b
a, b
{ 1 }, 1
a, b
b
a, b
{ 2 , 2 }, 2
{ 3 , 3 }, 3
{ 4 }, 4
a
Figure 6.7 Game structure H = Knw( G ) (for G of Figure 6.2)
probability, while ensuring that W is not left, even if the current state is
q
q (because if the game is actually in q , then it means that Player 1
cannot be sure that the game is not in q with some positive probability).
Note that for W = Q , the condition post σ ( q )
W is trivial. Hence,
for W 0 = Q the set W 1 = PosReach( W 0 ) contains all states from which
Player 1 can enforce to reach
with positive probability. Clearly, this set
is an over-approximation of the almost-surely-winning states, since from
Q
T
W 1
is
reached is 0. Therefore, we compute in W 2 = PosReach( W 1 ) the set of states
from which Player 1 can enforce to reach
\
and no matter the strategy of Player 1, the probability that
T
with positive probability without
leaving W 1 , giving a better over-approximation of the set of almost-surely-
winning states. The iteration continues until a fixpoint is obtained. Note that
W 0
T
W 1
W 2
is a decreasing sequence, and X 0
X 1
X 2
is
an increasing sequence for each computation of PosReach( W i ). This algorithm
is thus quadratic in the size of H , and exponential in the size of G .
⊇···
⊆···
Theorem 6.9 The problem of deciding whether Player 1 is almost-surely-
winning in a reachability game with imperfect information is EXPTIME-
complete.
It can be shown that the problem is EXPTIME-hard, see Chatterjee et al.
[2007], and thus the algorithm developed above is worst-case optimal. For
Buchi objectives, an EXPTIME algorithm can be obtained by substituting
the first line of the PosReach( W i ) operator by X 0 =
T∩ Spre( W i ) where
Spre( W i )=Apre( W i ,W i )=
W i
q
q : post σ ( q )
W i
{
q
|∃
σ
Σ
·∀
}
.
Intuitively, we start the iteration in PosReach( W i ) with those target states
from which Player 1 can force to stay in W i in the next round. This ensures
that whenever a target state is reached (which will happen with probability
one), Player 1 can continue to play and will again force a visit to the target set
with probability one, thus realising the objective Buchi(
T
) with probability 1.