Game Development Reference
In-Depth Information
(2) The model-checking problem for LFP -formulae of width at most k, for
any k
2 .
(3) The model-checking problem for the modal μ-calculus.
4.5.2 Alternation hierarchies
The formulae Win d also play an important role in the study of the alter-
nation hierarchy of the modal μ -calculus. Clearly, Win d has alternation
depth d and it has been shown that this cannot be avoided. As a consequence
the alternation hierarchy of the μ -calculus is strict, a result due to Bradfield
[1998] and Arnold [1999].
Sometimes, a slightly stronger formulation of this result is needed, for
parity games on finite and strongly connected graphs. This easily follows
from the general result by the finite model property of the μ -calculus and by
a straightforward reduction to strongly connected games.
Theorem 4.22
PG d are not definable
by formulae in the μ-calculus with alternation depth <d, even under the
assumption that the game graphs are finite and strongly connected.
Winning regions in parity games in
For LFP the strictness of the alternation hierarchy also applies, even on
certain fixed infinite structures, such as arithmetic
).
However, on finite structures , the interleaving of least and greatest fixed
points (or of lfp -operators and negation) can be completely avoided, at the
expense of increasing the arity of fixed-point operators. Indeed, a single
application of an lfp -operator to a first-order formula su ces to express
any LFP-definable property (see Immerman [1986] or Ebbinghaus and Flum
[1999]).
N
=(
N
, + ,
·
Theorem 4.23 On finite structures, every LFP -formula is equivalent to a
formula of the form ∃y [ lfp Rx.ϕ ( R, x )]( y,...,y ) .
This result can be streng th ened f ur ther. Notice that the model-checking
game of a formula
y [ lfp Rx.ϕ ( R, x )]( y,...,y ) is actually a reachability-
safety game. The winning region for Player 0 is this definable by an LFP-
formula of a particularly simple form, where the lfp -operator is applied to a
Δ 2 -formula.
Theorem 4.24 (Dahlhaus [1987]) Every LFP -definable property of finite
structures can be reduced, by a quantifier-free translation, to the problem of
computing winning regions in reachability games.

Custom Search