Game Development Reference

In-Depth Information

on the domain of arbitrary finite structures. Since there exist logics for NP

this would imply that P

=NP.

4.4.3 model-checking games for least fixed-point logic

We now construct evaluation games for LFP-formulae. We make the following

assumptions:

(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

variables.

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
).

A

Search Nedrilad ::

Custom Search