Game Development Reference
In-Depth Information
, the
winning regions W 0 and W 1 for the two players. This means that, for each
game
exist formulae ψ 0 ( x ) and ψ 1 ( x )of L that define, on each game
G∈S
G∈S
, and σ =0 , 1
W σ =
{
v
∈G
:
G|
= ψ σ ( v )
}
.
We can view a logic L and class
S
of games as balanced , if on the one
provides model-checking games for L , and on the other hand, the
winning regions for games in
hand,
S
are definable in L .
While reachability games are appropriate model-checking games for first-
order logic, the reverse relationship does not hold. Indeed it is well-known
that the expressive power of first-order logic, for defining properties of finite
or infinite structures, is rather limited. A general result making this precise
is Gaifman's Theorem , saying that first-order logic can express only local
properties . For an exact statement and proof of this fundamental result,
we refer to Ebbinghaus and Flum [1999]. Perhaps the simplest query that
is not local, and hence not first-order definable, is reachability : Given a
directed graph G =( V,E ) and a starting node v , determine the set of all
nodes that are reachable from v . This also implies that first-order logic is too
weak for reachability games; indeed the reachability problem can be viewed
as the problem of computing winning regions in the special case of one-player
reachability games.
S
Theorem 4.6
Winning regions of reachability games are not first-order
definable.
Thus, already for reachability games, and even more so for parity games,
more powerful logics are required to define the winning regions. Appropriate
logics for this are fixed-point logics that we are going to study in the next
section. In particular, we shall see that LFP and parity games (with a
bounded number of priorities) are balanced.
4.4 Logics with least and greatest fixed-points
Consider a formula ψ ( R, x ) of vocabulary τ ∪{R} where x is a tuple of
variables whose length matches the arity of R . Such a formula defines, for
every τ -structure
( A k )
( A k ) on the class
A
,an update operator F ψ :
P
→P
of k -ary relations on A ,by
F ψ : R
→{
a :(
A
,R )
|
= ψ ( R, a )
}
.
A fixed-point of F ψ is a relation R for which F ψ ( R )= R . Fixed-point
logics extend a basic logical formalism (such as first-order logic, conjunctive