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?