<p>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 <em>finite</em> transition systems I think this is impossible. Assuming infinite transition systems, you can define</p>

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

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

CC BY-SA 3.0
2011-04-08T20:51:22.517Z
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.
Mark Reitblatt
CC BY-SA 3.0
2011-04-09T04:29:19.103Z
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 :)
antti.huima
CC BY-SA 3.0
2011-04-09T09:02:33.250Z
I think this does the trick.
Dave Clarke
CC BY-SA 3.0
2011-04-09T16:07:10.583Z
I think it works too.
Mark Reitblatt
CC BY-SA 3.0
2011-04-09T23:34:18.840Z
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.
Mark Reitblatt
CC BY-SA 3.0
2011-04-10T01:12:16.073Z
I removed references to $\omega$-regularity. They weren't anyway needed. It is known that there is a Buchi automaton for every LTL formula so I think they can be used as a device. And there was no requirement that the transition systems would be finite. Finite transition systems generate trace sets that are as languages regular. I don't know if LTL equivalence = trace equivalence for trace sets generated by finite transition systems. If I would have to guess I would guess yes.
antti.huima
CC BY-SA 3.0
2011-04-10T01:37:33.080Z
I can construct two Buchi automata that are LTL indistinguishable. It's fairly simple: it's basically the trick you use, but the "outside" language is $\omega$-regular and not LTL expressible. But doing it for transition systems seems to be trickier.
Mark Reitblatt
CC BY-SA 3.0
2011-04-10T08:00:27.547Z
LTL equivalence = trace equivalence for finite transition systems.
Dave Clarke
CC BY-SA 3.0
2011-04-10T17:10:28.840Z
Is LTL equivalence = trace equivalence also for finitely branching transition systems? The solution above can be easily implemented as a transition system if one $\aleph_0$ branch is allowed
antti.huima
CC BY-SA 3.0
2011-04-11T03:21:29.870Z
Well ok Mark's answer also involves an $\aleph_0$ branch so I guess it's settled.
antti.huima
CC BY-SA 3.0
2011-04-08T19:22:16.810Z
2011-04-10T01:08:47.697Z
2011-04-10T01:08:47.697Z
antti.huima
<p>Reading Baier and Katoen closely, they are considering both finite and infinite transition systems. See page 20 of that book for definitions.</p>

<p>First, take the simple transition system $EVEN$: </p>

<p><img src="https://i.sstatic.net/1bvDJ.png" alt="EVEN"></p>

<p>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 <a href="http://portal.acm.org/citation.cfm?id=1382435.1382735" rel="nofollow noreferrer">Wolper '81</a>. 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&gt; n$, by a simple induction.</p>

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

<p><img src="https://i.sstatic.net/MIzoW.png" alt="enter image description here"></p>

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

<p>Corollary to the Lemma: If $NOTEVEN \vDash \phi$ then $EVEN \not\vDash \neg\phi$</p>

<p>Now, consider this simple transition system $TOTAL$:</p>

<p><img src="https://i.sstatic.net/W7rBc.png" alt="Total TS"></p>

<p>Its traces are clearly $\{a,\neg a\}^\omega$.</p>

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

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

CC BY-SA 3.0
2011-04-10T04:15:21.433Z
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...
Mark Reitblatt
CC BY-SA 3.0
2011-04-10T19:00:20.377Z
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$.
Sylvain
CC BY-SA 3.0
2011-04-10T21:03:22.097Z
@Sylvain you are correct. I tried to simplify, and I ended up breaking it! Let me fix that up.
Mark Reitblatt
CC BY-SA 3.0
2011-04-11T14:35:11.717Z
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}$?
Sylvain
CC BY-SA 3.0
2011-04-11T14:48:09.773Z
The formula $a$ distinguishes between $EVEN$ and $NOTEVEN$.
Vijay D
CC BY-SA 3.0
2011-04-11T15:11:39.667Z
@Vijay No, the issue is distinguishing between $TOTAL$ and $NOTEVEN$. Both $EVEN$ and $NOTEVEN$ satisfy the formula $a$. However, incorporating Sylvain's suggestion did break the argument. I needed the "bad" language to be a singleton. I can fix it with a string that counts (not unlike Antti's anwer below), but I don't have time to change it right this moment. And I'd like to stick in full proofs this time so that I don't have any other stupid mistakes.
Mark Reitblatt
CC BY-SA 3.0
2011-04-11T20:01:34.043Z
Ah. I got confused thinking $EVEN$ and $NOTEVEN$ were proposed for equivalence. Does an empty state mean that the state is not labelled $a$? As $NOTEVEN$  has an initial state labelled $\neg a$, it does not satisfy $a$.
Vijay D
CC BY-SA 3.0
2011-04-11T20:08:30.327Z
@Vijay Ahh, you're right. NOTEVEN doesn't satisfy $a$, mea culpa.
Mark Reitblatt
CC BY-SA 3.0
2011-04-11T22:24:14.910Z
The problem with my proof suggestion is I didn't work it out! I see the problem with your answer too. I thought while writing that $TOTAL$ should only satisfy 'true'. Should have followed that through.
Vijay D
CC BY-SA 3.0
2012-05-12T14:49:39.007Z
@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.
magnattic
CC BY-SA 3.0
2011-04-10T03:00:41.260Z
2011-04-10T21:22:34.023Z
2011-04-10T21:22:34.023Z
Mark Reitblatt
<p>I am looking for an easy example of two transition systems that are LTL equivalent, but not trace equivalent.</p>

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

