Game Development Reference
In-Depth Information
to deciding the model class of ψ inside
.
Its complexity is the structure complexity of the model-checking 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 first-order
model-checking. The size of the model-checking 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 first-order model-checking problem are
Pspace-complete. In turn, the game graphs have polynomial size for any
class of first-order formulae with bounded width.
|G
(
A
)
|≤|
ψ
|·|
A
|
Theorem 4.5 The model-checking problem for first-order logic is Pspace -
complete. For any fixed k ≥ 2 , the model-checking problem for first-order
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 model-checking problem for
first-order logic on a fixed structure with two elements. Reduce the problem
of solving reachability games to the model-checking problem for formulae of
width 2.
By applying the game-based analysis of model-checking to the case of a
fixed sentence ψ , we see that the structure complexity of first-order logic
is much lower than the expression or combined complexity. In particular,
the evaluation problem for any fixed first-order sentence can be computed
deterministically in logarithmic space.
For a detailed study of the complexity of first-order model-checking, 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