How to show that ECTL* is more expressive than CTL* $\cup$ Büchi (with an example) I am looking for a preferably simple property that is expressible in ECTL* but not in CTL* and not in Büchi, with a citable reference to the proof.



Details of what I've tried:

I've tried a modification of Wolper's even-property: the property $Eeven$ that holds for every Kripke structure containing a path where p holds at least in every even state. The ECTL* formula $E (\mathcal{A}_{even}(p))$ specifies $Eeven$ (with $\mathcal{A}_{even}$ being the Büchi automaton that accepts words where p holds at least in every even state). 

Because of the existential path quantifier, $E (\mathcal{A}_{even}(p))$ is trivially not expressible in Büchi. 

But is there a short proof that $E (\mathcal{A}_{even}(p))$ is not in CTL*? Or a reference to a proof (of any length)? 
After looking at Computation Tree Logic and Regular $\omega$-Languages, Wolfgang Thomas, 1989, I can think of a proof showing $Eeven$ is counting - but that would definitely not be a short proof :( Would using $Eeven$ is not star-free or $M(Eeven)$ is not group-free be any easier?
I think the simpler example is your property, which can be written for instance $E(((a+b)a)^\omega))$.
A simple way to show that is is not in CTL* is to show that this would imply that the word language $((a+b)a)^\omega$ is in LTL (because CTL* on linear structures is LTL). 

This fact is a classical result.
To show it, it suffices (for instance) to use the theorem stating LTL&lt;=>aperiodic $\omega$-semigroup. So we just need to compute the minimal $\omega$-semigroup of this language, and observe that it contains the group $\mathbb{Z}/2\mathbb{Z}$, so it is not aperiodic.