Game Development Reference
In-Depth 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 knowledge-based 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-
tion-based 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 equivalence-preserving 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 observation-based almost-surely-
winning strategy in G for a parity objective ϕ if and only if Player 1 has an
equivalence-preserving almost-surely-winning 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
almost-surely win the game with perfect information H = Knw( G ). Let