Game Development Reference

In-Depth Information

between games and logic is explored, namely the question of how winning

regions in games are definable in logic. We shall see that for parity games with

a bounded number of priorities, winning regions are definable in both LFP

and the modal
μ
-calculus. For parity games with an unbounded number of

priorities it is not known whether the winning regions are LFP-definable. We

show that this problem is intimately related to the open question of whether

parity games are solvable in polynomial time. In the last two sections we

shall discuss the relationship between logic and games for more complicated

scenarios provided by
inflationary fixed-point logic
and the
quantitative

μ
-calculus
. In both cases, we can indeed find generalisations of parity games

with a balanced two-way relationship to the associated fixed-point logic. On

the one hand, we obtain appropriate evaluation games for all formulae in the

logic, and on the other hand, the winning regions in the games are definable

in the logic

4.2 Reachability games and parity games

We consider turn-based games where two players move a token through a

directed graph, tracing out a finite or infinite path. Such a
graph game
is

specified by a directed graph
G
=(
V,E
), with a partition
V
=
V
0

V
1
of the

nodes into positions of Player 0 and positions of Player 1. In case (
v, w
)

∪

E

we call
w
a successor of
v
and we denote the set of all successors of
v
by
vE
.

A
play
in

∈

is a finite or infinite path
v
0
v
1
...
formed by the two players

starting from a given initial position
v
0
. Whenever the current position
v
i

belongs to
V
0
, then Player 0 chooses a successor
v
i
+1
∈ v
i
E
,if
v
i
∈ V
1
, then

v
i
+1
∈ v
i
E
is selected by Player 1.

For
reachability games
we define the winning condition either by saying

that Player
σ
loses at positions
v ∈ V
σ
where no moves are possible, or by

explicitly including the sets
T
0
,T
1
of winning terminal positions for each

player into the description of the game. A play that is not won by any of the

two players is called a
draw
. In reachability games, infinite plays are draws.

It is often convenient to have games without draws, so that Player 1 wins

every play that is not won by Player 0, and vice versa. As the complement of

a reachability condition is a
safety
condition this leads to a
reachability-

safety game
: the winning condition is given by a set
T

G

V
; Player 0 wins

a play if it reaches
T
, and Player 1 wins if it remains inside
V

⊆

T
.

There is an extensive theory of games with more general winning conditions

for infinite plays that are specified either by logical formulae from some logic

on infinite sequences such as temporal logic (LTL), first-order logic (FO), or

\

Search Nedrilad ::

Custom Search