Syntactic characterisation of the intersection of CTL and LTL The Baier and Katoen textbook references this paper


  E. M. Clarke and I. A. Draghicescu. Expressibility results for
  linear-time and branching-time logics, pages 428–437. Springer Berlin
  Heidelberg, Berlin, Heidelberg, 1989.


to say that, given a CTL formula P, if there exists an equivalent LTL one, it can be obtained by dropping all branch quantifiers (i.e. A and E) from P. 

Is there a syntactic criterion that provides a guarantee that if a CTL formula passes the test, then an equivalent LTL formula does exist?
Note that by "equivalent", we actually need to interpret LTL over trees. Thus, we say that a CTL formula $\phi$ is equivalent to an LTL formula $\psi$, if $\phi$ is equivalent to the CTL* formula $A\psi$.

Thus, we essentially compare LTL and CTL in the common grounds of CTL*.

Given this, it's not hard to construct a procedure to check the equivalent. Simply check whether the formula $\phi \iff A\psi$ is a tautology in CTL*. This can be done in 2EXPTIME. However, since satisfiability of CTL is only EXPTIME complete, it might be possible to reduce this to EXPTIME (but I haven't given it much thought).