Game Development Reference
In-Depth Information
that are able to force the cell
{
7
}
. We give here the sequence of antichains
computed by our algorithm.
X 0 =
{{
7
}}
,
X 1 = X 0
Cpre( X 0 )=
{{
1
}
,
{
2
}
,
{
3
}
,
{
7
}}
,
X 2 = X 1
,
X 3 = X 2 Cpre( X 2 )= {{ 1 , 2 },{ 2 , 3 },{ 1 , 3 },{ 4 },{ 5 },{ 6 },{ 7 }},
X 4 = X 3 Cpre( X 3 )= {{ 1 , 2 },{ 2 , 3 },{ 1 , 3 },{ 4 , 6 },{ 5 , 6 },{ 4 , 5 },{ 7 }},
X 5 = X 4 Cpre( X 4 )= {{ 1 , 2 , 3 },{ 4 , 6 },{ 5 , 6 },{ 4 , 5 },{ 7 }},
X 6 = X 5 Cpre( X 5 )= {{ 0 , 1 , 2 , 3 },{ 0 , 4 , 6 },{ 0 , 5 , 6 },{ 0 , 4 , 5 },{ 0 , 7 }},
X 7 = X 6 .
Cpre( X 1 )=
{{
1
}
,
{
2
}
,
{
3
}
,
{
4
}
,
{
5
}
,
{
6
}
,
{
7
}}
As
, this shows that Player 1 has a deterministic winning strategy
in this version of the 3-coin game.
{
0
}∈
X 7
6.3.4 Strategy construction
The algorithms presented in Section 6.2 for safety and reachability games
compute the set of winning positions for Player 1. We can use these algorithms
to compute the set of winning cells in a game with imperfect information,
using the controllable predecessor operator Cpre A . This gives a compact
representation (an antichain) of the downward-closed set of winning cells.
However, it does not construct surely-winning strategies. We show that in
general, there is a direct way to construct a surely-winning strategy for safety
games, but not for reachability and parity games.
For safety games with perfect information, the fixed-point computation
shows that the set of winning positions satisfies the equation W = T∩
Cpre( W ). Therefore, W ⊆ Cpre( W ), and thus for each ∈ W , there exists an
action σ Σ such that post σ ( {} ) ⊆ W . Since, W ⊆T , it is easy to see that
the memoryless strategy playing σ in each location ∈ W is surely-winning.
For safety games with imperfect information, the fixed-point W is repre-
sented by an antichain q win such that W = q win . The strategy construction
for safety games with perfect information can be extended as follows. By
definition of Cpre A , for each s
q win
there exists σ s
Σ such that for all
,wehavepost σ s ( s )
s for some s
o
∈O
o
q win . It is easy to see that
the strategy playing σ s in every cell s
s is surely-winning.
Thus, we can define a surely-winning strategy by the Moore machine
M, m I , update
where M = q win , m I = s such that s I
s for some
s
q win , μ : M
Σ is an output function such that μ ( s )= σ s as defined