Game Development Reference
In-Depth Information
,T α ) ( a ))
By ordinal induction, one can easily see that the games
G
((
A
associated with th e gfp -induction of ϕ in
A
coincide with the unfolding of the
game
G
=
G
(
A
( a )). B y the Unfolding Lemma, we conclude that Play er 0
,T α ) ( a )).
wins the game
G
(
A
( a )) if, and only if, she wins all games
G
((
A
,T α )
By the induction hypothesis this h olds if, and only if, (
A
|
= ϕ ( a ) for all
α , which is equivalent to
= ψ ( a ).
For least fixed-point formulae we can dualize the arguments.
A |
Theorem 4.12 Let ψ be a well-named and parameter-free LFP -formula in
negation normal form, and let
be a relational structure. Then Player 0 has
a winning strategy from position ψ ( a ) in the game G (A ( a )) if, and only if,
A | = ψ ( a ) .
A
For future reference we note that the model-checking games ψ (
A
) can not
only be easily constructed from
A
and ψ , but are also easily (i.e., first-order)
definable inside
A
.
Theorem 4.13
For every structure
A
with at least two elements, and
every formula ϕ ( x )
LFP the model-checking game
G
(
A
) is first-order
interpretable in A .
For finite structures, the size of the game
G
(
A
( a )) (and the time complex-
width( ψ ) . Hence, for LFP-formulae
of bounded width, the size of the game is polynomially bounded.
ity of its construction) is bounded by
|
ψ
|·|
A
|
Corollary 4.14 The model-checking problem for LFP -formulae of bounded
width (and without parameters) is in NP
Co-NP , in fact in UP
Co-UP .
By the complexity results for parity games mentioned at the end of
Section 4.2, we obtain complexity bounds for LFP model-checking which are
polynomial with respect to the size of the structure, but exponential in the
width and the alternation depth of the formula.
Corollary 4.15 The model-checking problem for LFP -formulae of bounded
width and bounded alternation depth is solvable in polynomial time.
We have imposed the condition that the fixed-point formulae do not contain
parameters. If parameters are allowed, then, at least with a naive definition
of width, Corollary 4.14 is no longer true (unless UP = Pspace). The
intuitive reason is that with parameters one can 'hide' first-order variables in
fixed-point variables. Indeed, by Dziembowski [1996] the evaluation problem
for quantified Boolean formulae can be reduced to the evaluation of LFP-
formulae with two first-order variables (but an unbounded number of monadic