Game Development Reference
InDepth 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 fixedpoint formulae we can dualize the arguments.
A

Theorem 4.12
Let ψ be a wellnamed and parameterfree
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 modelchecking games
ψ
(
A
,ψ
) can not
only be easily constructed from
A
and
ψ
, but are also easily (i.e., firstorder)
definable inside
A
.
Theorem 4.13
For every structure
A
with at least two elements, and
every formula ϕ
(
x
)
∈
LFP
the modelchecking game
G
(
A
,ϕ
)
is firstorder
interpretable in
A
.
For finite structures, the size of the game
G
(
A
,ψ
(
a
)) (and the time complex
width(
ψ
)
. Hence, for LFPformulae
of bounded width, the size of the game is polynomially bounded.
ity of its construction) is bounded by

ψ
·
A

Corollary 4.14
The modelchecking problem for
LFP
formulae of bounded
width (and without parameters) is in
NP
∩
CoNP
, in fact in
UP
∩
CoUP
.
By the complexity results for parity games mentioned at the end of
Section 4.2, we obtain complexity bounds for LFP modelchecking 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 modelchecking problem for
LFP
formulae of bounded
width and bounded alternation depth is solvable in polynomial time.
We have imposed the condition that the fixedpoint 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' firstorder variables in
fixedpoint variables. Indeed, by Dziembowski [1996] the evaluation problem
for quantified Boolean formulae can be reduced to the evaluation of LFP
formulae with two firstorder variables (but an unbounded number of monadic
Search Nedrilad ::
Custom Search