Game Development Reference
In-Depth Information
Notice that if ψ does not contain fixed-points, this game is the model-
checking game for first-order logic. However, if we have fixed-points 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 rst-order
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 fixed-point induction
defined by ϕ on
. The game goes to ϕ ( T,b ) and from there, as ϕ is a
first-order 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 fixed-point 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
fixed-points, 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 fixed-point variables of different kinds, then
S -atoms should get a lower priority than T -atoms.
(3) All positions that are not fixed-point 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 model-checking game for
ψ in
. The interesting case concerns
fixed-point formulae ψ ( a ):=[ gfp T x ( x )]( a ). By the inductive constructi on
of greatest fixed-points,
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