Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It only takes a minute to sign up.
Sign up to join this community
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?
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
Emerson's Model checking and the Mu Calculus
And there are many more. Just google terms like "expressive power", "mu calculus" and "temporal logics".
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:
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.
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.
