Time varying networks (Temporal Network/graph)

Stream: graph theory

[Ethan Arm]

Hi, I'm trying to implement Temporal graphs and I wanted some help on:

1. Is there already a project on the subject? I searched a bit but didn't found anything
2. I'm a new to Lean, and I'm not sure what is the best representation for it. I tried to mimick the implementation of Mathlib SimpleGraph to have a maximum of unified APi. Here is what I have for now ( it's a wip and a bit toyish):

universe u

structure TemporalGraph (V: Type u) where
  Adj : V → V → Nat

(3. Unshure where to ask this but shouldn't it be possible to use type classes to transfert most of the already define theorems to this new structure)

Thanks for any remarks :slight_smile:

[Shreyas Srinivas]

What is a temporal graph?

[Ethan Arm]

Sorry english is not my primary language and it seems that is called time varying networks in english, might be why i didn't find anything, I'm editing title in consequence

[(deleted)]

I just searched and a time varying network is a network whose links are only active at certain points in time. I think the best way to implement it is to have a list of times when a link is active, and then from the list we can have a function that takes a timestamp and returns the SimpleGraph at that point in time

[(deleted)]

Ultimately it is software engineering

[Mauricio Collares]

Arm Ethan said:

Sorry english is not my primary language and it seems that is called time varying networks in english, might be why i didn't find anything, I'm editing title in consequence

Don't worry, "temporal graph" is correct as well. At least I've heard multiple people in my department talk about them before.

[Shreyas Srinivas]

Arm Ethan said:

Sorry english is not my primary language and it seems that is called time varying networks in english, might be why i didn't find anything, I'm editing title in consequence

Oh that’s not what i mean. I am genuinely curious what a temporal graph is and what the output of Adj means

[Mauricio Collares]

I think one of the earliest papers in the area is https://dl.acm.org/doi/10.1145/335305.335364. Basically each edge is labeled with a natural number, corresponding to the time where it is "open"/"available" (some sources allow a set of natural numbers). Then you want to study structures which respect these times, e.g. the labels in a temporal path must be non-decreasing, which would correspond to waiting at a vertex until the next edge is available.

[Ethan Arm]

Shreyas Srinivas said:

Arm Ethan said:

Sorry english is not my primary language and it seems that is called time varying networks in english, might be why i didn't find anything, I'm editing title in consequence

Oh that’s not what i mean. I am genuinely curious what a temporal graph is and what the output of Adj means

My intuition was to define a relation as the same as SimpleGraph and label it with a natural number corresponding to wich time it exists. But after reflecting a bit my primary objective is to define time connectivity and for that I wanted to define a walk on it but I'm not sure if this definition is the most efficient.

Moreover I'm, for now, using the assumption that an edge exists only at one given time wich is a bit reductive but simpler for a start. At long term I was thinking of returning a list of natural corresponding to several times of existance.