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.
http://dx.doi.org/10.1109/SFCS.2000.892332
- 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 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
,
AX φ1
,
(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."
A
(after pushing negations to the atomic propositions) then there is an LTL equivalent. However, this does not work. ConsiderAF AG p
. If there were an LTL equivalent, it would have to beF G p
. However, this latter is not expressible in CTL. (Thanks also to @Shaull.) $\endgroup$ – Simon Bliudze Sep 21 '16 at 10:06