# Constructing automata with the same traces, but where a CTL-formula is not equally satisfied [closed]

Hard to put this question in a short title. As part of a self-exercise, I'm trying to solve 6.15b of Principles of Model Checking by Baier and Katoen. You're supposed to prove that there does not exist an equivalent LTL formula for the CTL formula $\phi = A\Diamond E\bigcirc A\Diamond \neg a$, without the theorem that says that you can remove all A's and E's.

It is hinted to me that if I can construct two automata $A$ and $A'$ such that $\textrm{Traces}(A) = \textrm{Traces}(A')$, but where $A \models \phi$ and $A' \not\models \phi$, I'm practically done. (Assume $\psi$ is an LTL formula with $\psi \equiv \phi$, then $A\models\psi\iff A'\models\psi$. This is a contradiction, which proves there is no LTL equivalent.)

Now, how to construct such automata? Currently I'm basically constructing simple automata that satisfy $\phi$, but all the variants with similar traces also appear to satisfy $\phi$.

Kinds regards.

One example of such automata is as follows. The first, $A_1$, consists of two states $q,s$, where $L(q)=a$ and $L(s)=\neg a$ ($L$ being the labeling function). $q$ has a transition to $q$ and to $s$, and $s$ has only a self loop.
The second,$A_2$ consists of 4 states $q_1,...,q_4$ with the following transitions: $$q_1\to q_2\vee q_3$$ $$q_2\to q_2$$ $$q_3\to q_3\vee q_4$$ $$q_4\to q_4$$ And the labels are: $L(q_1)=L(q_2)=L(q_3)=a$ and $L(q_4)=\neg a$.
It is easy to see that the traces of both automata are exactly $a^\omega \cup a^*\cdot a\cdot (\neg a)^\omega$, but path $q_1,q_2^\omega$ makes it so that $A_2\not\models \phi$, whereas $A_1\models \phi$.
By the way, you can remove $q_3$ from $A_2$, but I find it clearer this way.