-1
$\begingroup$

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.

$\endgroup$

closed as off-topic by Vijay D, David Eppstein, Kaveh Dec 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.

0
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Thanks! But how does one systematically get to this? $\endgroup$ – Bla Blaat May 7 '13 at 17:07
  • $\begingroup$ Like most things in math (and indeed - life), there is no systematic solution :) (to my knowledge, anyway) $\endgroup$ – Shaull May 7 '13 at 17:19

Not the answer you're looking for? Browse other questions tagged or ask your own question.