Game Development Reference
In-Depth Information
ingredients in the description of such games are the winning conditions
for infinite plays. Among the simplest of these are recurrence (or Buchi)
conditions, which require that certain good states must occur infinitely often
in a play, or eventual safety conditions, which impose that from some point
onwards the play must stay outside a bad region. Of special importance for
us are parity games . These are games of possibly infinite duration where
we assign to each position a natural number, and the winner of an infinite
play is determined according to whether the least number seen infinitely
often in the play is even or odd. The importance of parity games is due to
several reasons.
(1) Many classes of games arising in practical applications admit reductions
to parity games (over larger game graphs). This is the case for games
modelling reactive systems, with winning conditions specified in some
temporal logic or in monadic second-order logic over infinite paths (S1S),
for Muller games, but also for games with partial information appearing
in the synthesis of distributed controllers.
(2) Parity games are positionally determined . This means that from
every position, one of the two players has a winning strategy whose
moves depend only on the current position, not on the history of the play.
This property is fundamental for the algorithmic synthesis of winning
strategies.
(3) Parity games arise as the model-checking games for fixed-point logics
such as the modal μ -calculus or LFP, the extension of first-order logic
by least and greatest fixed-points. Conversely, winning regions of parity
games (with a bounded number of priorities) are definable in both LFP
and the μ -calculus. Parity games are also of crucial importance in the
analysis of structural properties of fixed-point logics.
The last point, the intimate relationship between parity games and fixed-
point logic is a central theme of this chapter.
We shall start with an introduction to basic notions on reachability and
parity games, explain the notions of winning strategies and winning regions
and discuss algorithmic questions related to games. We study connections
between logic and games for the special case of reachability games. In
particular, we shall present in detail the model-checking games for first-
order logic. After that, we introduce logics with least and greatest fixed
points, such as LFP and the modal μ -calculus, and explain why parity games
are appropriate evaluation games for these logics. We shall also discuss
the algorithmic consequences of this result. Then, the reverse relationship
Search Nedrilad ::




Custom Search