Game Development Reference
InDepth 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 LFPsentence
ψ
:=
∀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 firstorder definable. However it not di
cult to generalise
the LFPdefinition of reachability to
LFPdefinitions for the winning
regions of reachability (and safety) games
. Consider reachabilitysafety
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 LFPformula
ψ
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 fixedpoint 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
fixedpoints
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 fixedpoints 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
fixedpoints, and to use the duality (and De Morgan's laws) to translate
LFPformulae to
negation normal form
, i.e., to push negations all the way
to the atoms.
Search Nedrilad ::
Custom Search