Game Development Reference
InDepth Information
Player 1) tries to establish that the sentence is false. For firstorder 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 firstorder sentence in negation normal form, i.e., built up from atoms
and negated atoms by means of the propositional connectives
A
∧
,
∨
and the
quantifiers
. Obviously, any firstorder formula can be converted in linear
time into an equivalent one in
n
egation n
or
mal form. The modelchecking
game
∃
,
∀
,ψ
) 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
G
(
A
=
a
,
Ra
,or
¬
Ra
, the game
is over. Verifier has won the play if
=
ϕ
(
a
); otherwise, Falsifier has won.
Modelchecking games are a way of defining the semantics of a logic. The
equivalence to the standard definition can be proved by a simple induction.
A

Theorem 4.4
Verifier has a winn
in
g strategy from position ϕ
(
a
)
in the
game
G
(
A
,ψ
)
if, and only if,
A

=
ϕ
(
a
)
.
This suggests a gamebased approach to modelchecking: 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 firstorder modelchecking
A modelchecking 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 modelchecking
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
the structure
, then the modelchecking problem for
L
on this structure
amounts to deciding Th
L
(
A
. The
complexity of this problem is called the
expression complexity
of the
modelchecking problem (for
L
on
A
):=
{
ψ
∈
L
:
A

=
ψ
}
, the
L
theory
of
A
). Especially in finite model theory, one
often considers modelchecking problems for a fixed formula
ψ
, which amounts
A
Search Nedrilad ::
Custom Search