Syntactic characterisation of the intersection of CTL and LTL

Question

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?

Answer 1

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

Answer 2

I have posted the same question on ResearchGate and got pointers to two very interesting papers—thanks to Igor Konnov and Paul Attie. I will summarise here the information from the papers, relevant to the question, but first, here are the two papers:

1. Monika Maidl. "The common fragment of CTL and LTL," Proceedings of the 41st Annual Symposium on Foundations of Computer Science. pp. 643-652, 2000.
   http://dx.doi.org/10.1109/SFCS.2000.892332
2. Mikołaj Bojańczyk. "The common fragment of ACTL and LTL." International Conference on Foundations of Software Science and Computational Structures. pp. 172-185, 2008.
   http://dx.doi.org/10.1007/978-3-540-78499-9_13

The paper by Monika Maidl does, indeed, provide an answer very much along the lines I was looking for.

Maidl considers ACTL—"the fragment of those CTL formulas that contain, when in negation normal form, only A as a quantifier." She characterises the fragment of ACTL that is expressible in LTL, denoted by ACTL^det, where "det" stands for "deterministic". ACTL^det is defined inductively:

1. state predicates are in ACTL^det;

2. for ACTL^det formulas φ1 and φ2 and a predicate p, the formulae

   • φ1 ∧ φ2 ,
   • AX φ1,
   • (p ∧ φ1) ∨ (¬p ∧ φ2 ),
   • A (p ∧ φ1 ) U (¬p ∧ φ2),
   • A (p ∧ φ1) W (¬p ∧ φ2)

   all belong to ACTL^det.

Furthermore, Maidl makes the following remark: "For an ACTL^det formula φ, [the formula] A φ W p can be expressed in ACTL^det , since A φ W p ⇔ A (φ ∧ ¬p) W p. A special case is AG φ. Similarly, A φ U p can be expressed in ACTL^det."

In this paper, the class LTL^det of formulae equivalent to the ACTL^det ones. is characterised as "[t]hose LTL formulas the negation of which can be represented by a 1-weak Büchi automaton." In the second paper, Mikołaj Bojańczyk argues that this characterisation "was not known to [be] effective, i.e. there was no algorithm that decided if ¬φ could be recognized by [a] restricted Büchi automaton." He then provides such an algorithm.

Furthermore, Bojańczyk provides an example, showing that the common fragment of LTL and CTL is not limited to ACTL: "a very simple LTL property, “all paths belong to (ab)^∗a(ab)^∗c^ω”, can be defined in CTL but not ACTL."