CC BY-SA 2.5
2011-04-03T17:55:32.180Z
thanks for creating the tag, apparently not many questions here regarding this kind of logic
magnattic
CC BY-SA 2.5
2011-04-03T17:57:33.063Z
This is the end of logic I don't know much about, or I would have tried to be more helpful than just fixing the tag. :)
Neel Krishnaswami
CC BY-SA 2.5
2011-04-03T19:01:20.497Z
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.
Marc Hamann
CC BY-SA 2.5
2011-04-03T19:20:50.293Z
not to mention google searches :)
Suresh Venkat
CC BY-SA 2.5
2011-04-04T06:44:30.777Z
@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.
Charles Stewart
CC BY-SA 2.5
2011-04-04T13:38:46.700Z
@Charles Stewart:  I understand that point of view. If we are using LTL as an atomic technical term rather than as an acronym, then it is what it is.  Given the range of topics covered here, though, I still worry about ending up in TLA (three-letter acronym) soup. ;-)
Marc Hamann
CC BY-SA 2.5
2011-04-04T13:47:03.693Z
@atticae @Charles: Let me revise my suggestion based on Charles input. S4, for example, is a well understood term in modal logic, but outside of a specifically ML context I would probably refer to it as "S4 modal logic", or the like.  I wonder if something similar is appropriate here, even if to some it would seem redundant.
Marc Hamann
CC BY-SA 2.5
2011-04-04T14:12:38.570Z
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.
Sylvain
CC BY-SA 2.5
2011-04-04T21:03:48.793Z
@Sylvain: Dave deleted his answer.
Dave Clarke
CC BY-SA 2.5
2011-04-05T22:16:45.760Z
@Sylvain: My apologies, I am still pretty new to the whole field. But as you said, I think I would need an example in the constraints of the book, so finite Kripke stuctures and infinite traces. I didnt even consider infinite Kripke structures, but in the book it clearly says that they are working with Transition Systems without terminal states. Sorry for my english btw. :) I will start a bounty in the hopes for someone to come up with an easy example, if there is one.
magnattic
CC BY-SA 2.5
2011-04-05T22:20:31.450Z
And regarding the abbreviation topic: When searching for the topic in google I also looked for "LTL" instead the whole term. Might just be me though, if you think it should be expanded, feel free to edit the title.
magnattic
CC BY-SA 2.5
2011-04-06T08:41:27.450Z
@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.
Sylvain
CC BY-SA 2.5
2011-04-06T11:23:35.517Z
I would post the proof from the book here, but I guess that would violate copyright or something?
magnattic
CC BY-SA 2.5
2011-04-06T12:07:47.167Z
@atticae: The proof is straightforward, it's the counterexample to the other direction we are struggling with. In short the proof says that if two systems do not satisfy the same LTL formula, then there is one formula satisfied by one system but not by the other. By definition, this means that there is a trace in the first system that satisfies the first formula, but this trace does not occur in the second system. Hence the two systems are not trace equivalent.
Dave Clarke
CC BY-SA 2.5
2011-04-07T22:18:05.500Z
I would guess that if two transition systems satisfy the same LTL formulas, then they are isomorphic, and thus trace equivalent. Two finite structures satisfy the same set of First-order sentences(i.e., formulas without variables) iff they are isomorphic. By Kamp's theorem (See www.cs.toronto.edu/~libkin/csc2428/Lecture7.ps for a proof), LTL is equivalent to FO-logic, in the sense that for every LTL sentence $\varphi$ there is a FO sentence $\phi$ with the same models and vice versa. Thus if two TS are LTL-equiv, they are FO-equiv and thus isomorphic. But I might be missing someth.
Mateus de Oliveira Oliveira
CC BY-SA 2.5
2011-04-07T22:26:20.980Z
Is the author really saying that trace equivalence is strictly finner than LTL equivalence? Corollary 3.18 of the book states: TS is equiv to TS' iff they satisfy the same LT properties, in support of Sylvain's comment. I mean in this case LTL equiv, would also be finer than trace equiv.
Mateus de Oliveira Oliveira
CC BY-SA 3.0
2011-04-08T17:59:50.397Z
@Mateus LT = "Linear Time" properties, that is, sets of traces. It shouldn't be confused with LTL properties, which are specified by LTL formulas. Also, you have to be very careful when you throw around "isomorphic". Isomorphic as what? As first order structures? Does that imply that they are trace equivalent?
Mark Reitblatt
CC BY-SA 3.0
2011-04-10T01:55:28.877Z
@Dave Ok, after reviewing B&K, they consider both infinite and finite transition systems.
Mark Reitblatt
CC BY-SA 3.0
2011-04-11T21:12:31.437Z
@Mateus: Kamp's theorem is for FO with an order relation not FO  over an arbitrary signature. You cannot refer to the edge-relation of the transition system, which is required to specify the structure up to isomorphism.
Vijay D
CC BY-SA 3.0
2011-04-12T05:46:31.767Z
@Vijay, thanks for the explanation. I wasn't sure if there was not a way to express the edge relation of the transition system.
Mateus de Oliveira Oliveira
<lo.logic><model-checking><linear-temporal-logic>
Trace Equivalence vs LTL Equivalence
magnattic
# Trace Equivalence vs LTL Equivalence

