Game Development Reference
In-Depth 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 observation-based
surely-winning strategy in a game structure G with imperfect information for
an observable parity objective ϕ if and only if Player 1 has a surely-winning
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 non-observable 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 observation-based surely-winning strategy in G for Reach(
) if and only if
Player 1 has an observation-based surely-winning 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 non-observable Buchi objectives are more di cult to handle. For
such objectives and more generally for non-observable parity objectives, our
knowledge-subset construction is not valid and techniques related to Safra's
determinisation need to be used (Safra [1988]).
∈O}