# the conversion of \$ text {CTL} ^ * \$ basic formulas to \$ text {CTL} \$

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

It is not difficult to prove that it is equivalent to $$text {CTL}$$ formula $$E[pU(EqUr)]$$.

The informal reason is that a road where $$p$$ it's true up $$qUr$$ it's true it's the same as a finite branch where $$p$$ it is true along this, followed (concatenated with) by a path (which begins in a child of the last state of the previous branch) along which $$qUr$$ It is true.

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

The reason is that in the first one we demand that any branch contain a state from which $$qUr$$ It is true. Meanwhile, the last formula requires that any branch contain a state such that any computing from it has $$qUr$$ true.

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