(Asked by: username_0 on 2011-04-03)

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?

**Tags:** lo.logic, model-checking, linear-temporal-logic
> **Comments:**
> **username_0**: thanks for creating the tag, apparently not many questions here regarding this kind of logic  
> **username_1**: This is the end of logic I don't know much about, or I would have tried to be more helpful than just fixing the tag. :)  
> **username_2**: 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.  
> **username_3**: not to mention google searches :)  
> **username_4**: @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.  
> **username_2**: @Charles Stewart:  I understand that point of view. If we are using LTL as an atomic technical term rather than as an acronym, then it is what it is.  Given the range of topics covered here, though, I still worry about ending up in TLA (three-letter acronym) soup. ;-)  
> **username_2**: @atticae @Charles: Let me revise my suggestion based on Charles input. S4, for example, is a well understood term in modal logic, but outside of a specifically ML context I would probably refer to it as "S4 modal logic", or the like.  I wonder if something similar is appropriate here, even if to some it would seem redundant.  
> **username_5**: 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.  
> **username_6**: @Sylvain: Dave deleted his answer.  
> **username_0**: @Sylvain: My apologies, I am still pretty new to the whole field. But as you said, I think I would need an example in the constraints of the book, so finite Kripke stuctures and infinite traces. I didnt even consider infinite Kripke structures, but in the book it clearly says that they are working with Transition Systems without terminal states. Sorry for my english btw. :) I will start a bounty in the hopes for someone to come up with an easy example, if there is one.  
> **username_0**: And regarding the abbreviation topic: When searching for the topic in google I also looked for "LTL" instead the whole term. Might just be me though, if you think it should be expanded, feel free to edit the title.  
> **username_5**: @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.  
> **username_0**: I would post the proof from the book here, but I guess that would violate copyright or something?  
> **username_6**: @atticae: The proof is straightforward, it's the counterexample to the other direction we are struggling with. In short the proof says that if two systems do not satisfy the same LTL formula, then there is one formula satisfied by one system but not by the other. By definition, this means that there is a trace in the first system that satisfies the first formula, but this trace does not occur in the second system. Hence the two systems are not trace equivalent.  
> **username_7**: I would guess that if two transition systems satisfy the same LTL formulas, then they are isomorphic, and thus trace equivalent. Two finite structures satisfy the same set of First-order sentences(i.e., formulas without variables) iff they are isomorphic. By Kamp's theorem (See www.cs.toronto.edu/~libkin/csc2428/Lecture7.ps for a proof), LTL is equivalent to FO-logic, in the sense that for every LTL sentence $\varphi$ there is a FO sentence $\phi$ with the same models and vice versa. Thus if two TS are LTL-equiv, they are FO-equiv and thus isomorphic. But I might be missing someth.  
> **username_7**: Is the author really saying that trace equivalence is strictly finner than LTL equivalence? Corollary 3.18 of the book states: TS is equiv to TS' iff they satisfy the same LT properties, in support of Sylvain's comment. I mean in this case LTL equiv, would also be finer than trace equiv.  
> **username_8**: @Mateus LT = "Linear Time" properties, that is, sets of traces. It shouldn't be confused with LTL properties, which are specified by LTL formulas. Also, you have to be very careful when you throw around "isomorphic". Isomorphic as what? As first order structures? Does that imply that they are trace equivalent?  
> **username_8**: @Dave Ok, after reviewing B&K, they consider both infinite and finite transition systems.  
> **username_9**: @Mateus: Kamp's theorem is for FO with an order relation not FO  over an arbitrary signature. You cannot refer to the edge-relation of the transition system, which is required to specify the structure up to isomorphism.  
> **username_7**: @Vijay, thanks for the explanation. I wasn't sure if there was not a way to express the edge relation of the transition system.  

