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.
Constructing automata with the same traces, but where a CTL-formula is not equally satisfied
lo.logic;automata theory;model checking;linear temporal logic
SPOILER ALERT: Since you ask this in TCS, I assume you want the answer and not hints. If you don't want the full answer, don't continue reading...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.