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:
- Monika Maidl. "The common fragment of CTL and LTL," Proceedings of the 41st Annual Symposium on Foundations of Computer Science. pp. 643-652, 2000.
- 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.
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 ACTLdet, where "det" stands for "deterministic". ACTLdet is defined inductively:
- state predicates are in ACTLdet;
for ACTLdet formulas φ1 and φ2 and a predicate p, the formulae
φ1 ∧ φ2 ,
(p ∧ φ1) ∨ (¬p ∧ φ2 ),
A (p ∧ φ1 ) U (¬p ∧ φ2),
A (p ∧ φ1) W (¬p ∧ φ2)
all belong to ACTLdet.
Furthermore, Maidl makes the following remark: "For an ACTLdet formula φ, [the formula]
A φ W p can be expressed in ACTLdet , since
A φ W p ⇔ A (φ ∧ ¬p) W p. A special case is
AG φ. Similarly,
A φ U p can be expressed in ACTLdet."
In this paper, the class LTLdet of formulae equivalent to the ACTLdet 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."