Consider the $\text{CTL}^*$ formula $E[pU(qUr)]$.

It is not hard to show that it is equivalent to the $\text{CTL}$ formula $E[pU(EqUr)]$.

The informal reason is that a path where $p$ is true until $qUr$ is true is the same as a finite branch where $p$ is true along it, followed (concatenated with) by a path (starting at a son of the last state of the former branch) along which $qUr$ is true.

However, consider now the $\text{CTL}^*$ formula $A[pU(qUr)]$, here I have a problem in pushing the $A$ inside, because the $\text{CTL}$ formula $A[pU(AqUr)]$ is "stronger" than the former.

The reason is that in the former we demand that any branch contains a state starting from which $qUr$ is true. While, the latter formula demands that any branch contains a state such that any computation starting from it has $qUr$ true.

How can I still convert $A[pU(qUr)]$ to $\text{CTL}$?


Your Answer

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

Browse other questions tagged or ask your own question.