# CTL* and mu-calculus

it is well known that the modal $\mu$-calculus is one of the most expressive temporal logics for expressing properties of trees/graphs, and that CTL* is strictly less expressive than the $\mu$-calculus.

Here I would like to ask for an example of $\mu$-calculus formula, as simple as possible, that is not expressible in CTL*, and hopefully for an explaination of its meaning (fixed-point formulas quickly become unreadable). Any good reference for a "concrete" simple example would also be great!

Take a path property that is not first-order expressible, e.g. $$\nu x.p\wedge\Diamond\Diamond x$$ which says that there exists a path where the atomic proposition $p$ holds at every even position, and any valuation can be used on odd positions.
• @LORE81: the $p$ at even positions'' example is a classic, that you can find for instance in the paper by Wolper pointed by @DaveBall in his question. It is not too difficult to prove directly by induction on LTL formulae; alternatively, you can construct the transition monoid and see that it is not aperiodic; finally you can try an Ehrenfeucht-Fraïssé argument, though it's long to spell out in full detail. – Sylvain Jan 22 '13 at 20:13