<p>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.</p>

CC BY-SA 3.0
2013-01-22T08:46:12.727Z
thanks a lot for this simple answer. Could you also suggest a reference supporting this example? Thank you again
LORE81
CC BY-SA 3.0
2013-01-22T19:57:24.163Z
Nice question & answer (+2). Have a look at http://cstheory.stackexchange.com/q/16186/6424. I gave the evenness example there too. Maybe some answer will refer to evenness, too.
DaveBall aka user750378
CC BY-SA 3.0
2013-01-22T20:13:09.670Z
@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
CC BY-SA 3.0
2013-01-21T19:01:06.983Z
2013-01-21T19:01:06.983Z
Sylvain
<p>it is well known that the <a href="http://en.wikipedia.org/wiki/Modal_%CE%BC-calculus">modal $\mu$-calculus</a> is one of the most expressive temporal logics for expressing properties of trees/graphs, and that <a href="http://en.wikipedia.org/wiki/CTL%2a">CTL*</a> is strictly less expressive than the $\mu$-calculus.</p>

<p>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!</p>

<p>Thank you in advance</p>

<lo.logic><model-checking><temporal-logic><mu-calculus>
CTL* and mu-calculus
LORE81
# CTL* and mu-calculus

(Asked by: username_0 on 2013-01-21)

it is well known that the [modal $\mu$-calculus](http://en.wikipedia.org/wiki/Modal_%CE%BC-calculus) is one of the most expressive temporal logics for expressing properties of trees/graphs, and that [CTL\*](http://en.wikipedia.org/wiki/CTL%2a) 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

**Tags:** lo.logic, model-checking, temporal-logic, mu-calculus


---

## 1 answers

### Answer by username_1 on 2013-01-21. Score: 11 | Accepted answer

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.

> **Comments:**
> **username_0**: thanks a lot for this simple answer. Could you also suggest a reference supporting this example? Thank you again  
> **username_2**: Nice question & answer (+2). Have a look at http://cstheory.stackexchange.com/q/16186/6424. I gave the evenness example there too. Maybe some answer will refer to evenness, too.  
> **username_1**: @username_0: 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.  

---

