<p>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...</p>

<p>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.</p>

<p>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$.</p>

<p>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$.</p>

<p>By the way, you can remove $q_3$ from $A_2$, but I find it clearer this way.</p>

CC BY-SA 3.0
2013-05-07T17:07:56.923Z
Thanks! But how does one systematically get to this?
Bla Blaat
CC BY-SA 3.0
2013-05-07T17:19:16.310Z
Like most things in math (and indeed - life), there is no systematic solution :) (to my knowledge, anyway)
Shaull
CC BY-SA 3.0
2013-05-07T16:59:17.310Z
2013-05-07T16:59:17.310Z
Shaull
<p>Hard to put this question in a short title. As part of a self-exercise, I'm trying to solve 6.15b of <em>Principles of Model Checking</em> 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.</p>

<p>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.)</p>

<p>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$.</p>

<p>Kinds regards.</p>

<lo.logic><automata-theory><model-checking><linear-temporal-logic>
Constructing automata with the same traces, but where a CTL-formula is not equally satisfied
Bla Blaat
# Constructing automata with the same traces, but where a CTL-formula is not equally satisfied

(Asked by: username_0 on 2013-05-07)

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.

**Tags:** lo.logic, automata-theory, model-checking, linear-temporal-logic


---

## 1 answers

### Answer by username_1 on 2013-05-07. Score: 0 | Accepted answer

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.

> **Comments:**
> **username_0**: Thanks! But how does one systematically get to this?  
> **username_1**: Like most things in math (and indeed - life), there is no systematic solution :) (to my knowledge, anyway)  

---

