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.

Search Nedrilad ::

Custom Search