8
$\begingroup$

It is known that the temporal logics LTL,CTL,CTL* can be translated/embedded into the $\mu$-calculus. In other words, the (modal) $\mu$-calculus subsumes these logics, (i.e. it is more expressive.)

Could you please explain/point me to papers/books that elaborate on this matter. In particular, are there concrete fairness, liveness, etc. properties not expressible in the temporal logics but in the $\mu$-calculus?

$\endgroup$
7
$\begingroup$

As for a $\mu$-calculus formula not expressible in CTL*, see this post.

As for texts on the subject, you are likely to get further ahead by reading papers, as these topics are not covered in many books. Still, the Handbook of Modal Logic may be a good start.

As for papers, try:

Expressive power of Temporal Logics

This PhD thesis

Emerson's Model checking and the Mu Calculus

And there are many more. Just google terms like "expressive power", "mu calculus" and "temporal logics".

$\endgroup$
  • $\begingroup$ Thanks for the example and suggestions. Could you please suggest any relevant papers? I remember seeing some in the past but have hard time locating them now... $\endgroup$ – Dimiter Oct 31 '13 at 19:28
  • $\begingroup$ Added papers to the answer. $\endgroup$ – Shaull Oct 31 '13 at 19:35
  • $\begingroup$ There is a book on modeling with mCRL2 now (for a rough idea of its content, see the book announcement). $\endgroup$ – reinierpost Jan 23 '15 at 17:24
4
$\begingroup$

The $\mu$-calculus is strictly more expressive than LTL, CTL and CTL*. This is a consequence of a few different results.

The first step is to show that the $\mu$-calculus is as expressive as temporal logics. The main idea for encoding these logics comes from recognizing temporal properties as fixed points. At a very informal level, least fixed points allow you to express properties of a finitary nature and greatest fixed points apply to infinitary properties. For example, eventually $\varphi$ in LTL defines that there is an instant in the finite future at which $\varphi$ is true, while always $\varphi$ states that $\varphi$ is true at an infinite number of future time-steps. In terms of fixed points the eventually property would be expressed using a least fixed point and the always property using a greatest fixed point. Following such an intuition temporal operators can be encoded as fixed point operators.

The next step is to show that the $\mu$-calculus is more expressive. The main idea is alternation depth. Fixed points alternate if a least fixed point influences the greatest fixed point, and vice-versa. The alternation depth of a $\mu$-calculus formula counts the number of alternations that occur in it. The operators in CTL can be encoded by $\mu$-calculus formulae with alternation depth $1$. The operators in CTL* and LTL can be encoded by $\mu$-calculus formulae with alternation depth at most $2$. However, the alternation hierarchy of the $\mu$-calculus is strict, which means that increasing alternation depth in a formula allows you to express strictly more properties. This is why people say the $\mu$-calculus is more expressive than these temporal logics.

Some references:

  1. The initial arguments that the $\mu$-calculus subsumes several logics appears in Modalities for Model Checking:Branching Time Logic Strikes Back, Emerson and Lei, 1985.
  2. The translation of CTL into the $\mu$-calculus is straightforward. You can find it in the book on Model Checking by Clarke, Grumberg and Peled. You can also find it in Model Checking and the $mu$-calculus by Emerson or in Ken McMillan's dissertation.
  3. The translation of CTL* into the $\mu$-calculus is involved. Rather than the original, indirect translation, I suggest the paper of Mads Dam on Translating CTL* into the modal mu-calculus.
  4. There is a simpler translation of LTL into what is called the linear-time $\mu$-calculus, in which the modalities operate over traces and not states. See Axiomatising Linear Time Mu-calculus by Roope Kaivola.
  5. The alternation hierarchy is studied in The modal mu-calculus alternation hierarchy is strict by Julian Bradfield and in A hierarchy theorem for the $\mu$-calculus by Giacomo Lenzi.

All this is about expressivity not about utility. In practice, people don't usually specify properties as $\mu$-calculus expressions because they might find temporal logics easier to work with. The industrial specification languages differ from both temporal logics and the $\mu$-calculus in their syntax and their expressive power.

$\endgroup$
  • $\begingroup$ Thank you for a great answer! Regarding your comment on utility: suppose I want to use a μ-calculus model checker, but specify things in temporal logics, which is easier. Is there a technique (even better, a tool) that automatically translates formulae in any of these logics (CTL,CTL* or LTL) to the μ-calculus? Thanks! $\endgroup$ – Dimiter Nov 20 '13 at 7:15
  • $\begingroup$ SMV internally translates CTL into $\mu$-calculus. Not sure what tool explicitly does this. $\endgroup$ – Vijay D Nov 20 '13 at 8:41
2
$\begingroup$

It is well known that $\mu$-calculi can express properties that "count modulo a constant", e.g., "all even steps visit a $A$-state" which is captured by something like $\mu X.A \land\Box\Box X$. Such properties cannot be stated with the standard TL modalities Until and Next since these modalities are 1st-order definable. See D. C. Kozen's 1983 article.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.