# 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?

• A similar question has also been asked here in the $\mu$-calculus context. – DaveBall aka user750378 Jan 22 '13 at 19:54
• what do you mean when you say "not in Buchi" ? Do you mean that there is no nondeterministic Buchi tree automaton for the language ? p – Denis Jan 23 '13 at 12:05
• @dkuper, sorry for the imprecision: I meant a classic nondet. Büchi automaton $\mathcal{A}$ and acceptance lifted from linear properties to branching time by universal path quatification (like it's usually done for LTL): $\mathcal{A}$ accepts a Kripke structure $\mathcal{K}$ iff $\mathcal{A}$ accepts all infinite paths in $\mathcal{K}$ (which corresponds to the ECTL* formula A$\mathcal{A}(p_1,..,p_n)$ with $\Sigma = \{p_1,...,p_n\}$). – DaveBall aka user750378 Jan 23 '13 at 14:33

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<=>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.
• it means "repeated infinitetely many times". $a^\omega$ is the infinite word $aaaaa\dots$, and $(a+b)^\omega$ is any infinite word with letters in $\{a,b\}$. In the example $((a+b)a)^\omega$ is any infinite word with the letter $a$ on all even positions, for instance $aababaaaaabaaaba\dots$ – Denis Jul 7 '13 at 17:46