patternMinor
Why use $\mu$-calculus and not LTL,CTL,CTL*?
Viewed 0 times
whycalculusltlctlandusenot
Problem
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?
(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?
Solution
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".
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".
Context
StackExchange Computer Science Q#16603, answer score: 9
Revisions (0)
No revisions yet.