1
$\begingroup$

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?

Improve this question
$\endgroup$
3
  • $\begingroup$ A similar question has also been asked here in the $\mu$-calculus context. $\endgroup$
    – DaveBall aka user750378
    Jan 22, 2013 at 19:54
  • $\begingroup$ 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 $\endgroup$
    – Denis
    Jan 23, 2013 at 12:05
  • $\begingroup$ @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\}$). $\endgroup$
    – DaveBall aka user750378
    Jan 23, 2013 at 14:33

1 Answer 1

Reset to default
4
$\begingroup$

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.

Improve this answer
$\endgroup$
4
  • $\begingroup$ 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. $\endgroup$
    – Sylvain
    Jan 24, 2013 at 19:24
  • $\begingroup$ @myself: actually it's not so clear given the section "details of what I tried" in the question... $\endgroup$
    – Sylvain
    Jan 24, 2013 at 19:31
  • $\begingroup$ what does the omega superscript mean? $\endgroup$
    – panny
    Jul 7, 2013 at 14:45
  • $\begingroup$ 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$ $\endgroup$
    – Denis
    Jul 7, 2013 at 17:46

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.