Game Development Reference
InDepth Information
,
we construct the game structure (with perfect information)
H
= Knw(
G
)=
Given a game structure with imperfect information
G
=
L, l
I
,
Σ
,
Δ
,
O
Q, q
I
,
Σ
,
Δ
H
as follows:
•
Q
=
{
(
s,
)
∃
o
∈O
:
s
⊆
o
and
∈
s
}
;
•
the initial state is
q
I
=(
{
l
I
}
,l
I
);
Q
is defined by ((
s,
)
,σ,
(
s
,
))
•
the transition relation Δ
H
⊆
Q
×
Σ
×
∈
such that
s
= post
σ
(
s
)
Δ
H
iff there is an observation
o
∈O
∩
o
and
(
, σ,
)
∈
Δ.
The structure
H
is called the
extended knowledgebased subset construction
of
G
. Intuitively, when
H
is in state (
s,
), it corresponds to
G
being in
location
and the knowledge of Player 1 being
s
. The game
H
= Knw(
G
)
is given in Figure 6.7 for the game
G
of Figure 6.2. Reachability and safety
objectives defined by a target set
L
are transformed into an objective
of the same type where the target set of states is
T⊆
T
=
{
(
s,
)
∈
Q

∈T}
.
A parity objective
ϕ
in
G
defined by a priority function
pr
:
L
is
transformed into a parity objective
ϕ
Knw
in
H
using the priority function
pr
Knw
such that
pr
Knw
(
s,
)=
pr
(
o
) for all (
s,
)
→
N
∈
Q
and
o
∈O
such that
s
⊆
o
.
Equivalence preserving strategies
Since we are interested in observa
tionbased strategies for Player 1 in
G
, we require that the strategies of
Player 1 in
H
only depend on the sequence of knowledge
s
0
...s
i
in the
sequence of previously visited states (
s
0
,
0
)
...
(
s
i
,
i
). Two states
q
=(
s,
)
and
q
=(
s
,
)of
H
are
equivalent
, written
q ≈ q
,if
s
=
s
, i.e., when the
knowledge of Player 1 is the same in the two states. For a state
q ∈ Q
,we
denote by [
q
]
≈
=
{q
∈ Q  q ≈ q
}
the
≈
equivalence class of
q
. Equivalence
and equivalence classes for plays and labelled histories are defined in the
expected way. A strategy
α
for Player 1 in
H
is
equivalencepreserving
if
α
(
ρ
)=
α
(
ρ
) for all labelled histories
ρ, ρ
of
H
such that
ρ
ρ
.
≈
Theorem 6.8
(Chatterjee et al. [2007])
For all game structures G with
imperfect information, Player
1
has an observationbased almostsurely
winning strategy in G for a parity objective ϕ if and only if Player
1
has an
equivalencepreserving almostsurelywinning strategy in H
= Knw(
G
)
for
the parity objective ϕ
Knw
.
Solving reachability objectives
It can be shown that for reachability
and Buchi objectives, memoryless strategies are su
cient for Player 1 to
almostsurely win the game with perfect information
H
= Knw(
G
). Let
Search Nedrilad ::
Custom Search