---

## 2 answers

### Answer by username_8 on 2011-04-10. Score: 9 | Accepted answer

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](https://i.sstatic.net/1bvDJ.png)

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](http://portal.acm.org/citation.cfm?id=1382435.1382735). 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](https://i.sstatic.net/MIzoW.png)

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](https://i.sstatic.net/W7rBc.png)

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.

> **Comments:**
> **username_8**: 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...  
> **username_5**: 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$.  
> **username_8**: @Sylvain you are correct. I tried to simplify, and I ended up breaking it! Let me fix that up.  
> **username_5**: 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}$?  
> **username_9**: The formula $a$ distinguishes between $EVEN$ and $NOTEVEN$.  
> **username_8**: @Vijay No, the issue is distinguishing between $TOTAL$ and $NOTEVEN$. Both $EVEN$ and $NOTEVEN$ satisfy the formula $a$. However, incorporating Sylvain's suggestion did break the argument. I needed the "bad" language to be a singleton. I can fix it with a string that counts (not unlike Antti's anwer below), but I don't have time to change it right this moment. And I'd like to stick in full proofs this time so that I don't have any other stupid mistakes.  
> **username_9**: Ah. I got confused thinking $EVEN$ and $NOTEVEN$ were proposed for equivalence. Does an empty state mean that the state is not labelled $a$? As $NOTEVEN$  has an initial state labelled $\neg a$, it does not satisfy $a$.  
> **username_8**: @Vijay Ahh, you're right. NOTEVEN doesn't satisfy $a$, mea culpa.  
> **username_9**: The problem with my proof suggestion is I didn't work it out! I see the problem with your answer too. I thought while writing that $TOTAL$ should only satisfy 'true'. Should have followed that through.  
> **username_0**: @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.  

---

### Answer by username_10 on 2011-04-08. Score: 3

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.

> **Comments:**
> **username_8**: 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.  
> **username_10**: 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 :)  
> **username_6**: I think this does the trick.  
> **username_8**: I think it works too.  
> **username_8**: 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.  
> **username_10**: I removed references to $\omega$-regularity. They weren't anyway needed. It is known that there is a Buchi automaton for every LTL formula so I think they can be used as a device. And there was no requirement that the transition systems would be finite. Finite transition systems generate trace sets that are as languages regular. I don't know if LTL equivalence = trace equivalence for trace sets generated by finite transition systems. If I would have to guess I would guess yes.  
> **username_8**: I can construct two Buchi automata that are LTL indistinguishable. It's fairly simple: it's basically the trick you use, but the "outside" language is $\omega$-regular and not LTL expressible. But doing it for transition systems seems to be trickier.  
> **username_6**: LTL equivalence = trace equivalence for finite transition systems.  
> **username_10**: Is LTL equivalence = trace equivalence also for finitely branching transition systems? The solution above can be easily implemented as a transition system if one $\aleph_0$ branch is allowed  
> **username_10**: Well ok Mark's answer also involves an $\aleph_0$ branch so I guess it's settled.  

---

