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 acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Browse other questions tagged or ask your own question.