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
\