Game Development Reference
In-Depth Information
W i +1
0, and therefore the sequence of sets ( W i ) i≥ 0 is
decreasing and eventually stabilises. The limit of this sequence is defined as
W =
i≥ 0
W i
⊆T
for all i
W i
and this is the set of surely-winning locations for Player 1. This result follows
from the facts that for all i
W i +1 , Player 1
0 and from all locations
can force the game to be in a location of W i
in the next round, and that
W = W j +1 = W j
0. We can compute the sets W i as follows:
for some j
W 0
= T
W i +1
= T∩ Cpre( W i ) for all i ≥ 0 .
Note that the limit W is obtained after at most n iterations where n =
is
the number of target locations. The set W can also be viewed as the greatest
solution of the equation W =
|T|
·T∩ Cpre( W ). The
argument showing that a unique greatest fixpoint exists is not developed
in this chapter. We simply mention that it relies on the theory of complete
lattices and Kleene's fixpoint theorem.
T∩ Cpre( W ), denoted νW
Theorem 6.2 (Safety games) The set of surely-winning positions for
Player 1 in safety games with perfect information can be computed in linear
time.
For reachability objectives, the algorithmic solution based on Cpre com-
putes a sequence of sets W i ( i
W i , Player 1
0) such that from every
can force the game to reach some location
∈T
within the next i rounds. It
can be computed as follows:
W 0
=
T
W i +1
T∪ Cpre( W i ) for all i
=
0 .
The necessary number of iterations is at most
|
L
\T|
. In terms of fixpoint,
the set W is the least solution of the equation W =
T∪ Cpre( W ), denoted
μW
·T∪ Cpre( W ).
Theorem 6.3 (Reachability games) The set of surely-winning positions
for Player 1 in reachability games with perfect information can be computed
in linear time.
For parity objectives, several algorithms have been proposed in the litera-
ture (see, e.g., Zielonka [1998], Jurdzinski [2000], Schewe [2008], and Fried-
mann and Lange [2009] for a survey). Using the result of memoryless deter-
minacy (Theorem 6.1), it is easy to show that parity games can be solved in