<p>The important thing to notice is that in finite transition systems, two systems <span class="math-container">$K_1,K_2$</span> over an alphabet <span class="math-container">$\Sigma$</span> are not trace equivalent (for infinite traces) if and only if there exists a finite trace <span class="math-container">$w\in \Sigma^*$</span> that is in one of them, but not the other.</p>
<p>Indeed, if <span class="math-container">$K_1$</span> and <span class="math-container">$K_2$</span> are not trace equivalent, denoted <span class="math-container">$L(K_1)\neq L(K_2)$</span>, then w.l.o.g. there exists an infinite trace <span class="math-container">$x\in L(K_1)\setminus L(K_2)$</span>, but we can say something stronger: since the transition systems are finite, we can actually assume <span class="math-container">$x$</span> is of the form <span class="math-container">$x=uv^\omega$</span> for finite words <span class="math-container">$u,v\in \Sigma^*$</span>.
This &quot;lasso&quot; structure of <span class="math-container">$x$</span> tells us that there is a finite trace <span class="math-container">$uv^m\in L(K_1)\setminus L(K_2)$</span>, for some <span class="math-container">$m\in \mathbb{N}$</span>, thus getting rid of the &quot;infinitely many prefixes&quot; problem.</p>
<p>Now, we can define an LTL formula, using &quot;next&quot; operators, that states &quot;<span class="math-container">$uv^m$</span> is not a prefix of the trace&quot;. This formula holds in <span class="math-container">$K_2$</span>, but not in <span class="math-container">$K_1$</span>.</p>

CC BY-SA 4.0
2021-04-20T09:24:16.600Z
Why do you need to consider lassos ? Isn't it enough to say that a finite transition system contains a trace iff it contains all its prefixes ?
Denis
CC BY-SA 4.0
2021-04-20T09:29:21.770Z
@Denis I could, but then I would need Kőnig's Lemma, and for that I need to google Konig, and copy-paste the ő, and I was trying to avoid doing that (also, obviously I didn't think of that, and went directly to lassos) :)
Shaull
CC BY-SA 4.0
2021-04-20T06:05:47.497Z
2021-04-20T06:05:47.497Z
Shaull
<p>I am following Katoen's <a href="https://www.youtube.com/playlist?list=PLnbFC0ntxiqdpoWwMKCVh6BRwBePHaqQx" rel="nofollow noreferrer">YouTube course</a> about Model Checking.</p>
<p>I am trying to understand how finite transition machines are different from infinite transition machines in terms of equivalences. That lead me to the following <a href="https://cstheory.stackexchange.com/questions/5841/trace-equivalence-vs-ltl-equivalence">question</a> regarding equivalences, but the focus there was on infinite transition machines. Comments in the thread claimed that LTL equivalence = trace equivalence in finite transition machines, when LTL includes the next operator but I do not see how.</p>
<p>The direction from trace equivalence to LTL equivalence is immediate, due to the fact that only traces satisfy LTL formulas.</p>
<p>The other direction is problematic for me:
If we have two transition machines that are LTL equivalent, I understand that they are equivalent with respect to finite traces, because I can use the next operator, but what happens with infinite traces?</p>
<p>If I try and assume the claim is false in hopes of reaching a contradiction, I get that an infinite number of prefixes from each infinite trace from either transition system would have to be in both trace sets, but where's the problem? Can't I express infinitely many different prefixes using a finite transition machine?</p>

<linear-temporal-logic>
Why does LTL equivalence (with next oeprator) implie trace equivalence in finite transition machines?
Louie_the_unsolver
# Why does LTL equivalence (with next oeprator) implie trace equivalence in finite transition machines?

(Asked by: username_0 on 2021-04-20)

I am following Katoen's [YouTube course](https://www.youtube.com/playlist?list=PLnbFC0ntxiqdpoWwMKCVh6BRwBePHaqQx) about Model Checking.

I am trying to understand how finite transition machines are different from infinite transition machines in terms of equivalences. That lead me to the following [question](https://cstheory.stackexchange.com/questions/5841/trace-equivalence-vs-ltl-equivalence) regarding equivalences, but the focus there was on infinite transition machines. Comments in the thread claimed that LTL equivalence = trace equivalence in finite transition machines, when LTL includes the next operator but I do not see how.

The direction from trace equivalence to LTL equivalence is immediate, due to the fact that only traces satisfy LTL formulas.

The other direction is problematic for me:
If we have two transition machines that are LTL equivalent, I understand that they are equivalent with respect to finite traces, because I can use the next operator, but what happens with infinite traces?

If I try and assume the claim is false in hopes of reaching a contradiction, I get that an infinite number of prefixes from each infinite trace from either transition system would have to be in both trace sets, but where's the problem? Can't I express infinitely many different prefixes using a finite transition machine?

**Tags:** linear-temporal-logic


---

## 1 answers

### Answer by username_1 on 2021-04-20. Score: 2 | Accepted answer

The important thing to notice is that in finite transition systems, two systems $K\_1,K\_2$ over an alphabet $\Sigma$ are not trace equivalent (for infinite traces) if and only if there exists a finite trace $w\in \Sigma^\*$ that is in one of them, but not the other.

Indeed, if $K\_1$ and $K\_2$ are not trace equivalent, denoted $L(K\_1)\neq L(K\_2)$, then w.l.o.g. there exists an infinite trace $x\in L(K\_1)\setminus L(K\_2)$, but we can say something stronger: since the transition systems are finite, we can actually assume $x$ is of the form $x=uv^\omega$ for finite words $u,v\in \Sigma^\*$.
This "lasso" structure of $x$ tells us that there is a finite trace $uv^m\in L(K\_1)\setminus L(K\_2)$, for some $m\in \mathbb{N}$, thus getting rid of the "infinitely many prefixes" problem.

Now, we can define an LTL formula, using "next" operators, that states "$uv^m$ is not a prefix of the trace". This formula holds in $K\_2$, but not in $K\_1$.

> **Comments:**
> **username_2**: Why do you need to consider lassos ? Isn't it enough to say that a finite transition system contains a trace iff it contains all its prefixes ?  
> **username_1**: @username_2 I could, but then I would need Kőnig's Lemma, and for that I need to google Konig, and copy-paste the ő, and I was trying to avoid doing that (also, obviously I didn't think of that, and went directly to lassos) :)  

---

