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?
Why use $\mu$-calculus and not LTL,CTL,CTL*?
logic;simulation;linear temporal logic;mu calculus;computation tree logic