Game Development Reference
In-Depth Information
there exists no transition ( , σ, )
Δ, then Player 1 is declared losing the
game. Given a non-total game graph G and parity objective ϕ in G , define a
generic construction of a total game graph G along with a parity objective
ϕ such that Player 1 has a surely-winning strategy in
G, ϕ
if and only if
G
he has a surely-winning strategy in
.
Exercise 6.3 Traditionally, a two-player game is a directed graph V,v I ,E
where V is partitioned into V 1 ,V 2 the sets of vertices of Player 1 and Player 2
respectively, v I ∈ V is the initial vertex, and E ⊆ V ×V is a set of edges. We
call this model an edge-game . A parity objective is defined by a priority
function pr : V
as above. A (memoryless) strategy for player i
( i =1 , 2) is a function γ i : V i
→{
0 , 1 ,...,d
}
V i .
The definition of plays and outcomes is adapted accordingly. Show that
the edge-games are equivalent to our game graphs by defining a generic
transformation ( a ) from parity edge-games to parity game graphs, and ( b )
from parity game graphs to parity edge-games, such that player 1 has a
surely-winning strategy in one game if and only if he has a surely-winning
strategy in the other game.
Hint: for ( a ), first define an equivalent bipartite graph
E such that ( v, γ i ( v ))
E for all v
V ,v I ,E
such
that for all edges ( v, v )
E , v
V 1 if and only if v
V 2 .
Algorithms We present an algorithmic solution to the problem of deciding,
given a game graph G and an objective ϕ , if Player 1 has a surely-winning
strategy for ϕ in G . The set of locations in which Player 1 has a surely-
winning strategy can be computed symbolically as the solution of certain
nested fixpoint formulas, based on the controllable predecessor operator
Cpre :2 L
2 L
which, given a set of locations s
L , computes the set of
locations
L from which Player 1 can force the game to be in a location
of s in the next round, i.e., she has an action σ
Σ such that all transitions
from labelled by σ lead to s . Formally,
L :if( , σ, )
Δ then
Cpre( s )=
{
L
|∃
σ
Σ
·∀
s
}
.
Exercise 6.4
( a ) Show that Cpre is a monotone operator for the subset
s implies Cpre( s )
Cpre( s ) for all s, s
ordering i.e., s
L .
( b ) Define the controllable predecessor operator for the two-player edge-games
of Exercise 6.3.
). To win such a game,
Player 1 has to be able to maintain the game in the set
Consider a game with safety objective Safe(
T
T
for infinitely many
0, let W i
rounds. For all i
L be the set of locations from which Player 1
can maintain the game in the set
T
for at least the next i rounds. Clearly