0

I am following Katoen's YouTube course 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 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?

Louie_the_unsolver
  • 19
  • 3

1 Answers1

2

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

Shaull
  • 5,571
  • 1
  • 22
  • 32
  • 1
    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 Apr 20 '21 at 09:24
  • 1
    @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 Apr 20 '21 at 09:29