=Paper=
{{Paper
|id=None
|storemode=property
|title=On modal mu-calculus in S5 and applications
|pdfUrl=https://ceur-ws.org/Vol-810/paper-l01.pdf
|volume=Vol-810
|dblpUrl=https://dblp.org/rec/conf/cilc/DAgostinoL11
}}
==On modal mu-calculus in S5 and applications==
https://ceur-ws.org/Vol-810/paper-l01.pdf
On modal µ-calculus in S5 and applications
Giovanna D’Agostino1 and Giacomo Lenzi2
1
University of Udine, Italy
2
University of Salerno, Italy gilenzi@unisa.it
Abstract. We show that the vectorial µ-calculus model checking prob-
lem over arbitrary graphs reduces to the vectorial, existential µ-calculus
model checking problem over S5 graphs. We also draw some consequences
of this fact. Moreover, we give a proof that satisfiability of µ-calculus in
S5 is N P -complete, and by using S5 graphs we give a new proof that the
satisfiability problem of the existential µ-calculus is also N P -complete.
1 Introduction
Model checking is a technique widely used in verification of computer systems,
be they hardware or software, see [4]. In model checking, systems are modeled
as sets with one or more binary relation (in this paper we focus on systems
with one relation, i.e. graphs). The desirable properties a system should have
are formalized in some modal-like logic. Actually, modal logic itself is not ex-
pressive enough. For this reason, one considers more powerful formalisms. One
of them is modal µ-calculus, introduced in [15], an extension of modal logic with
least and greatest fixpoints of monotonic set-theoretic functions. Intuitively, least
fixpoints correspond to inductive definitions, and greatest fixpoints correspond
to coinductive definitions. Unlike plain modal logic, the µ-calculus is powerful
enough to express global properties of systems, i.e. properties which depend on
the whole possible history of the system. For instance, with greatest fixpoints
we can capture safety properties such as “the system will never crash”, whereas
with least fixpoints we can capture termination properties such as “every com-
putation of the system will terminate”. More complicate properties, e.g. fairness,
can be used by combining least and greatest fixpoints.
The model checking technique raises a natural computational question, which
is known as the (µ-calculus) model checking problem. Formally, the µ-calculus
model checking problem is: given a µ-calculus formula and a finite graph, check
whether the graph satisfies the formula. Because of the importance of model
checking in practice, it would be desirable to have an efficient, i.e. polynomial
time computable, model checking algorithm for arbitrary (finite) graphs, but this
algorithm has not been found. We know that the problem is in the complexity
class U P , see [14] (and a co − U P bound follows since the µ-calculus is closed
under negation). Recall that the class U P (Unique P ) contains the problems
solved in polynomial time by nondeterministic Turing machines which have at
most one accepting path on each input. So, the class U P lies somewhere between
P and N P (in particular, the model checking problem is in N P ). We will see
that the µ-calculus is tightly related to games, in particular parity games, and
in fact a promising approach to the model checking problem is the study of
various kinds of games. It must be said, however, that efficient model checking
algorithms exist when the number of alternating fixpoints is bounded, and this
is often the case in practice.
The other main theme of this paper is given by S5 graphs, i.e. graphs whose
relation is an equivalence.
The modal logic of S5 graphs (also called modal logic S5) is important be-
cause it is widely recognized as a good epistemic logic, where the box operator
[ ]φ means that some agent knows φ. When modal logic is interpreted on Kripke
structures, i.e. graphs, the vertices of the structure represent possible situations,
and it is reasonable that the knowledge of an agent is represented by an equiv-
alence relation on the vertices, which indicates that certain situations are not
distinguishable, in the agent’s knowledge.
So, S5 is a way of formalizing the ideas of knowledge, and it is used in many
applications such as artificial intelligence, etc. Often multimodal versions of S5
are considered, where different agents come into play; in this paper, however, we
will focus on a single modality, representing a single agent.
We will consider also the class of all transitive graphs, called K4 in the
modal logic literature. Many interesting relations are transitive: for instance, the
relation “the event A is posterior to the event B” defines a transitive relation
between events. In this paper K4 graphs play only a minor role; papers dedicated
to the µ-calculus in K4 are [2], [5] and [6].
In this paper we compare the behavior of the µ-calculus on arbitrary graphs
and on S5 graphs. It is well known that the µ-calculus is expressively equivalent
to modal logic over S5, but this equivalence does not transfer automatically to
an equivalence in complexity, neither for model checking, nor for satisfiability.
From this perspective we first show that the µ-calculus model checking prob-
lem for arbitrary graphs is as difficult as the subcase of S5 graphs, although the
class of S5 graphs is significantly simpler than the class of all graphs.
Then we move to the satisfiability problem. Quite generally, recall that the
satisfiability problem for a logic L on a class of models C is: given a formula φ
in L, decide whether there is a model of φ which is in C.
The satisfiability problem of the µ-calculus on arbitrary graphs is settled, in
the sense that it is EXP T IM E-complete: EXP T IM E-hardness of the problem
follows from [12], and membership to EXP T IM E is proved in [8]. We note
that S5 has also an application to the satisfiability problem of fragments of the
µ-calculus: the satisfiability problem of the so-called existential (or box-free) µ-
calculus on arbitrary graphs is as difficult as the same problem on S5 graphs. By
using this observation we give an alternative proof of a result of [13] to the effect
that the satisfiability problem for the existential µ-calculus is N P -complete. We
also give a proof that satisfiability of µ-calculus in S5 is N P -complete, so in this
respect we have a better complexity than the EXP T IM E complexity the full
µ-calculus. Both results depend on a linear size model property for µ-calculus
formulas in S5.
1.1 Related work
Given the relevance of S5 as epistemic logic, many papers in the modal logic
literature are dedicated to it, and in particular on its proof theory. Finding a
good axiom system for S5 is a longstanding open problem, see [19]. The situation
is even more difficult for the modal µ-calculus in S5, where a recent contribution
is [1].
2 Syntax
2.1 Scalar modal µ-calculus
We present here the usual modal µ-calculus, and we call it scalar because, as we
will see, there is also a vectorial version of the µ-calculus. We follow the standard
presentation of the formulas of modal µ-calculus:
φ = A | ¬A | X | φ ∨ φ | φ ∧ φ | h iφ | [ ]φ | µX.φ | νX.φ,
where A ranges over a set At of atoms and X ranges over a set V ar of fixpoint
variables. h i and [ ] denote the modal operators: the diamond, or the existential
operator, and the box, or the universal operator.
Intuitively, µX.φ(X) denotes the least fixpoint of the function φ(X), and
νX.φ(X) denotes the greatest fixpoint of this function.
A µ-calculus formula φ is called guarded if for every fixpoint subformula of
φ, say νX.ψ(X) or µX.ψ(X), every occurrence of X in ψ is in the scope of a
modal operator.
Free and bound variables are defined in analogy with first order logic, be-
cause fixpoints µX and νX are syntactically analogous to quantifiers ∃x and
∀x (note however that semantically, fixpoint variables correspond to monadic
second order variables, i.e. variables ranging over sets, rarther than first order
variables ranging over individuals).
A µ-calculus formula is called a sentence if it has no free variables. Although
formulas are not closed under negation, a negation of sentences is available: the
negation of a sentence is obtained by exchanging A and ¬A, ∧ and ∨, h i and
[ ], and µ with ν.
Given a formula φ, we denote by |φ| the size of φ.
2.2 Functional µ-calculus
We can generalize modal µ-calculus to functional µ-calculus, following [3]. Func-
tional µ-calculus has n-ary function symbols, to be interpreted by monotonic
functions on powersets (or more generally, on complete lattices). The syntax is
X|φ ∧ ψ|φ ∨ ψ|f (φ1 , . . . , φn )|µX.φ|νX.φ.
2.3 Vectorial µ-calculus
The most standard presentation of modal µ-calculus is in the scalar syntax of
the previous section. In this section we generalize the syntax by allowing systems
of equations: although this extension does not affect the expressiveness of the
logic, it may increase succinctness.
We essentially follow the presentation of [3]. We restrict to powersets rather
than arbitrary complete lattices. So we can consider a set V and n monotonic
functions f1 , . . . , fn from P (V )n+m to P (V ). A µ-system is a system S of n
equations
x1 =θ1 f1 (x1 , . . . , xn , y1 , . . . , ym )
S: ...
xn =θn fn (x1 , . . . , xn , y1 , . . . , ym )
where θ1 , . . . , θn ∈ {µ, ν}.
The µ-system S is by definition equivalent to a n tuple of scalar µ-calculus
formulas, called the solution of S, computed inductively as follows.
If n = 1 then the solution is θx1 .f1 (x1 , y1 , . . . , ym ).
If n > 1, let g1 (x2 , . . . , xn , y1 , . . . , ym ) = θ1 x1 .f1 (x1 , . . . , xn , y1 , . . . , ym ). The
solution of S is (g1 (h2 , . . . , hn , y1 , . . . , ym ), h2 , . . . , hn ), where (h2 , . . . , hn ) is the
solution of the system
x2 =θ2 f2 (g1 (x2 , . . . , xn , y1 , . . . , ym ), . . . , xn , y1 , . . . , ym )
S1 : ...
xn =θn fn (g1 (x2 , . . . , xn , y1 , . . . , ym ), . . . , xn , y1 , . . . , ym )
We denote by soli (S) the i-th component of the solution of S.
A µ-system of equations is called a modal µ-system if all functions fi are
combinations of variables, atoms, negated atoms, conjunctions, disjunctions, di-
amonds, and boxes.
The modal µ-calculus vectorial model checking problem is: given a finite
graph G and a modal µ-system S, decide whether G satisfies sol1 (S).
2.4 The LEF T relation
Given a µ-system S, we define a relation LEF T between the variables of S as
follows.
Let y, z two variables of S. We say that y is at left of z, written y LEF T z,
if there is an equation of S where y is the variable at the left hand side of the
equality and z occurs at the right hand side.
A modal µ-system is called a modal system if the LEF T relation on variables
is acyclic. Every modal system is equivalent to a formula of modal logic.
2.5 Composition
Let φ(X) be a formula containing a free variable X and let ψ be a sentence. Then
the composition φ[X/ψ] is the formula obtained by replacing X everywhere with
ψ in φ. Note that ψ is a sentence, hence there is no variable capturing.
The usual notion of composition of formulas can be extended to µ-systems
as follows.
Let S be a µ-system. The scope of a left variable y in S is the set of all
variables z such that there is a LEF T path from y to z.
Let S, T be two systems where the variables at left of S and T are disjoint.
Let A be an atom of S. Then the composition of S and T is the system obtained
by concatenating the equations of S and of T and by replacing A with the left
variable of the first equation of T . Composition is possible only without capture,
i.e. T must not have free variables y such that some occurrence of A is in the
scope of y in S.
2.6 Vectorial alternation depth hierarchy
We define the vectorial hierarchies V EC −Σn , V EC −Πn , V EC −∆n as follows.
V EC − Σ0 = V EC − Π0 are the modal systems. V EC − Σn+1 is the closure of
V EC − Πn under composition and adding a µ equation as a first equation of the
system. V EC −Πn+1 is the closure of V EC −Σn under composition and adding a
ν equation as a first equation of the system. V EC−∆n = V EC−Σn ∩V EC−Πn .
The alternation depth of a system S is the least n such that S is in V EC −∆n+1 .
3 Semantics and related concepts
3.1 Graphs and models
Like it is usually done for modal logic, we give Kripke semantics to the µ-calculus
by using the notion of model.
A graph (also called frame) is a pair G = (V, E), where V is a set of vertices
and E is a binary edge relation on V .
A graph G = (V, E) is called total if E = V 2 , i.e., all possible edges are
present.
A path in a graph G from a vertex x to a vertex y is a finite sequence of
vertices z1 , . . . , zn such that z1 = x, zn = y and zi Ezi+1 for every i < n.
A point y is reachable from a point x if there is a path from x to y.
A model is a pair (G, Col), where G is a graph and Col is a coloring function
from some domain D to the powerset of V .
3.2 Bisimulation
Intuitively, bisimulation between models indicates that the two models have the
same observable behavior. Formally, we can define a bisimulation between two
models (G, Col) and (G0 , Col0 ) as a relation B ⊆ V (G) × V (G0 ) such that,
whenever (xBx0 ):
– x ∈ Col(d) if and only if x0 ∈ Col0 (d) for every d ∈ D;
– if xEy, then there is y 0 such that x0 E 0 y 0 and yBy 0 ;
– if x0 E 0 y 0 , then there is y such that xEy and yBy 0 .
We say that two pointed colored graphs (G, Col, x) and (G0 , Col0 , x0 ) are bisimilar
if and only if there is a bisimulation B such that xBx0 .
3.3 Special classes of graphs
We consider a few subclasses of graphs.
A graph (V, E) is called total if E = V 2 , that is, all possible edges are present.
The class K4 is the class of all (vertex colored) graphs whose relation is
transitive. The class S5 is the class of all (vertex colored) graphs whose relation
is an equivalence relation. Since equivalence relations are reflexive, symmetric
and transitive, S5 is included in K4 (as a class of graphs). The names K4 and
S5 come from the modal logic literature.
We also speak of total models, K4 models and S5 models in the obvious
sense.
Note that every total graph belongs to S5. Moreover, for every S5 model
M and every vertex x of M , there is a total model M 0 containing x such that
(M, x) and (M 0 , x) are bisimilar: in fact M 0 is the submodel of M given by all
points of M reachable from x.
Moreover, every S5 model M is bisimilar to a S5 graph M 0 , colored in the
same way, where every two different points have different colors: in fact, M 0 is M
modulo the equivalence relation of having the same color, and the bisimulation
is the projection function.
3.4 Semantics
The semantics of µ-calculus extends the usual Kripke semantics for modal logic.
So, to give semantics to the µ-calculus, we must consider models of the form
M = (G, V al) where G = (V, E) is a graph and V al is a valuation function from
At ∪ V ar to the powerset of V . To each model M and each formula φ we can
associate a subset ||φ||M of V , defined in this way:
– ||A||M = V al(A) and ||¬A||M = V \ V al(A) if A is an atom;
– ||X||M = V al(X);
– ||φ ∨ ψ||M = ||φ||M ∪ ||ψ||M ;
– ||φ ∧ ψ||M = ||φ||M ∩ ||ψ||M ;
– ||h iφ||M is the set of all elements of V having some successor in ||φ||M ;
– ||[ ]φ||M is the set of all elements of V having every successor in ||φ||M ;
– ||µX.φ(X)||M is the smallest set S ⊆ V such that S = ||φ||M [X := S],
where M [X := S] is obtained from M by letting V al(X) = S;
– ||νX.φ(X)||M is the greatest set S ⊆ V such that S = ||φ||M [X := S].
The last two items are well defined since the map sending S to ||φ||M [X := S]
is a monotonic function on the powerset of V and so, by the Knaster-Tarski
Theorem, this map has both a least and a greatest fixpoint.
We also say that a vertex v of a model M verifies a formula φ, written
M, v |= φ, if v ∈ ||φ||M .
4 Parity games
4.1 Definition
It is notoriously difficult to understand µ-calculus formulas, especially when
there are many alternating fixpoints. A means to understand the µ-calculus is
given by parity games. We will see that the semantics of µ-calculus formulas can
be given in terms of parity games.
Intuitively, a parity game is a game where two players, called c and d, move
in a graph (the notation, due to Arnold, suggests that c means conjunctive
and d means disjunctive). The vertexes of the graph are labeled with finitely
many positive integers. d wants to have many high even numbers along the play,
whereas c wants to have many odd numbers.
Let us define parity games more formally. A parity game is a structure Γ =
(Vc , Vd , E, v0 , Ω), where Vc and Vd are disjoint sets, E is a binary relation on
Vc ∪ Vd , v0 ∈ Vc ∪ Vd is the initial vertex, and Ω : Vc ∪ Vd → {1, . . . , n} is the
priority function; the number n is called the index of the game.
A play of Γ is a sequence of vertices, starting from v0 , where the successor
of the current vertex must be an E-successor of that vertex, and this successor
is chosen by the player d, if the vertex is in Vd , and by c if the vertex is in Vc .
If the play reaches a position where either player has no moves, the other
wins. If this never happens, then the play is infinite, and d wins if the greatest
priority occurring infinitely often is even, and c wins otherwise.
A strategy of a player p is a function which, given an initial segment of a
play ending with a p- position, determines the next move of p. A strategy is
positional if the move depends only on the last vertex of the segment.
A strategy Σ of a player p is winning if every play where p moves according
to Σ is won by p.
Note that parity games are Borel games, so by Borel determinacy, see [17],
they enjoy determinacy: there is always one of the two players who has a winning
strategy.
A well known property of parity games is positional determinacy:
Theorem 1. (See [9], Theorem 4.4) If either player has a winning strategy in
a parity game, then it has a positional winning strategy.
However in this paper we will use a slightly stronger form of determinacy.
Let us call a strategy strongly positional if the move on a position depends only
on the successors of the position (not on the position itself). Clearly, a strongly
positional strategy is positional, but the converse does not hold: if two different
nodes have the same successors, a stronlgy positional strategy gives the same
answer on the two nodes, whereas a positional one need not to.
Now a careful analysis of [9] gives the following strenghtening of the previous
theorem:
Corollary 1. If either player has a winning strategy in a parity game, then it
has a strongly positional winning strategy.
Proof. Note that players c and d are called AN D and OR in [9]. The successor
of an OR position in the positional strategy of Theorem 4.4 of [9] is chosen in a
way which does not quite depend on the OR position, but depends only on the
set of positions reachable in one step from that OR position. So, the resulting
strategy is actually strongly positional. t
u
4.2 From the µ-calculus to parity games
The semantics of the µ-calculus can be given in terms of a parity game. More
precisely, given a sentence φ and a model M = (V, E, V al), with a distinguished
vertex v0 of V , we can define an evaluation game Γ (φ, v0 , M ) as follows (we
consider sentences rather than arbitrary formulas for simplicity).
The positions of Γ (φ, v0 , M ) are the pairs (ψ, v), where v ∈ V and ψ is a
subformula of φ. The d positions are the pairs of the form (ψ ∨ χ, v) or (h iψ, v);
all other positions are c positions. (φ, v0 ) is the initial position.
There are edges from (ψ ∨χ, v) or (ψ ∧χ, v) to (ψ, v) and (χ, v); from (h iψ, v)
or ([ ]ψ, v) to (ψ, w) for every successor w of v in V ; from (µX.ψ, v) and (νX.ψ, v)
to (ψ, v); and if a variable occurrence X appears in a subformula µX.ψ or νX.ψ,
there is an edge from (X, v) to (µX.ψ, v) or (νX.ψ, v) respectively. Finally, we
put also an edge from (A, v) or (¬A, v) to itself for every atom A, and from (Y, v)
to itself for every variable Y free in φ.
To define the Ω function we proceed as follows. First we assign priorities to
fixpoint subformulas of φ: we assign to each greatest fixpoint subformula νX.χ
in φ a priority 2|χ|, and we assign to µX.χ a priority 2|χ| + 1. This ensures that:
– least fixpoints have odd priority;
– greatest fixpoints have even priority;
– the priority of larger subformulas is larger.
Now we let Ω(ψ, v) be the priority of ψ, if ψ is a fixpoint formula; Ω(A, v) = 2
if M, v |= A and Ω(A, v) = 1 otherwise, if A is an atom, a negated atom or a
free variable of φ; and Ω(ψ, v) = 1 otherwise.
It results that M, v0 |= φ if and only if player d has a winning strategy in
Γ (φ, v0 , M ).
4.3 From parity games to µ-calculus
We have seen that in a sense, µ-calculus reduces to parity games. However, as is
well known, also the other way round is true: if we consider parity game of index
n as a graph vertex-colored by c, d, 1, . . . , n, then there is a µ-calculus formula
Wn , due to Walukiewicz, such that an arena for parity games (G, v0 ) verifies Wn
if and only if player d has a winning strategy in the parity game associated to
(G, v0 ). This formula is
^ ^
Wn = µX1 νX2 . . . θXn .(d → h i (i → Xi ) ∧ (c → [ ] (i → Xi ).
i i
5 The reduction to S5
In [13] there is a reduction of µ-calculus model checking to box free µ-calculus
model checking. Here we modify the result by specializing to S5 and by referring
to the vectorial model checking rather than the scalar one:
Theorem 2. Given a finite model M and a modal µ-system S, there is a finite
S5 model M 0 and a box free modal µ-system S 0 , such that M 0 and S 0 are built
in time polynomial in the size of M plus the size of S, and such that M verifies
sol1 (S) if and only if M 0 verifies sol1 (S 0 ).
Proof. Let M = (V, E, V al) be a model. Let S be a modal µ-system. Up to
perform a polynomial time rewriting of S, we can suppose that the equations
of S have one of the following forms: X = A, X = ¬A where A is an atom,
X = Y ∨ Z, X = Y ∧ Z, X = h iY , X = [ ]Y , X = Y .
Now M 0 is obtained as follows. The vertices of M 0 are the vertices of M . Let
us enumerate these vertices as v1 , . . . , vn . Let Ai be an atom which is true in G’
only in the point vi . The relation E 0 of M 0 holds for every pair of vertices of M 0 ,
so M 0 is an S5 model.
Moreover S 0 is obtained by replacing every equation of S of the form
X = h iY
with _
X= {Ai ∧ h i(Aj ∧ Y )|vi Rvj },
and every equation of S of the form
X = [ ]Y
with ^
X= {Ai → h i(Aj ∧ Y )|vi Rvj }.
Note that one could expect that the right handV side of X = [ ]Y is replaced
by the De Morgan dual of X = h iY , so to have {Ai → [ ](Aj → Y )|vi Rvj }.
However, the atoms Ai are interpreted as singletons, so
[ ](Aj → Y )
is in fact equivalent to its De Morgan dual
h i(Aj ∧ Y ),
and this allows us to replace the box with the diamond.
t
u
We do not know whether Theorem 2 can be specialized to the scalar µ-
calculus. In fact, the problem is that the translation from a modal µ-system to
a single formula of the modal µ-calculus (i.e., the algorithm which builds the
solution of a modal µ-system) takes exponential time in general.
6 Corollaries
It is well known that there is a translation of vectorial µ-calculus in S5 to
vectorial modal logic in S5. In fact, given a modal µ-system in S5, we can first
consider its solution and translate it into modal logic. From the previous theorem
we obtain:
Corollary 2. If there is a polynomial time computable translation from box-
free vectorial µ-calculus in S5 to vectorial modal logic in S5, then the vectorial
µ-calculus model checking problem is in P .
Proof. By [16], model checking for vectorial modal logic (over arbitrary graphs)
reduces in polynomial time to the problem of solving Boolean equation systems
with only one type of fixpoint, and this problem is in P by [3]. By the previous
theorem, vectorial model checking reduces to vectorial model checking over S5
in polynomial time; so if the translation in the statement exists, then by a chain
of reductions, the vectorial µ-calculus model checking problem is in P . t
u
Considerations analogous to S5 hold in the larger class of graphs K4. In fact,
from [2], [6] and [5] it follows that there is a translation from vectorial µ-calculus
in K4 to V EC − Π2 in K4. From the previous theorem we obtain:
Corollary 3. If there is a polynomial time computable translation from vecto-
rial µ-calculus in K4 to V EC − Π2 in K4, then the µ-calculus model checking
problem is in P .
Proof. Every S5 graph is also a K4 graph, so by the previous theorem, there
is a polynomial time reduction from vectorial model checking over arbitrary
graphs to vectorial model checking in K4. Moreover, by [16], model checking for
V EC − Π2 (over arbitrary graphs) reduces in polynomial time to the problem
of solving Boolean equation systems of class Π2 , and this problem is in P by [3].
So if the translation in the statement exists, then by a chain of reductions, the
vectorial µ-calculus model checking problem is in P .
t
u
7 Satisfiability in S5
In this section we investigate the µ-calculus satisfiability problem for S5. We
begin with establishing a linear size model property.
Lemma 1. If a formula φ has a S5 model, then it has a S5 model of size linear
in φ.
Proof. Let (M, x0 ) be a S5 model of φ. Up to bisimulation we can suppose that
M is total. Then player d has a winning strategy in the game Γ (φ, x0 , M ). By
Corollary 1, d has a strongly positional winning strategy in the game, call it Σ.
Consider a diamond position (h iψ, y) of the game. Since M is total, the set of
successors of (h iψ, y) does not depend on y, so the choice of Σ also does not
depend on y, but only on ψ. Let us denote by (ψ, xψ ) the successor position of
(h iψ, y) chosen by Σ. Let N be the submodel of M given by x0 plus all points
xψ .
First, N has size linear in φ because its size is at most the number of diamond
subformulas of φ (plus one). Moreover, we note that if player c in the game always
chooses elements of N in box positions, then the game remains in N forever, and
is won by d since Σ is winning on M .
t
u
As a consequence we have:
Theorem 3. The satisfiability problem for the µ-calculus in S5 is N P -complete.
Proof. N P -hardness holds because the µ-calculus contains propositional logic.
To show that the problem is in N P , suppose that models and formulas are en-
coded as strings in a convenient finite alphabet (e.g. ASCII code). We prove that
there is a problem S in P T IM E and a polynomial p such that φ is satisfiable in
S5 iff there exists a witness z such that (φ, z) ∈ S and length(z) ≤ p(length(φ)).
Since µ-calculus model checking is in N P (see [7]), we know that there exists a
problem S 0 in P T IM E and a polynomial q such that, for any finite model M , M
satisfies φ iff there exists a y with (M, φ, y) ∈ S 0 and length(y) ≤ q(length(M ) +
length(φ)). Moreover, by Lemma 1, φ is satisfiable in S5 iff φ is satisfiable in a
model M of size linear in φ, which we can code with a length at most r(length(φ))
for some polynomial r.
Let S be the set of tuples (φ, M, y) such that:
– M is an S5 model (i.e. the accessibility relation is an equivalence);
– (M, φ, y) ∈ S 0 ;
– length(M ) ≤ r(length(φ));
– length(y) ≤ q(length(M ) + length(φ)).
So, φ is satisfiable in S5 if and only if there exists a witness z = (M, y) such that
(φ, z) ∈ S. Note that S is in P T IM E. Moreover, (φ, z) ∈ S implies length(z) ≤
p(length(φ)), where p(x) = r(x) + q(r(x) + x). So, φ is satisfiable in S5 if and
only if there exists a witness z = (M, y) such that (φ, z) ∈ S and length(z) ≤
p(length(φ)). So S and p satisfy the desired properties.
t
u
Note that the restriction of the previous theorem to modal logic was already
known, see [11].
8 On existential µ-calculus
A formula of the µ-calculus is called existential, or box-free, if it contains no
box operators [ ]φ. Intuitively, existential µ-calculus is considerably simpler
than general µ-calculus. In fact, the satisfiability problem for the µ-calculus
is EXP T IM E-complete, whereas, as shown in [13], the same problem for the
existential µ-calculus is N P -complete. Note that this last result can be obtained
in a way different from [13] as follows.
First we observe:
Lemma 2. The satisfiability problem for existential µ-calculus is polynomial
time equivalent to the same problem on S5.
Proof. If an existential formula φ has a model M , then φ is also true on the
reflexive, symmetric, transitive closure of M , which is an S5 graph of the same
size as M .
t
u
Moreover, as a corollary of the previous section we have:
Corollary 4. The satisfiability problem for existential µ-calculus in S5 is N P -
complete.
Proof. The satisfiability problem for existential µ-calculus in S5 is N P because,
by Theorem 3, it is a particular case of an N P problem. Moreover, the problem
is N P -hard because existential µ-calculus contains propositional logic. t
u
From the previous lemma and the previous corollary it follows:
Corollary 5. The satisfiability problem for existential µ-calculus is N P -complete.
9 On µ-calculus and modal logic in S5
It is known that µ-calculus in S5 is as expressive as modal logic, so in S5 there
is no fixpoint alternation hierarchy. In this section we describe two translations
from µ-calculus to modal logic; the first is due to Alberucci and Facchini, whereas
the second is based on a bisimulation argument.
9.1 On the complexity of translations from the µ-calculus to modal
logic over S5
In [2] a recursive translation of µ-calculus into modal logic in S5 is given. The
construction is performed by induction on ordinals (rather than ordinary induc-
tion on numbers). In order to set up the construction, a notion of ordinal rank
of µ-calculus formulas is introduced, with the following properties:
– rank(A) = rank(¬A) = 1;
– rank(h iφ) = rank([ ]φ) = rank(φ) + 1;
– rank(φ ∧ ψ) = rank(φ ∨ ψ) = max{rank(φ), rank(ψ)} + 1;
– rank(µX.φ(X)) = rank(νX.φ(X)) = sup{rank(φn (X)) + 1; n ∈ IN}.
A µ-calculus sentence φ is well named if it is guarded and, for any variable
X, no two distinct occurrences of fixpoint operators in φ bind X, and the atom
X occurs only once in φ.
Using the semantical laws µX.ψ(X, X) = µX.µY.ψ(X, Y ), νX.ψ(X, X) =
νX.νY.ψ(X, Y ) (see [3]), and renaming of bounded variables, we see that any
µ-calculus formula is equivalent to a well named formula of a size which is linear
in the size of φ. For instance, the formula µX([ ]X ∧ h iX) ∧ νX[ ]X is equivalent
to the well named formula µXµY ([ ]X ∧ h iY ) ∧ νZ[ ]Z.
The following translation t from well named µ-formulas to modal logic in S5
can be defined:
– t(A) = A, t(¬A) = ¬A;
– t(true) = true, t(f alse) = f alse;
– t(h iφ) = h it(φ);
– t([ ]φ) = [ ]t(φ);
– t(φ ∧ ψ) = t(φ) ∧ t(ψ);
– t(φ ∨ ψ) = t(φ) ∨ t(ψ);
– t(µX.φ(X)) = t((φ(φ(f alse))∗ );
– t(νX.φ(X)) = t((φ(φ(true))∗ ),
where (φ(φ(f alse))∗ , (φ(φ(true))∗ denote the well named formulas obtained from
φ(φ(f alse)), φ(φ(true)) by renaming repeated bound variables. The translation
t is given by induction on the rank, so it is well defined. Moreover:
Lemma 3. If φ is a well named formula, then the length of t(φ) is at most 2|φ| .
Proof. We need a preliminary composition lemma:
Lemma 4. t(φ[X/ψ]) = t(φ)[X/t(ψ)].
Proof. By induction on φ. t
u
Now the bound as in the lemma can be proved by induction on the rank of
φ. The most delicate case is µX.ψ(X) and νX.ψ(X). Now, by Lemma 4, we
have t(µX.ψ(X)) = t(ψ(ψ(f alse)) = t(ψ)[X/t(ψ(f alse))], and since X oc-
curs only once in ψ, we obtain the bound |t(µX.ψ)| = |t(ψ)[X/t(ψ(f alse))]| ≤
2|t(ψ(f alse))| ≤ 2 × 2|ψ(f alse)| = 2|ψ(f alse)|+1 ≤ 2|µX.ψ(X)| . The case of ν is
analogous. t
u
So, the translation t is at most exponential. We also can show that the
exponential upper bound for the translation t is tight. In fact, consider the well
named formulas:
φn = µX1 . . . µXn .X1 ∨ (X2 ∨ . . . ∨ Xn ).
We can show by induction that t(φn ) has size at least 2n . In fact, the base case
n = 1 is true; for the inductive case, we begin with a lemma:
Lemma 5. The following equivalences hold:
– |t(φ(f alse ∨ α))| > |t(φ(α)|;
– if X is a variable free in φ, then |t(φ(X ∨ α))| > |t(φ(α)|.
Proof. By induction on φ. t
u
Now consider t(φn ) with n > 1. By definition of t we have
t(φn ) = t(µX2 . . . µXn .(µX2 . . . µXn .f alse ∨ X2 ∨ . . . ∨ Xn ) ∨ X2 . . . ∨ Xn )
and by Lemma 4 we obtain
t(φn ) = t(µX2 . . . µXn .Y ∨ X2 . . . ∨ Xn )[Y /t(µX2 . . . µXn .f alse ∨ X2 ∨ . . . ∨ Xn ).
By evaluating the sizes we see that
|t(φn )| ≥ |t(µX2 . . . µXn .Y ∨X2 . . .∨Xn )|+|t(µX2 . . . µXn .f alse∨X2 ∨. . .∨Xn )]|−1;
by Lemma 5 we obtain
|t(φn )| ≥ 2|t(µX2 . . . µXn .X2 ∨ . . . Xn )|,
and, by renaming the variables,
|t(φn )| ≥ 2|t(φn−1 )|.
Finally, the inductive hypothesis gives |t(φn−1 )| ≥ 2n−1 , so |t(φn )| ≥ 2n .
9.2 An alternative translation
A translation from µ-calculus to modal logic different from [2] is obtained as
follows. Let φ be a µ-calculus formula containing a set At of atoms. Then, up to
bisimulation, there are finitely many S5 models colored with At, more precisely
exponentially many of them. Each bisimulation class is described by a character-
istic formula, that is, the conjunction of h iγ where γ is a conjunction of atoms
and negated atoms present in the model of the class, and ¬h iγ where γ is a
conjunction not present in the class. So, φ is equivalent to the disjunction of the
characteristic formulas of the bisimulation classes of the models of φ. Note that
this alternative translation is also (at most) exponential.
9.3 A corollary
Both translations of the previous subsections give an exponential blow up in the
size of the formula. It is then natural to ask whether there exists a polynomial
time computable translation from the µ-calculus to modal logic over S5. This
question is related to the results of the previous section, as the following final
corollary shows:
Corollary 6. If there is a polynomial time computable translation from the µ-
calculus to modal logic over S5 and Theorem 2 specializes to scalar µ-calculus,
then the µ-calculus model checking problem is in P .
Proof. Given a µ-formula φ and a model M , first reduce the problem to a µ-
formula φ0 over an S5 model M 0 , and then apply the polynomial translation in
order to obtain a modal formula φ∗ with
M |= φ ⇔ M 0 |= φ∗ .
Since both M 0 and φ∗ are obtained in polynomial time from M, φ and modal
model checking is in P , we have done. t
u
10 Conclusion
In this paper we have investigated some aspects of µ-calculus on S5 graphs.
Arguably, these graphs are quite simple. However, simplicity of S5 graphs gives
us better satisfiability bounds than arbitrary graphs, but not better bounds on
the model checking problem.
An interesting question is whether there is a direct, natural translation from
modal µ systems to modal systems in S5: by this we mean that the translation
should not go through transforming a system of equations into a single scalar
term.
A similar analysis of µ-calculus model checking and satisfiability could be
carried over other important classes of graphs. An example is K4. Since satisfi-
ability in K4 efficiently reduces to general satisfiability, in K4 we have the same
bound as in K, that is, EXP T IM E. It would be interesting to see whether a
better bound can be given. Note that for model checking, as we have seen, a
better bound for K4 with respect to arbitrary graphs does not exist.
The same analysis could be done for other interesting classes of graphs, e.g.
the longstanding Gödel-Löb class GL (i.e. the transitive wellfounded graphs),
or for more recent classes such as graphs of bounded tree width or classes with
forbidden minors. A good model checking algorithm for bounded tree width is
e.g. [18], but we do not have yet a polynomial time model checking algorithm
on graphs of bounded tree width. Apparently there is no result on satisfiability
on bounded tree width.
Acknowledgments
This work has been partially supported by the PRIN project n. 20089M932N
Innovative and multi-disciplinary approaches for constraint and preference rea-
soning.
References
1. L. Alberucci, Sequent Calculi for the Modal µ-Calculus over S5. J. Log. Comput.
19(6): 971–985 (2009).
2. L. Alberucci and A. Facchini, The modal µ-calculus hierarchy over restricted classes
of transition systems, J. Symb. Logic 74 (2009) 1367–1400.
3. A. Arnold and D. Niwinski, Rudiments of µ-calculus, North-Holland, 2001.
4. Edmund M. Clarke, Jr., Orna Grumberg and Doron A. Peled, Model Checking,
MIT Press, 1999.
5. A. Dawar and M. Otto, Modal characterisation theorems over special classes of
frames, Ann. Pure Appl. Logic 161 (2009), 1–42.
6. G. D’Agostino and G. Lenzi, On the µ-calculus over transitive and finite transitive
frames, Theor. Comput. Sci. 411(50): 4273–4290 (2010).
7. E. Allen Emerson: Model Checking and the Mu-calculus. Descriptive Complexity
and Finite Models 1996: 185–214.
8. E. A. Emerson and C. S. Jutla, The complexity of tree automata and logics of
programs. In Proc. 29th IEEE FOCS 328–337 (1988).
9. E. A. Emerson and C. S. Jutla. Tree Automata, Mu-Calculus and Determinacy
(Extended Abstract). FOCS 1991: Pages 368–377.
10. Robert S. Streett and E. Allen Emerson. An Automata Theoretic Decision Proce-
dure for the Propositional Mu-Calculus. Information and Computation 81 (1989),
249–264.
11. R. Fagin, Reasoning about knowledge, MIT Press, 2003.
12. M. J. Fischer and R. E. Ladner, Propositional dynamic logic of regular programs,
J. Comput. System Sci., 18 (1979), pp. 194–211.
13. Thomas A. Henzinger, Orna Kupferman, and Rupak Majumdar, On the Univer-
sal and Existential Fragments of the Mu-Calculus, Theoretical Computer Science
354:173-186, 2006.
14. M. Jurdzinski, Deciding the winner in parity games is in U P ∩ co − U P , Inform.
Proc. Letters 68 (1998), 119-124.
15. D. Kozen, Results on the Propositional mu-Calculus, Theor. Comput. Sci. 27: 333–
354 (1983).
16. A. Mader, Verification of Modal Properties using Boolean Equation Systems, Ph.
D. Thesis, 1997.
17. D. A. Martin, Borel determinacy, Ann. Math., 102 (1975), pp. 363–371.
18. J. Obdrzalek, Fast Mu-Calculus Model Checking when Tree-Width Is Bounded.
CAV 2003, 80–92.
19. F. Poggiolesi, A cut-free simple sequent calculus for modal logic S5, Review of
Symbolic Logic, 1:3–15, 2008.
20. I. Walukiewicz, Completeness of Kozen’s Axiomatisation of the Propositional Mu-
Calculus, Information and Computation 157 (2000), 142–182.