Game Development Reference
InDepth Information
to deciding the
model class
of
ψ
inside
.
Its complexity is the
structure complexity
of the modelchecking problem
(for
ψ
on
D
, Mod
D
(
ψ
):=
{
A
∈D
:
A

=
ψ
}
D
).
Since reachability games can be solved in linear time, the size of the game
graph directly gives us an upper bound for the time complexity for firstorder
modelchecking. The size of the modelchecking game
,ψ
) is the number
of different instantiations of the subformulae of
ψ
with elements from
G
(
A
.It
depends on several parameters, including the cardinality of the structure
A
A
, the number of subformulae of
ψ
(which is of course bounded by the
length
ψ
) and the
width
of
ψ
which is defined as the maximal number of
free variables in subformulae of
ψ
. Clearly,
width(
ψ
)
,so
the crucial parameter is the width of the formula: if we have subformulae
with many free variables, then the number of instantiations, and thus the
size of the game, becomes very large. In general the combined complexity
and the expression complexity of firstorder modelchecking problem are
Pspacecomplete. In turn, the game graphs have polynomial size for any
class of firstorder formulae with bounded width.
G
(
A
,ψ
)
≤
ψ
·
A

Theorem 4.5
The modelchecking problem for firstorder logic is
Pspace

complete. For any fixed k ≥
2
, the modelchecking problem for firstorder
formulae of width at most k is
Ptime
complete.
Exercise 4.1
Prove the hardness results. Reduce QBF, the problem of
evaluating quantified Boolean formulae, to the modelchecking problem for
firstorder logic on a fixed structure with two elements. Reduce the problem
of solving reachability games to the modelchecking problem for formulae of
width 2.
By applying the gamebased analysis of modelchecking to the case of a
fixed sentence
ψ
, we see that the structure complexity of firstorder logic
is much lower than the expression or combined complexity. In particular,
the evaluation problem for any fixed firstorder sentence can be computed
deterministically in logarithmic space.
For a detailed study of the complexity of firstorder modelchecking, giv
ing precise complexity bounds in terms of deterministic and alternating
complexity classes, the reader may consult Gradel [2007].
4.3.4 Definability of winning regions
Let
be a class of games, represented as structures of some fixed vocabulary.
We say that
winning regions on
S
are definable in a logic
L
if there
S
Search Nedrilad ::
Custom Search