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

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

CC BY-SA 3.0
2013-01-24T19:24:01.907Z
Though I find your answer perfectly relevant, I think the goal of the original question when asking for a non-Büchi example was to avoid linear properties.
Sylvain
CC BY-SA 3.0
2013-01-24T19:31:52.200Z
@myself: actually it's not so clear given the section "details of what I tried" in the question...
Sylvain
CC BY-SA 3.0
2013-07-07T14:45:22.050Z
what does the omega superscript mean?
panny
CC BY-SA 3.0
2013-07-07T17:46:04.713Z
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
CC BY-SA 3.0
2013-01-24T16:57:34.437Z
2013-01-24T16:57:34.437Z
Denis
<p>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.</p>

<hr>

<p>Details of what I've tried:</p>

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

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

<p>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 <a href="http://dx.doi.org/10.1007/BFb0013041" rel="nofollow">Computation Tree Logic and Regular $\omega$-Languages, Wolfgang Thomas, 1989</a>, 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?</p>

CC BY-SA 3.0
2013-01-22T19:54:59.440Z
A similar question has also been asked [here in the $\mu$-calculus context](http://cstheory.stackexchange.com/questions/16164/ctl-and-mu-calculus).
DaveBall aka user750378
CC BY-SA 3.0
2013-01-23T12:05:45.913Z
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
CC BY-SA 3.0
2013-01-23T14:33:28.447Z
@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
<lo.logic><automata-theory><model-checking><temporal-logic><linear-temporal-logic>
How to show that ECTL* is more expressive than CTL* $\cup$ Büchi (with an example)
DaveBall aka user750378
# How to show that ECTL* is more expressive than CTL* $\cup$ Büchi (with an example)

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

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](http://dx.doi.org/10.1007/BFb0013041), 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?

**Tags:** lo.logic, automata-theory, model-checking, temporal-logic, linear-temporal-logic

> **Comments:**
> **username_0**: A similar question has also been asked [here in the $\mu$-calculus context](http://cstheory.stackexchange.com/questions/16164/ctl-and-mu-calculus).  
> **username_1**: 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  
> **username_0**: @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\}$).  

---

## 1 answers

### Answer by username_1 on 2013-01-24. Score: 4 | Accepted answer

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.

> **Comments:**
> **username_2**: Though I find your answer perfectly relevant, I think the goal of the original question when asking for a non-Büchi example was to avoid linear properties.  
> **username_2**: @myself: actually it's not so clear given the section "details of what I tried" in the question...  
> **username_3**: what does the omega superscript mean?  
> **username_1**: 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$  

---

