The question is about an operator that transforms any CTL* formula ${\psi}$ into a (not necessarily equivalent) LTL formula ${A\psi^d}$, where $d$ means syntactically removing all $A,E$ quantifiers from ${\psi}$.

Is it true that this operator preserves logical equality, i.e. ${\psi_1}\equiv_{CTL*}{\psi_2}\implies {A\psi_1^d}\equiv_{LTL}{A\psi_2^d}$ ?

  • $\begingroup$ That's a tricky one. I would suggest looking at the paper "The Common Fragment of ACTL and LTL" by Mikołaj Bojańczyk, where he shows that LTL $\cap$ CTL is not the same as LTL $\cap$ ACTL. The example language that he uses may be suitable for showing that your conjecture does not hold. $\endgroup$
    – DCTLib
    Jun 4, 2018 at 11:29
  • $\begingroup$ @DCTLib I don't think that your suggested approach would work, as if a CTL* formula $\psi$ is LTL definable, then $\psi$ is equivalent to $A\psi^d$. This result is showed in "Expressibility Results for Linear-Time and Branching-Time Logics" by Clarke and Draghicescu. I think this implies that the statement by OP holds if $\psi_1$ is LTL definable, doesn't it? $\endgroup$
    – SimonJ
    Jun 7, 2018 at 6:45
  • $\begingroup$ @SimonJ the statement does hold for ${\psi_1}$ that is LTL expressible, where ${\psi_2}$ is the LTL equivalent. I wondered if this is also correct for the general case where ${\psi_2}$ is not in LTL, or even ${\psi_1}$ is not LTL expressible. $\endgroup$ Jun 8, 2018 at 9:29


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.