9
$\begingroup$

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!

Thank you in advance

|cite|improve this question
$\endgroup$
11
$\begingroup$

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.

|cite|improve this answer
$\endgroup$
  • $\begingroup$ thanks a lot for this simple answer. Could you also suggest a reference supporting this example? Thank you again $\endgroup$ – LORE81 Jan 22 '13 at 8:46
  • $\begingroup$ Nice question & answer (+2). Have a look at cstheory.stackexchange.com/q/16186/6424. I gave the evenness example there too. Maybe some answer will refer to evenness, too. $\endgroup$ – DaveBall aka user750378 Jan 22 '13 at 19:57
  • $\begingroup$ @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. $\endgroup$ – Sylvain Jan 22 '13 at 20:13

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.