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

Search Nedrilad ::

Custom Search