Game Development Reference
InDepth Information
fixedpoint variables) on a fixed structure with three elements. Hence the
expression complexity of evaluating such formulae is Pspacecomplete.
For LFPformulae of unbounded width, our analysis in terms of model
checking games only gives only exponential time bound. This cannot be
improved, even for very simple LFPformulae (Vardi [1982]).
Theorem 4.16
The modelchecking problem for
LFP
formulae (of un
bounded width) is
Exptime
complete, even for formulae with only one fixed
point operator, and on a fixed structure with only two elements.
4.4.4 The modal
μ
calculus
A fragment of LFP that is of fundamental importance in many areas of com
puter science (e.g., controller synthesis, hardware verification, and knowledge
representation) is the modal
μ
calculus
L
μ
. It is obtained by adding least
and greatest fixedpoints to propositional modal logic (ML) rather than to
FO. In other words
L
μ
relates to ML in the same way as LFP relates to FO.
Modal logics such as ML and the
μ
calculus are evaluated on transition
systems (alias Kripke structures, alias coloured graphs) at a particular
node. Given a formula
ψ
and a transition system
G
, we write
G, v
=
ψ
to denote that
G
holds at node
v
of
G
. Recall that formulae of ML, for
reasoning about
transition systems
G
=(
V,
(
E
a
)
a∈A
,
(
P
b
)
b∈B
), are built
from atomic propositions
P
b
by means of the usual propositional connectives
and the modal operators

a
and [
a
]. That is, if
ψ
is a formula and
a
∈
A
is
an action, then we can build the formulae
a
ψ
and [
a
]
ψ
, with the following
semantics:
G, v

=
a
ψ
iff
G, w

=
ψ
for
some w
suchthat(
v, w
)
∈
E
a
,
G, v

=[
a
]
ψ
iff
G, w

=
ψ
for
all w
suchthat(
v, w
)
∈
E
a
.
If there is only one transition relation, i.e.,
A
=
{
a
}
, then we simply write
and
, respectively.
ML can be viewed as an extension of propositional logic. However, in our
context it is more convenient to view it as a simple fragment of firstorder
logic. A modal formula
ψ
defines a query on transition systems, associating
with
G
a set of nodes
ψ
G
♦
for [
a
] and
a
, and this set can be defined
equivalently by a firstorder formula
ψ
∗
(
x
). This translation maps atomic
propositions
P
b
to atoms
P
b
x
, it commutes with the Boolean connectives,
:=
{
v
:
G, v

=
ψ
}
Search Nedrilad ::
Custom Search