Game Development Reference
In-Depth Information
H = Knw( G )=
Q, q I , Σ , Δ H
, let Reach(
T
)with
T⊆
Q be an observable
reachability objective in H , and
the equivalence relation between states
of H as defined above. Player 1 almost-surely wins from the set of states
W
2 Σ and Good : Q
Q if there exist functions Allow : Q
Σ such that
for all q
W :
1 for all q
Allow( q ), post σ ( q )
q and for all σ
W ,
( q, q )
( q, Good( q ) ,q )
2 in the graph ( W, E ) with E =
{
W
×
W
|
Δ H }
,
all infinite paths visit a state in
T
,
3 Good( q )
Allow( q ).
Condition 1 ensures that the set W of winning states is never left. This
is necessary because if there was a positive probability to leave W , then
Player 1 would not win the game with probability 1. Condition 2 ensures
that from every state q ∈ W , the target T is entered with some positive
probability (remember that the action Good( q ) is played with some positive
probability). Note that if all infinite paths in ( W, E ) eventually visit T , then
all finite paths of length n = |W| do so. Therefore, the probability to reach
T
within n rounds can be bounded by a constant κ> 0, and thus after
every n rounds the target set
is reached with probability at least κ . Since
Condition 1 ensures the set W is never left, the probability that the target
set has not been visited after m
T
κ ) m . Since the
game is played for infinitely many rounds, the probability to reach
·
n rounds is at most (1
T
is
κ ) m = 1. By Condition 3, the actions that ensure progress
towards the target set can be safely played.
The algorithm to compute the set of states W
lim m→∞ 1
(1
Q from which Player 1
has an equivalence-preserving almost-surely-winning strategy for Reach(
T
)
is the limit of the following computations:
W 0
=
Q
W i +1
= PosReach( W i ) for all i
0
where the PosReach( W i ) operator is the limit of the sequence X j
defined by
X 0
=
T
X j +1
X j
Apre( W i ,X j ) for all j
=
0
where
Apre( W, X )=
{
q
W
|∃
σ
Σ:
post σ ( q )
q
q : post σ ( q )
X and
W
}
.
The operator Apre( W, X ) computes the set of states q from which Player 1
can ensure that some state of X is visited in the next round with positive