Game Development Reference
In-Depth Information
fixed-point variables) on a fixed structure with three elements. Hence the
expression complexity of evaluating such formulae is Pspace-complete.
For LFP-formulae 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 LFP-formulae (Vardi [1982]).
Theorem 4.16 The model-checking 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 fixed-points 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 first-order
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 first-order formula ψ ( x ). This translation maps atomic
propositions P b to atoms P b x , it commutes with the Boolean connectives,
:=
{
v : G, v
|
= ψ
}