LTS

Stream: CSLib

[Pieter Cuijpers]

I'm going through the LTS file and since there is no dedicated topic for it yet, I thought I create one - instead of making a separate topic for each question that I might encounter. I guess at this stage of development it is good if different questions about the same part of the library are discussed in the same topic, because everything is influencing everything still.

[Pieter Cuijpers]

My first question is about the current definition of LTS.Acyclic.
I had expected to find a defintion that says: an acyclic LTS is an LTS that has no cycles.
Instead, it reads: an acyclic LTS is an LTS that has no infinite multi-step transitions.
Those two definitions are different in an infinite state LTS - in which case I find the first clearer.
What is the reason to choose the second one?

[Fabrizio Montesi]

I was thinking of revising that def, it's weird for me as well. I remember I was basically formalising what's written in the intro to bisim book, I'll have another look at it.