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

Search Nedrilad ::

Custom Search