Game Development Reference
InDepth Information
2
L
•
The set of locations is
S
=
{
s
∈
\{
∅
}∃
o
∈O·
s
⊆
o
}
. In the sequel,
we call a set
s
∈
S
a
cell
.
•
The initial location is
s
I
=
{
l
I
}
.
The set of labelled transitions Δ
K
⊆
S
contains all (
s, σ, s
) for
•
S
×
Σ
×
such that
s
= post
σ
(
s
)
which there exists
o
∈O
∩
o
.
Note that since the game graph
G
is total and the observations form a
partition of the locations, the game graph
G
K
is also total.
To complete the reduction, we show how to translate the objectives. Given
a priority function
pr
:
defining the parity objective
ϕ
in
G
,
we define the parity objective
ϕ
K
in
G
K
using the priority function
pr
K
such
that
pr
K
(
s
)=
pr
(
o
) for all
s ∈ S
and
o ∈O
such that
s ⊆ o
.
O→{
0
,...,d
}
Theorem 6.6
(Chatterjee et al. [2007])
Player
1
has an observationbased
surelywinning strategy in a game structure G with imperfect information for
an observable parity objective ϕ if and only if Player
1
has a surelywinning
strategy in the game structure G
K
with perfect information for the parity
objective ϕ
K
.
Exercise 6.7
Write a proof of Theorem 6.6.
Observable safety and reachability objectives are defined by sets
T⊆L
of
target locations that are a union of observations. Hence for all cells
s ∈ S
,
either
s ∩T
= ∅ or
s ⊆T
. In the above reduction, such an objective is
transformed into an objective of the same type with the set of target cells
T
K
=
{
s
∈
S

s
⊆T}
.
Exercise 6.8
Consider a game structure with imperfect information
G
=
L, l
I
,
Σ
,
Δ
,O
and a
nonobservable
reachability objective defined by
T⊆L
.
Construct an equivalent game structure with imperfect information
G
with
an observable reachability objective Reach(
T
), i.e., such that Player 1 has
an observationbased surelywinning strategy in
G
for Reach(
) if and only if
Player 1 has an observationbased surelywinning strategy in
G
for Reach(
T
T
).
Hint: take
G
=
O
O
=
L, l
I
,
Σ
,
Δ
,
where
{
o
∩T 
o
∈O}∪{
o
∩
(
L
\T
)

o
.
Note that nonobservable Buchi objectives are more di
cult to handle. For
such objectives and more generally for nonobservable parity objectives, our
knowledgesubset construction is not valid and techniques related to Safra's
determinisation need to be used (Safra [1988]).
∈O}
Search Nedrilad ::
Custom Search