<p>I have posted the same question on <a href="https://www.researchgate.net/post/Is_there_a_syntactic_criterion_on_CTL_formulae_that_guarantees_the_existence_of_an_equivalent_LTL_formula" rel="nofollow">ResearchGate</a> and got pointers to two very interesting papers&mdash;thanks to <a href="http://forsyte.at/people/konnov/" rel="nofollow">Igor Konnov</a> and <a href="http://www.cs.aub.edu.lb/pa07/" rel="nofollow">Paul Attie</a>. I will summarise here the information from the papers, relevant to the question, but first, here are the two papers:</p>

<ol>
<li>Monika Maidl. "The common fragment of CTL and LTL," Proceedings of the 41st Annual Symposium on Foundations of Computer Science. pp. 643-652, 2000.<br/> <a href="http://dx.doi.org/10.1109/SFCS.2000.892332" rel="nofollow">http://dx.doi.org/10.1109/SFCS.2000.892332</a></li>
<li>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.<br/> <a href="http://dx.doi.org/10.1007/978-3-540-78499-9_13" rel="nofollow">http://dx.doi.org/10.1007/978-3-540-78499-9_13</a></li>
</ol>

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

<p>Maidl considers ACTL&mdash;"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<sup>det</sup>, where "det" stands for "deterministic". ACTL<sup>det</sup> is defined inductively:</p>

<ol>
<li>state predicates are in ACTL<sup>det</sup>;</li>
<li><p>for ACTL<sup>det</sup> formulas φ1 and φ2 and a predicate p, the formulae</p>

<ul>
<li><code>φ1 ∧ φ2</code> ,</li>
<li><code>AX φ1</code>,</li>
<li><code>(p ∧ φ1) ∨ (¬p ∧ φ2 )</code>,</li>
<li><code>A (p ∧ φ1 ) U (¬p ∧ φ2)</code>,</li>
<li><code>A (p ∧ φ1) W (¬p ∧ φ2)</code></li>
</ul>

<p>all belong to ACTL<sup>det</sup>.</p></li>
</ol>

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

<p>In this paper, the class LTL<sup>det</sup> of formulae equivalent to the ACTL<sup>det</sup> 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 <code>¬φ</code> could be recognized by [a] restricted Büchi automaton." He then provides such an algorithm.</p>

<p>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)<sup>∗</sup>a(ab)<sup>∗</sup>c<sup>ω</sup>”, can be defined in CTL but not ACTL." </p>

CC BY-SA 3.0
2016-09-26T16:59:46.207Z
2016-09-26T17:06:50.767Z
2016-09-26T17:06:50.767Z
Simon Bliudze
<p>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$.</p>

<p>Thus, we essentially compare LTL and CTL in the common grounds of CTL*.</p>

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

CC BY-SA 3.0
2016-09-21T09:47:21.123Z
This provides a procedure for checking whether a CTL formula has an LTL equivalent:
1. Take a CTL formula ϕ;  
2. Remove the branch quantifiers to obtain an LTL formula ψ;
3. Check whether ϕ⟺Aψ is a tautology in CTL*.
If yes, then ψ is equivalent to ϕ. However, the question is whether there is a way to characterise (at least some) CTL formulae, for which this will be guaranteed to work. Say, if all branch quantifiers in ϕ are `A` and `some other condition` holds, then ψ as above is guaranteed to be equivalent to ϕ without having to perform the step 3.
Simon Bliudze
CC BY-SA 3.0
2016-09-20T18:20:57.270Z
2016-09-20T18:20:57.270Z
Shaull
<p>The Baier and Katoen textbook references this paper</p>

<blockquote>
  <p>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.</p>
</blockquote>

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

<p>Is there a syntactic criterion that provides a guarantee that if a CTL formula passes the test, then an equivalent LTL formula <em>does exist</em>?</p>

CC BY-SA 3.0
2016-09-21T10:06:55.383Z
The first intuition is that if all the path quantifiers are `A`
(after pushing negations to the atomic propositions) then there is an LTL equivalent. However, this does not work. Consider `AF AG p`. If there were an LTL equivalent, it would have to be `F G p`. However, this latter is not expressible in CTL. (Thanks also to @Shaull.)
Simon Bliudze
<linear-temporal-logic>
Syntactic characterisation of the intersection of CTL and LTL
Simon Bliudze
# Syntactic characterisation of the intersection of CTL and LTL

(Asked by: username_0 on 2016-09-20)

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*?

**Tags:** linear-temporal-logic
> **Comments:**
> **username_0**: The first intuition is that if all the path quantifiers are `A` (after pushing negations to the atomic propositions) then there is an LTL equivalent. However, this does not work. Consider `AF AG p`. If there were an LTL equivalent, it would have to be `F G p`. However, this latter is not expressible in CTL. (Thanks also to @Shaull.)  

---

## 2 answers

### Answer by username_0 on 2016-09-26. Score: 0 | Accepted answer

I have posted the same question on [ResearchGate](https://www.researchgate.net/post/Is_there_a_syntactic_criterion_on_CTL_formulae_that_guarantees_the_existence_of_an_equivalent_LTL_formula) and got pointers to two very interesting papers—thanks to [Igor Konnov](http://forsyte.at/people/konnov/) and [Paul Attie](http://www.cs.aub.edu.lb/pa07/). 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 ACTLdet, where "det" stands for "deterministic". ACTLdet is defined inductively:

1. state predicates are in ACTLdet;
2. 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."


---

### Answer by username_1 on 2016-09-20. Score: 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).

> **Comments:**
> **username_0**: This provides a procedure for checking whether a CTL formula has an LTL equivalent: 1. Take a CTL formula ϕ;   2. Remove the branch quantifiers to obtain an LTL formula ψ; 3. Check whether ϕ⟺Aψ is a tautology in CTL*. If yes, then ψ is equivalent to ϕ. However, the question is whether there is a way to characterise (at least some) CTL formulae, for which this will be guaranteed to work. Say, if all branch quantifiers in ϕ are `A` and `some other condition` holds, then ψ as above is guaranteed to be equivalent to ϕ without having to perform the step 3.  

---

