17
$\begingroup$

I am looking for an easy example of two transition systems that are LTL equivalent, but not trace equivalent.

I have read the proof of Trace Equivalence being finer than LTL Equivalence in the book "Principles of Model Checking" (Baier/Katoen) but I'm not sure I really understand it. I am unable to picture it, is there maybe a simple example that can visualize the difference?

$\endgroup$
  • 3
    $\begingroup$ Might I recommend expanding the acronym in the title. This will help others find the question and answers and might also help bring your question to the attention of those who can provide good responses. $\endgroup$ – Marc Hamann Apr 3 '11 at 19:01
  • 1
    $\begingroup$ not to mention google searches :) $\endgroup$ – Suresh Venkat Apr 3 '11 at 19:20
  • 5
    $\begingroup$ @Marc: Using the acronym LTL is absolutely standard - modal logicians like their brief names (think B, D4.3, KL, &c.). I think the title shouldn't be expanded, given that we have the tag. $\endgroup$ – Charles Stewart Apr 4 '11 at 6:44
  • 1
    $\begingroup$ The question is still not very well defined: are you allowing infinite Kripke structures? Do you consider mixed (maximal) finite and infinite traces, or only allow infinite ones? I am asking because AFAICR Baier & Katoen only consider the case of finite Kripke structures and infinite traces, which rule out Dave's answer below. $\endgroup$ – Sylvain Apr 4 '11 at 14:12
  • 1
    $\begingroup$ @atticae: with finite total Kripke structures (and thus infinite traces), I'd expect LTL equivalence and trace equivalence to be the same thing... I'll think about it. $\endgroup$ – Sylvain Apr 6 '11 at 8:41
9
+50
$\begingroup$

Reading Baier and Katoen closely, they are considering both finite and infinite transition systems. See page 20 of that book for definitions.

First, take the simple transition system $EVEN$:

EVEN

Lemma: No LTL formula recognizes the language $L_{even} = $Traces$(EVEN)$. A string $c \in L_{even}$ iff $c_i = a$ for even $i$. See Wolper '81. You can prove this by first showing that no LTL formula with $n$ "next-time" operators can distinguish the strings of the form $p^i\neg p p^\omega$ for $i> n$, by a simple induction.

Consider the following (infinite, non-deterministic) transition system $NOTEVEN$. Note that there are two different initial states:

enter image description here

Its traces are precisely $\{a,\neg a\}^\omega - L_{even}$.

Corollary to the Lemma: If $NOTEVEN \vDash \phi$ then $EVEN \not\vDash \neg\phi$

Now, consider this simple transition system $TOTAL$:

Total TS

Its traces are clearly $\{a,\neg a\}^\omega$.

Thus, $NOTEVEN$ and $TOTAL$ are not trace equivalent. Suppose they were LTL inequivalent. Then we would have an LTL formula $\phi$ such that $NOTEVEN \vDash \phi$ and $TOTAL \not\vDash \phi$. But then, $EVEN\vDash \neg\phi$. This is a contradiction.

Thanks to Sylvain for catching a stupid bug in the first version of this answer.

$\endgroup$
  • $\begingroup$ Hmm, this isn't perfectly clear. Should I make the steps around the contradiction more explicit? The transition systems also aren't as pretty as they could be... $\endgroup$ – Mark Reitblatt Apr 10 '11 at 4:15
  • $\begingroup$ You are mis-interpreting the $L_\text{even}$ language: the system you are proposing is equivalent to the formula $a\wedge\mathsf{G}((a\to\mathsf{X}\neg a)\wedge(\neg a\to\mathsf{X}a))$. The correct system should have a nondeterministic choice in the initial, $a$-labeled state $q_0$ between going to a state $q_1$ labeled by $a$ and one $q_2$ not labeled by $a$. Both $q_1$ and $q_2$ have transitions returning to $q_0$. $\endgroup$ – Sylvain Apr 10 '11 at 19:00
  • $\begingroup$ @Sylvain you are correct. I tried to simplify, and I ended up breaking it! Let me fix that up. $\endgroup$ – Mark Reitblatt Apr 10 '11 at 21:03
  • $\begingroup$ Can't you "reverse" the argument, so that the two systems you compare in the end are $\mathit{EVEN}$ and $\mathit{TOTAL}$ instead of $\mathit{NOTEVEN}$ and $\mathit{TOTAL}$? $\endgroup$ – Sylvain Apr 11 '11 at 14:35
  • 1
    $\begingroup$ @Mark Reitblatt: From what do you reason that sentence in the end "But then, $EVEN\vDash \neg\phi$."? I cannot see an argumentation that leads to that point, which is essential to show the contradiction. $\endgroup$ – magnattic May 12 '12 at 14:49
3
$\begingroup$

If your LTL definition includes the "next" operator, then the following applies. You have two sets of traces $A$ and $B$ . Let $b$ be any finite prefix of a trace in $B$. $b$ must also be a finite prefix of a trace in $A$, because otherwise you can convert this to a formula that is just a series of next-operators that detects the difference. Therefore every finite prefix of a $B$-word needs to be a finite prefix of an $A$-word and vice versa. This means that if $A \not= B$, there needs to be a word in $b$ so that all its finite prefixes appear in $A$ but $b$ in itself does not appear in $A$. If $A$ and $B$ are generated by finite transition systems I think this is impossible. Assuming infinite transition systems, you can define

$A = \{a,b\}^\omega$ and $B = A \setminus \{w\}$ where $w$ is e.g. the infinite word $aba^2b^2a^3b^3a^4b^4\cdots$.

Any LTL formula that holds universally for $A$ will hold universally for $B$ because $B$ is a subset of $A$. Any LTL formula that holds for $B$ also holds for $A$; for the sake of contradiction, assume not, but that $\varphi$ holds for every element of $B$ (i.e. for every element of the universe expect for the word $w$) but not for $w$. Then $\neg\varphi$ evaluates to true on $w$ but not on any other word of the universe (and LTL is closed under negation), and there is no LTL formula that can be true only for $w$ as every Buchi automaton that accepts only one infinite word must be strictly cyclic whereas $w$ is not.

$\endgroup$
  • $\begingroup$ Those are finite traces. Assuming you extend them to infinite traces with $a^\omega$ at the end, the formula $\neg (b\wedge X (b \wedge X G a))$ accepts the second set but rejects the first. $\endgroup$ – Mark Reitblatt Apr 8 '11 at 20:51
  • $\begingroup$ You're right, I wrote a new answer :) LOL, I remembered from my days in theoretical cs that LTL doesn't have the next operator :) $\endgroup$ – antti.huima Apr 9 '11 at 4:29
  • $\begingroup$ I think this does the trick. $\endgroup$ – Dave Clarke Apr 9 '11 at 9:02
  • $\begingroup$ I think it works too. $\endgroup$ – Mark Reitblatt Apr 9 '11 at 16:07
  • $\begingroup$ This answer isn't satisfactory. The OP was asking for transition systems, but the answer is about languages and justified in terms of Buchi automata and $\omega$-regular languages, which aren't in the text referenced. $\endgroup$ – Mark Reitblatt Apr 9 '11 at 23:34

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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