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.

Search Nedrilad ::

Custom Search