Game Development Reference

In-Depth Information

4.6.3 Games for IFP

We restrict attention to finite structures. The model-checking game for an

IFP-formula
ψ
on a finite structure

,ψ
)=

(
V,E,V
0
,V
1
,B,
Ω). As in the games for LFP, the positions are subformulae

of
ψ
, instantiated by elements of

A

is a backtracking game

G

(

A

. We only describe the modifications.

We always assume that formulae are in negation normal form, and write

ϑ
for the negation normal form of
¬ϑ
. Consider any
ifp
-formula
ϕ
∗
(
x
):=

[
ifp
T x.ϕ
(
T,x
)](
x
)in
ψ
. In general,
ϕ
can have positive or n
eg
ative occur-

rences of the fixed-point variable
T
. We use the notation
ϕ
(
T,T
) to separate

positive and negative occurre
nc
es of
T
.
To
d
efi
ne the set of positions we in-

clude also all subformulae of
T x

A

ϕ
. N
ote that an
ifp
-subformula

in
ϕ
is translated into a
dfp
-subformula in
ϕ
, and vice versa. To avoid

conflicts we have to change the
na
mes
of
t
h
e
fi
xed-point variables when

doing this, i.e., a s
u
b
fo
r
mu
la [
i
f
p
Ry
.ϑ
(
R
, R, y
)](
y
)in
ϕ
will correspond to a

subformula [
dfp
R
y.ϑ
(
R
,R
, y
)](
y
)of
ϕ
where
R
is a new relation variable,

distinct from
R
.

From a position
ϕ
∗
(
a
)
th
e play proceeds to
T a

∨

ϕ
and
T x

∧

ϕ
(
T,a
). When a play

reaches a position
T c
or
T c
the play proceeds back to the formula defining

the fixed-point by a regeneration move. More pre
cis
ely,
t
he regeneration of

an
ifp
-atom
T c
is
T c∨ϕ
(
T,c
), the regeneration of
T
c
is
T c∧ϕ
(
T,c
). Verifier

can move from
T c
to its regeneration, Falsifier from
T c
.For
dfp
-subformulae

ϑ
∗
(
x
):=[
dfp
Rx.ϑ
(
R,
x
)
](
x
)
,
dual definitions apply. Verifier moves from

Rc
to its regeneration
Rc ∨ ϑ
(
R, c
), and Falsifier can make regeneration

moves from
Rc
to
Rc

∨

ϑ
(
R, c
). The priority assignment associates with each

ifp
-variable
T
an odd priority Ω(
T
) and with each
dfp
-variable
R
an even

priority Ω(
R
), such that for any two distinct fixed-point variables
S, S
,we

have Ω(
S
)

∧

=Ω(
S
), a
nd
wh
ene
ver
S
depends on
S
, then Ω(
S
)
<
Ω(
S
).

Positions of the form
Sc
and
Sc
are called
S
-positions. All
S
-positions get

priority Ω(
S
), all other formulae get a higher priority. The set
B
of backtrack

positions is the set of
S
-positions, where
S
is any fixed-point variable.

Let us fo
cu
s on IFP-formulae with a single fixed-point,
ψ
:= [
ifp
T x.ϕ
](
a
)

where
ϕ
(
T,x
) is a first-order formula. Whe
n
the pla
y
reaches a position
T c

Verifier can make a regeneration move t
o
T
c

ϕ
(
T,c
) or backtrack. Dually,

Falsifier can regenerate from positions
T c
or backtrack. However, since we

have only one fixed-point, all backtrack positions have the same priority and

only one backtrack move can occur in a play.

In this simple case, the rules of the backtracking game ensure that infinite

plays (which are plays without backtracking moves) are won by Falsifier,

since
ifp
-atoms have odd priority. However, if one of the players backtracks

∨

Search Nedrilad ::

Custom Search