Game Development Reference
In-Depth Information
be computed in polynomial time. Denote by W σ the set of positions from
which Player σ has a strategy to win the game in at most n moves. Then
W σ =
is the set of winning terminal positions for
Player σ , and we can compute the sets W σ inductively by using
W n +1
{
v
V 1 −σ : vE =
∅}
σ := W σ ∪{v ∈ V 0 : vE ∩ W σ = ∅}∪{v ∈ V 1 : vE ⊆ W σ }
until W n + σ = W σ .
With a more sophisticated algorithm, which is a clever variant of depth-
first search, one can actually compute the winning regions of both players in
linear time O (
|
V
|
+
|
E
|
Theorem 4.1 Winning regions of finite reachability games, and hence also
reachability-safety games, can be computed in linear time.
Further, the problem of computing winning regions of reachability games
is complete for Ptime (see Greenlaw et al. [1995]).
Positional determinacy and complexity of parity games. Winning
strategies can be very complicated objects since they may depend on the
entire history of a play. However, for many important games, including
reachability, safety, and parity games, it su ces to consider positional
strategies , which are strategies that depend only on the current position,
not on the history of the play. A game is positionally determined ,ifitis
determined, and each player has a positional winning strategy on her winning
region.
The positional determinacy of reachability games - and reachability-safety
games - is obvious since the winning condition itself is purely positional. For
parity games the positional determinacy is a non-trivial and fundamental
result. It has been established independently by Emerson and Jutla [1991]
and Mostowski [1991] for parity games with a finite game graph. This is
generalised by Zielonka [1998] to infinite game graphs with a finite number
of priorities. Finally positional determinacy has been extended by Gradel
and Walukiewicz [2006] to parity games with rng(Ω) = ω .
Theorem 4.2
Every parity game is positionally determined.
In a parity game G =( V,V 0 ,V 1 ,E, Ω), a positional strategy for Player σ ,
defined on W
V , can be represented by a subgraph H =( W, S )
( V,E )
such that there is precisely one outgoing S -edge from each node v
V σ
W
and vS = vE for each node v
W . On a finite game graph, such a
strategy is winning on W if, and only if, the least priority on every cycle in
( W, S ) has the same parity as σ .
V 1 −σ