Game Development Reference
,T α ) ,ϕ ( a ))
By ordinal induction, one can easily see that the games
associated with th e gfp -induction of ϕ in
coincide with the unfolding of the
,ψ ( a )). B y the Unfolding Lemma, we conclude that Play er 0
,T α ) ,ϕ ( a )).
wins the game
,ψ ( a )) if, and only if, she wins all games
,T α )
By the induction hypothesis this h olds if, and only if, (
= ϕ ( a ) for all
α , which is equivalent to
= ψ ( a ).
For least fixed-point formulae we can dualize the arguments.
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 ) .
For future reference we note that the model-checking games ψ (
,ψ ) can not
only be easily constructed from
and ψ , but are also easily (i.e., first-order)
For every structure
with at least two elements, and
every formula ϕ ( x )
LFP the model-checking game
,ϕ ) is first-order
interpretable in A .
For finite structures, the size of the game
,ψ ( 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
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
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  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