Take the 2-minute tour ×
Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It's 100% free, no registration required.

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?

share|improve this question
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. –  Kaveh Jan 22 '13 at 18:56
Migrating to Computer Science. –  Dave Clarke Jan 23 '13 at 5:57
Why do you say that formula is not a CTL formula? What is your CTL language definition (BNF)? –  Pål GD Jan 23 '13 at 12:35
add comment

migrated from cstheory.stackexchange.com Jan 23 '13 at 5:57

This question came from our site for theoretical computer scientists and researchers in related fields.

1 Answer

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

share|improve this answer
add comment

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.