I have a CTL* formula: $\mathsf{EF}[p\land \mathsf{AX}[q\ \mathsf{U}\ r]]$ but in my application, I am limited to CTL. To my understanding, this formula is no valid CTL and I wonder whether I can transform it (preserving semantic, of course). The CTL* formula should express "there exists a path on which $p$ holds and from that point, in all subsequent states, $q$ holds until $r$ eventually holds".

Is this correct and is there a way to convert it to CTL?

  • $\begingroup$ Welcome to cstheory, a Q&A site for research-level questions in theoretical computer science (TCS). Your question does not appear to be a research-level question in TCS. Please see the FAQ for more information on what is meant by this. Your question might be suitable for Computer Science which has a broader scope. $\endgroup$
    – Kaveh
    Jan 22, 2013 at 18:56
  • $\begingroup$ Migrating to Computer Science. $\endgroup$ Jan 23, 2013 at 5:57
  • $\begingroup$ Why do you say that formula is not a CTL formula? What is your CTL language definition (BNF)? $\endgroup$
    – Pål GD
    Jan 23, 2013 at 12:35

1 Answer 1


A somewhat late response:

The formula $AX(p U q)$ is equivalent to the CTL formula $AXA(pUq)$: Consider a state that satisfies the former, then in all the paths from it, after one transition it holds that $pUq$. Thus, in all the paths after one transition, we reach a state from which all the paths satisfy $p U q$, so the state satisfies the latter. The converse is obvious, sine the second formula is harder to satisfy.

So an equivalent CTL formula is $EF[p\wedge AXA(pUq)]$.


Your Answer

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