Game Development Reference
Player 1) tries to establish that the sentence is false. For first-order logic,
the evaluation games are simple, in the sense that (1) all plays are finite
(regardless of whether the input structure is finite or infinite) and (2) winning
conditions are defined in terms of reachability.
Let us assume that
=( A, R 1 ,...,R m ) is a relational structure and ψ
is a first-order sentence in negation normal form, i.e., built up from atoms
and negated atoms by means of the propositional connectives
. Obviously, any first-order formula can be converted in linear
time into an equivalent one in n egation n or mal form. The model-checking
,ψ ) has positi o ns ϕ ( a ) where ϕ ( x ) is a subformula of ψ which is
instantiated by a tuple a of elements of A . The initial position of the game
is the formula ψ .
Verifier (Player 0) moves from positions associated with disjunctions and
with formulae starting with an existential quantifier. From a position ϕ ∨ ϑ ,
she moves to either ϕ or ϑ . From a position ∃yϕ ( a, y ), Verifier can move to any
position ϕ ( a, b ), where b ∈ A . Dually, Falsifier (Player 1) makes corresponding
moves for conjunctions a nd universal quantifications. A t atom s or negated
atoms, i.e., positions ϕ ( a ) of the form a = a , a
= a , Ra ,or
Ra , the game
is over. Verifier has won the play if
= ϕ ( a ); otherwise, Falsifier has won.
Model-checking games are a way of defining the semantics of a logic. The
equivalence to the standard definition can be proved by a simple induction.
Verifier has a winn in g strategy from position ϕ ( a ) in the
,ψ ) if, and only if,
= ϕ ( a ) .
This suggests a game-based approach to model-checking: given A and
ψ , construct the game G (A ,ψ ) and decide whether Verifier has a winning
strategy from the initial position.
4.3.3 Complexity of first-order model-checking
A model-checking problem has two inputs: a structure and a formula. We
can measure the complexity in terms of both inputs, and this is what is
commonly referred to as the combined complexity of the model-checking
problem (for L and D ). However, in many cases, one of the two inputs is
fixed, and we measure the complexity only in terms of the other. If we fix
, then the model-checking problem for L on this structure
amounts to deciding Th L (
complexity of this problem is called the expression complexity of the
model-checking problem (for L on
, the L -theory of
). Especially in finite model theory, one
often considers model-checking problems for a fixed formula ψ , which amounts