# 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.

## closed as off-topic by Vijay D, David Eppstein, KavehDec 1 '13 at 19:06

This question appears to be off-topic. The users who voted to close gave this specific reason:

• "Your question does not appear to be a research-level question in theoretical computer science. For more information about the scope, please see help center. Your question might be suitable for Computer Science which has a broader scope." – Vijay D, David Eppstein, Kaveh
If this question can be reworded to fit the rules in the help center, please edit the question.

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.