Game Development Reference
In-Depth Information
starting point v , find the set of nodes that are reachable by a path from v .
It is definable in LFP, by the formula
ψ ( x ):=[ lfp Rx . x = v ∨∃z ( Rz ∧ Ezx )]( x ) .
Indeed, in any graph ( G, v ), the set ψ G,v :=
{
w : G, v
|
= ψ ( w )
}
is precisely
the set of nodes reachable from w .
Exercise 4.3
Prove that the LFP-sentence
ψ := ∀y∃zFyz ∧∀y [ lfp Ry . ∀x ( Fxy→ Rx )]( y )
is an infinity axiom, i.e., it is satisfiable but does not have a finite model.
We have noticed above that winning regions of reachability and safety
games are not first-order definable. However it not di cult to generalise
the LFP-definition of reachability to LFP-definitions for the winning
regions of reachability (and safety) games . Consider reachability-safety
games G =( V,V 0 ,V 1 ,E,T ) where Player 0 wants to reach T and Player 1
tries to stay outside of T . On such games, the winning region W 0 of Player 0
is uniformly definable by the LFP-formula ψ 0 ( x ):=[ lfp Wx . ϕ ]( x ) with
ϕ ( W, x ):= Tx
( V 0 x
∧∃
y ( Exy
Wy ))
( V 1 ∧∀
y ( Exy
Wy )) .
The complement of W 0 , which is the winning region for Player 1 for her
associated safety condition, is defined by a greatest fixed-point formula
ψ 1 ( x ):=[ gfp Wx . η ( W, x )]( x ) with
η ( W, x ):=
¬
Tx
( V 0 x
→∀
y ( Exy
Wy ))
( V 1 →∃
y ( Exy
Wy )) .
This is just a special case of the duality between least and greatest
fixed-points which implies that for any formula ϕ ,
[ gfp Rx.ϕ ]( t )
≡¬
[ lfp Rx.
¬
ϕ [ R/
¬
R ]]( t ) ,
where ϕ [ R/¬R ] is the formula obtained from ϕ by replacing all occurrences of
R -atoms by their negations. (As R occurs only positively in ϕ , the same is true
for ¬ϕ [ R/¬R ].) Because of this duality, greatest fixed-points are sometimes
omitted in the definition of LFP. However, for studying the relationship
between LFP and games it is much more convenient to keep the greatest
fixed-points, and to use the duality (and De Morgan's laws) to translate
LFP-formulae to negation normal form , i.e., to push negations all the way
to the atoms.