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?
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)]$.
