Why does LTL equivalence (with next oeprator) implie trace equivalence in finite transition machines?
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 &quot;lasso&quot; 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 &quot;infinitely many prefixes&quot; problem.
Now, we can define an LTL formula, using &quot;next&quot; operators, that states &quot;$uv^m$ is not a prefix of the trace&quot;. This formula holds in $K_2$, but not in $K_1$.