Game Development Reference
In-Depth Information
and it translates the modal operators by use of quantifiers as follows:
( ) ( 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 first-order
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
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 ψ :
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 second-order
logic (MSO).
The model-checking 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