2
$\begingroup$

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?

Improve this question
$\endgroup$
1
  • $\begingroup$ 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.) $\endgroup$ – Simon Bliudze Sep 21 '16 at 10:06
1
$\begingroup$

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

Improve this answer
$\endgroup$
1
  • 2
    $\begingroup$ 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. $\endgroup$ – Simon Bliudze Sep 21 '16 at 9:47
0
$\begingroup$

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

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.