Game Development Reference
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.
ML , there exists a first-order
formula ψ ∗ ( x ) of width 2, which is equivalent to ψ in the sense that G, v
For every formula ψ
= ψ ∗ ( v ) .
The modal μ -calculus L μ extends ML by the following rule for building
fixed-point 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 fixed-point formulae is completely analogous to
that for LFP. The formula ψ defines on G (with universe V , and with
interpretations for other free second-order variables that ψ may have besides
X ) the monotone operator F ψ :
( V )
( V ) assigning to every set X
the set ψ G ( X ):=
V :( G, X ) ,v
G, v | = μX.ψ iff v ∈ lfp ( F ψ )
G, v | = νX.ψ iff v ∈ gfp ( F ψ ) .
X asserts that there exists a path
along a -transitions to a node where ϕ holds. The formula νX.μY.
The formula μ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
L μ is equivalent to a formula ψ ∗ ( x )
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 second-order
The model-checking games for LFP easily translate into games for the
μ -calculus . Given a formula ψ
L μ and a transition system
, we obtain a
,ψ ), with positions ( ϕ, v ) where ϕ is a subformula of ψ and