Expressiveness of Büchi vs CTL(*)

Question

What is the relationship between the expressiveness of LTL, Büchi/QPTL, CTL and CTL*?

Can you give some references that cover as many of these temporal logics as possible (especially between linear- and branching-time)?

A Venn diagram with those temporal logics and some practical properties as examples would be perfect.

---

For instance:

• Is it true that there are properties specifiable in Büchi but not in CTL*? Do you have a good example?
• How about in Büchi and CTL but not in LTL?

---

Details:

The expressiveness of the logics is more relevant for me than the examples. The latter is just helpful for understanding and motivation.

I already know of the expressibility theorem between CTL* and LTL from [Clarke and Draghicescu, 1988], but do not like the usual example of fairness being in CTL and not in LTL since there are a plethora of fairness variants, some of which are expressible in LTL.

I also do not like the usual example of the evenness Büchi-property, given, e.g., in [[Wolper83]][5] about the restrictions of LTL, since adding another propositional variable would solve the problem ($even(p) \equiv q \wedge \Box ( q \implies X \neg q ) \wedge \Box ( \neg q \implies X q ) \wedge \Box ( q \implies p )$).

I do like the example of the evenness Büchi-property, given, e.g., in [Wolper83] about the restrictions of LTL, since it is simple and shows the necessity of PQTL for evenness (thanks for the note below).

---

Update:

I think the expressibility theorem between CTL* and LTL from [Clarke and Draghicescu, 1988] can be lifted to Büchi automata, resulting in:

Let $\phi$ be a CTL* state formula. 
Then $\phi$ is expressible via Büchi automaton 
         iff $\phi$ is equivalent to $A\phi^d$.

With this, Büchi $\cap$ CTL* = LTL, answering my questions above:

• Is it true that there are properties specifiable in Büchi but not in CTL*? Yes, e.g. evenness.
• How about in Büchi and CTL but not in LTL? No.

Has anyone lifted Clarke and Draghicescu's theorem already to Büchi automata, or stated a similar theorem? Or is this too trivial to be mentioned in a paper, since CTL*'s path quantifiers are obviously "orthogonal" to the criteria on accepted paths states by Büchi automata?

Answer 1

One thing we have to be clear on is the kind of property we are talking about: CTL and CTL* are branching-time logics, used to talk about tree languages, whereas LTL is a linear-time logic, which per se talks about words, but can be applied to trees by requiring all branches to satisfy the formula.

This already gives you a hint for some CTL properties which LTL cannot express, namely ones which mix universal and existential path quantifiers, like AGEFp ("It will always be possible to get to a p-state"). The usual example in the other direction is FGa, see for example http://blob.inf.ed.ac.uk/mlcsb/files/2010/02/mlcsb7.pdf for details (and a Venn diagram).

Regarding automata, things get more complicated. You could be talking about word or tree automata; if the latter, note that Büchi automata are less expressive than the other acceptance conditions (Rabin/parity/...) in this case. See for example http://www.cs.rice.edu/~vardi/papers/lics96r1.ps.gz for comparisons (including the case of derived languages, which are the tree languages recognizable by word automata).

Answer 2

I'm not answering the full question but only part of it (I have no interest in branching time).

Your definition of $\mathit{even}$ would better read $\mathit{even}(p) \equiv \exists q.(q \land \Box ( q \leftrightarrow \mathsf{X} \lnot q ) \land \Box ( q \rightarrow p ))$. You are introducing $q$ only to remember if you are on an odd or even position, but this $q$ information is not on your system so it should not be a free variable of your formula (otherwise your system and your formula are defined on different alphabets). Such a formula is an Existentially-Quantified LTL formula (EQLTL for short).

EQLTL formula can only have $\exists$ quantifiers at the top-level. And they are as expressive as Büchi automata. For instance to translate the EQLTL formula $\exists q.(q \land \Box ( q \leftrightarrow \mathsf{X} \lnot q ) \land \Box ( q \rightarrow p ))$ as a Büchi automaton, you would simply translate the LTL formula $q \land \Box ( q \leftrightarrow \mathsf{X} \lnot q ) \land \Box ( q \rightarrow p )$, and then erase the $q$ variable from everywhere in the automaton. Conversely any Büchi automaton can be converted into an EQLTL formula easily: declare an existential variables for all the states $\exists s_1.\exists s_2\ldots$, and use these to encode transitions and acceptance states (e.g. $\exists s_1.\exists s_2.(s_1\land\Box(s_1\rightarrow a\land \mathsf{X}s_2)\land\Box(s_2)\rightarrow b\land\mathsf{X}(s_1))\land\Box\Diamond s_2\land\Box(\bigwedge_i (s_i\rightarrow\bigwedge_{j\ne i}\neg s_j)))$ if $s_1$ can go to $s_2$ with $a$, $s_2$ can go to $s_1$ with $b$, and $s_2$ is Büchi-accepting; the last conjunction of implications make sure you cannot be in two states at once). You might want to read Stutter-Invariant Languages, ω-Automata, and Temporal-Logic on this subject.

Basically the $\exists q$ is used here like some second-order quantifier (there exist a set of states where $q$ hold and such that...). EQLTL and Büchi automata are equalivent to S1S, and LTL is equalivent to F1S. $even$ is the typical S1S formula that cannot be expressed by F1S.

QPTL, which you mentioned, adds $\exists$, $\forall$ (not only at the top-level), and past operators. It contains EQLTL but is not more expressive (since QPTL can be converted to Büchi automata and Büchi automata can be converted to EQLTL).

CTL is about branching time, so it's a different world. A CTL formula like $\mathsf{EF}\mathsf{AG}p$ which is reasoning on the tree of all possible futures have now equivalent in LTL which is reasoning on all possible scenarios.