What is the relationship between the expressiveness of LTL, Bchi/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 Bchi but not in CTL*? Do you have a good example?How about in Bchi 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 Bchi-property, given, e.g., in [Wolper83] 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 Bchi-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 Bchi automata, resulting in: Let $\phi$ be a CTL* state formula. Then $\phi$ is expressible via Bchi automaton          iff $\phi$ is equivalent to $A\phi^d$.With this, Bchi $\cap$ CTL* = LTL, answering my questions above:Is it true that there are properties specifiable in Bchi but not in CTL*? Yes, e.g. evenness.How about in Bchi and CTL but not in LTL? No.Has anyone lifted Clarke and Draghicescu's theorem already to Bchi 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 Bchi automata?
Expressiveness of Bchi vs CTL(*)
lo.logic;automata theory;model checking;temporal logic
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 Bchi 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).