Labelled Transition Systems (LTSs)

Stream: graph theory

[Fabrizio Montesi]

Hi all,
@Rida Hamadani made me aware that the graph angle might be relevant to this discussion: #mathlib4 > Labelled Transition Systems (LTS)

An LTS is essentially a very relaxed labelled digraph (potentially infinitely-many nodes, potentially nondeterministic edge relation, potentially infinitely-many edges between two nodes, etc.), as in:

structure LTS (State : Type u) (Label : Type v) where
  tr : State → Label → State → Prop

I've received quite a few messages (both in the thread and privately), and I'm still uncertain as to whether this should go into mathlib or not. (Potentially with some renamings and added theorems to integrate it with what's already in graph theory or 'Computability'.)

If you're interested in this kind of stuff, please feel free to read the first and last message currently in the thread and pitch in. :)

[Rida Hamadani]

I think this definition should go into the cslib library mentioned in that discussion, but graph theory used to prove things about it should use mathlib's language and PR'd into mathlib

[Fabrizio Montesi]

That for sure. I guess my main question is whether there's interest for a 'labelled digraph' structure or not.

[Fabrizio Montesi]

(digraph with labelled edges)

[Fabrizio Montesi]

(or whether it's already defined somewhere and I'm not seeing it..?)

[Rida Hamadani]

I think there is interest in porting docs#SimpleGraph.Walk.edges onto Digraphs

[Rida Hamadani]

As for labelling the edges of a Digraph instead of a walk, I don't think it deserves a separate structure because it is too simple, unless there is a good reason (ex. using it a lot in some result). Something like this would work:
Fin G.edgeSet.card -> G.edge

[Fabrizio Montesi]

Ah, I see! That might be distinguishing point between mathlib and a cslib. (In CS, it is used really a lot and having the familiar terminology is valuable.)

(I have walk for labelled Digraphs btw, it'd just require some terminology change from LTS to graph theory: https://github.com/fmontesi/mathlib4/blob/fc52687d660778ccd62c42b1f70a412e38918bd7/Mathlib/Computability/LTS/Basic.lean#L72)

[Fabrizio Montesi]

Fin G.edgeSet.card -> G.edge Is G a SimpleGraph here?

[Rida Hamadani]

I mean G to be a Digraph, but I think edgeSet hasn't been ported onto digraphs yet

[Fabrizio Montesi]

Would that allow for self-loops and non-symmetric edges?

[Rida Hamadani]

Yes

[Fabrizio Montesi]

Nice, I'll keep an eye on the development of DiGraph, maybe in the future I'll be able to use it a bit more for our purposes. :)