Game Development Reference
InDepth Information
Notice that if
ψ
does not contain fixedpoints, this game is the model
checking game for firstorder logic. However, if we have fixedpoints the
games may now admit infinite plays. The winning condition for infinite plays
will be a parity condition. To motivate the priority assignment let us discuss
some special cases:
Consider a formula with just one
lfp
operator,
ap
plied t
o
a
fi
rstorder
formula. The intuitio
n
is that from position [
lfp
T x.ϕ
(
T,x
)](
b
), Verifier
tries to establish that
b
enters
T
at some stage
α
of the fixedpoint induction
defined by
ϕ
on
. The game goes to
ϕ
(
T,b
) and from there, as
ϕ
is a
firstorder formula, Verifier can ei
t
her win
t
he
ϕ
game in a finite number of
steps, or force it to a position
T c
, where
c
enters t
he
fixedpoint at some
stage
β<α
. The game then resumes at position
ϕ
(
c
). As any descending
sequence of ordinals is finite, Verifier will win the game in a finite number
of steps. If the formula is not true, then Falsifier can either win in a finite
number of steps or force the play to go through infinitely many positions of
the form
T c
. Hence, these positions should be assigned priority 1 (and all
other positions higher priorities) so that such a play will be won by Falsifier.
For
gfp
formulae, the situation is reversed. Veri
fi
er wants to force an infinite
play, going infinitely often through positions
T c
,so
gfp
atoms are assigned
priority 0.
In the general case, we have a formula
ψ
with nested least and greatest
fixedpoints, and in an infinite play of
A
,ψ
) one may see different fixed
point variables infinitely often. But one of these variables is then the smallest
with respect to the dependency order
G
(
A
=
ψ
if,
and only if, this smallest variable is a
gfp
variable (provided the players play
optimally).
Hence, the priority labelling is defined as follows.
ψ
. It can be shown that
A

(1) Even priorities are assigned to
gfp
atoms and odd priorities to
lfp
atoms.
(2) If
S
ψ
T
and
S, T
are fixedpoint variables of different kinds, then
S
atoms should get a lower priority than
T
atoms.
(3) All positions that are not fixedpoint atoms, get a maximal (i.e., most
irrelevant) priority.
This completes the definition of the game
G
(A
,ψ
). Note that the number
of priorities in
G
(A
,ψ
) is essentially the alternation depth of
ψ
.
We want to prove that
G
(
A
,ψ
) is indeed a correct modelchecking game for
ψ
in
. The interesting case concerns
fixedpoint formulae
ψ
(
a
):=[
gfp
T
x
.ϕ
(
x
)](
a
). By the inductive constructi
on
of greatest fixedpoints,
A
. The proof proc
ee
ds by ind
uc
tio
n
on
A
,T
α
)
A

=[
gfp
T x.ϕ
(
x
)](
a
) if, and only if, (
A

=
ϕ
(
a
)
for all stages
T
α
of the
gfp
induction of
ϕ
on
A
. Further, by the induction
Search Nedrilad ::
Custom Search