Game Development Reference
InDepth Information
and it translates the modal operators by use of quantifiers as follows:
(
aψ
)
∗
(
x
):=
∃y
(
E
a
xy ∧ ψ
∗
(
y
))
([
a
]
ψ
)
∗
(
x
):=
∀y
(
E
a
xy → ψ
∗
(
y
))
.
Note that the resulting formula has width 2 and can thus be written with
only two variables.
Theorem 4.17
ML
, there exists a firstorder
formula ψ
∗
(
x
)
of width 2, which is equivalent to ψ in the sense that G, v
For every formula ψ
∈

=
ψ
=
ψ
∗
(
v
)
.
iff G

The
modal
μ
calculus
L
μ
extends ML by the following rule for building
fixedpoint formulae: If
ψ
is a formula in
L
μ
and
X
is a propositional variable
that only occurs positively in
ψ
, then
μX.ψ
and
νX.ψ
are also
L
μ
formulae.
The semantics of these fixedpoint formulae is completely analogous to
that for LFP. The formula
ψ
defines on
G
(with universe
V
, and with
interpretations for other free secondorder variables that
ψ
may have besides
X
) the monotone operator
F
ψ
:
P
(
V
)
→P
(
V
) assigning to every set
X
⊆
V
the set
ψ
G
(
X
):=
{
v
∈
V
:(
G, X
)
,v

=
ψ
}
.Now,
G, v 
=
μX.ψ
iff
v ∈
lfp
(
F
ψ
)
G, v 
=
νX.ψ
iff
v ∈
gfp
(
F
ψ
)
.
Example 4.18
X
asserts that there exists a path
along
a
transitions to a node where
ϕ
holds. The formula
νX.μY.
The formula
μX.ϕ
∨
a
a
((
ϕ
∧
X
)
Y
) says that there exists a path from the current node on which
ϕ
holds infinitely often.
∨
Exercise 4.4
Prove that the formulae in Example 4.18 do indeed express
the stated properties.
The translation from ML into FO extends to a translation from
L
μ
into
LFP.
L
μ
is equivalent to a formula ψ
∗
(
x
)
Theorem 4.19
Every formula ψ
∈
∈
LFP
of width two.
Further the argument proving that LFP can be embedded into second
order logic also shows that
L
μ
is a fragment of
monadic secondorder
logic
(MSO).
The modelchecking games for LFP easily translate into
games for the
μ
calculus
. Given a formula
ψ
∈
L
μ
and a transition system
K
, we obtain a
parity game
G
(
K
,ψ
), with positions (
ϕ, v
) where
ϕ
is a subformula of
ψ
and
Search Nedrilad ::
Custom Search