Game Development Reference
on the domain of arbitrary finite structures. Since there exist logics for NP
this would imply that P
4.4.3 model-checking games for least fixed-point logic
We now construct evaluation games for LFP-formulae. We make the following
(1) Fixed-point formulae do not contain parameters. This means that in a
subfo rm ula [ fp Rx.ϕ ] (where fp means either lfp or gfp ), th e formula
ϕ ( R, x ) contains no free first-order variables besides those in x . This is
no loss of generality since one can always eliminate parameters, but it
may affect the complexity of model-checking algorithms.
(2) Formulae are in negation normal form, i.e., negations apply to atoms only.
Due to the standard dualities of first-order operators and the duality of
least and greatest fixed points, this is no loss of generality.
(3) Every fixed-point variable is bound only once and the free relation
variables are distinct from the fixed-point variables. For every fixed-point
variable T occur ri ng in ψ , we write ϕ T for the unique subformula in ψ
of the form [ fp T x.η ( T,x )].
(4) Finally, we require that each occurrence of a fixed-point variable T in
ϕ T is inside the scope of a quantifier. Again, this is no loss of generality.
For two fixed-point variables S, T , we say that S depends on T if T
occurs free in ϕ S . The transitive closure of this dependency relation is called
the dependency order , denoted by
ψ . The alternation level al ψ ( T )of
T in ψ is the maximal number of alternations between least and greatest
fixed-point variables on the ψ -paths from T . The alternation depth ad ( ψ )
of a fixed-point formula ψ is the maximal alternation level of its fixed-point
For a structure
and an LFP-sentence ψ , the arena of the model-checking
game G (A ,ψ ) is defined as for first-order model-checking games, with ad-
ditional moves for fixed-point formulae. The positions are subformulae of
ψ instantiated by elements of A. The moves are as in the first-order game,
except for the positions associated with fixed-point formulae and with fixed-
point atoms. At such positions there is a unique move (by Falsifier, say)
to the formula defining the fixed-point . For ea ch fi x ed-point variable T in
ψ , th e re is a u ni q ue subformula [ fp T x.ϕ ( T,x )]( y )of ψ . From position
[ f p T x.ϕ ( T,x )]( b ), Falsifier moves to ϕ ( T,b ), and from any fixed-point atom
T c , she moves to the position ϕ ( T,c ).