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