Paper
Gossiping and the Characterization by T-Graphs and M-Graphs
29 pages · 7 marked passages · pdflatex · download PDF · lax-630294
-
The Gossiping Problem
Let be a multigraph. A labeling assigns a natural number to every edge. A strict temporal path from to is a path from to in whose edge labels strictly increase in traversal order; the path of length zero is allowed. The labeled graph is temporally connected if, for every ordered pair of vertices , there is a strict temporal path from to . The instance of Gossiping is a yes-instance if some labeling makes temporally connected.
Interpreting each edge as a call between its endpoints and each label as the time of the call, a labeling is an ordering of the calls, and it is temporally connected exactly when every participant learns every secret.
1 import Mathlib.Combinatorics.Graph.Basic 2 import Mathlib.Order.Fin.Basic 3 import Mathlib.Order.Monotone.Basic 4 … module docstring, 30 lines 35 36 namespace Lax630294.Gossiping 37 38 open Graph 39 40 variable {α β : Type*} 41 42 /-- A strict temporal path from `u` to `v` with respect to the labeling `ℓ`: a path 43 of some length `k` whose edge labels strictly increase along the path. -/ 44 def HasTemporalPath (G : Graph α β) (ℓ : β → ℕ) (u v : α) : Prop := 45 ∃ (k : ℕ) (x : Fin (k + 1) → α) (e : Fin k → β), 46 x 0 = u ∧ x (Fin.last k) = v ∧ Function.Injective x ∧ 47 (∀ i : Fin k, G.IsLink (e i) (x i.castSucc) (x i.succ)) ∧ 48 StrictMono (fun i => ℓ (e i)) 49 50 /-- The labeling `ℓ` makes `G` temporally connected: every vertex reaches every 51 vertex by a strict temporal path. -/ 52 def IsTemporallyConnected (G : Graph α β) (ℓ : β → ℕ) : Prop := 53 ∀ u ∈ V(G), ∀ v ∈ V(G), HasTemporalPath G ℓ u v 54 55 /-- `G` is label-connected, i.e. a yes-instance of Gossiping: some labeling makes it temporally connected. -/ 56 def IsLabelConnected (G : Graph α β) : Prop := 57 ∃ ℓ : β → ℕ, IsTemporallyConnected G ℓ 58 59 end Lax630294.Gossiping 60 -
Cycles, Spanning Trees and Spanning Forests of a Multigraph
Let be a multigraph and let be a set of edges of ; we identify with the spanning subgraph of that keeps all vertices of and only the edges in . The components of are the connected components of this subgraph; every vertex of lies in a component, even if it is incident to no edge of .
A set of edges is simple if it contains no loop and no two parallel edges. A simple set is acyclic if the subgraph it forms has no cycle, and it is a tree if it is acyclic and connected. A spanning tree of is a simple set of edges of forming a tree on all vertices of . A spanning forest with components of is a simple acyclic set of edges of with exactly components.
A cycle of length consists of pairwise distinct vertices and pairwise distinct edges such that joins and , with indices taken modulo . Its edge set is .
1 import Mathlib.Combinatorics.Graph.Delete 2 import Mathlib.Combinatorics.Graph.Simple 3 import Mathlib.Combinatorics.SimpleGraph.Acyclic 4 import Mathlib.Data.Set.Card 5 import Mathlib.Data.ENat.Basic 6 … module docstring, 35 lines 42 43 namespace Lax630294.SpanningStructures 44 45 open Graph 46 47 variable {α β : Type*} 48 49 /-- The simple graph underlying the spanning subgraph of `G` with edge set `F`. -/ 50 abbrev underlying (G : Graph α β) (F : Set β) : SimpleGraph V(G) := 51 (G.restrict F).toSimpleGraph 52 53 /-- The vertices of `G` incident to an edge of `F`. -/ 54 def incidentVertices (G : Graph α β) (F : Set β) : Set α := 55 {x | ∃ e ∈ F, G.Inc e x} 56 57 /-- `C` is the edge set of a cycle of `G` of some length `n ≥ 1`: there are 58 pairwise distinct vertices `v 0, …, v (n - 1)` and pairwise distinct edges 59 `e 0, …, e (n - 1)` such that `e i` links `v i` and `v (i + 1)`, with indices 60 taken modulo `n`, and `C` consists of these edges. Its length is `C.encard`. -/ 61 def IsCycle (G : Graph α β) (C : Set β) : Prop := 62 ∃ n : ℕ, 0 < n ∧ ∃ (v : ZMod n → α) (e : ZMod n → β), 63 Function.Injective v ∧ Function.Injective e ∧ 64 (∀ i, G.IsLink (e i) (v i) (v (i + 1))) ∧ Set.range e = C 65 66 /-- `T` is a spanning tree of `G`. -/ 67 def IsSpanningTree (G : Graph α β) (T : Set β) : Prop := 68 T ⊆ E(G) ∧ (G.restrict T).Simple ∧ (underlying G T).IsTree 69 70 /-- `F` is a spanning forest of `G` with exactly `k` components. -/ 71 def IsSpanningForest (G : Graph α β) (F : Set β) (k : ℕ) : Prop := 72 F ⊆ E(G) ∧ (G.restrict F).Simple ∧ (underlying G F).IsAcyclic ∧ 73 ENat.card (underlying G F).ConnectedComponent = k 74 75 end Lax630294.SpanningStructures 76 -
The Gossiping Problem
Let be a multigraph. A labeling assigns a natural number to every edge. A strict temporal path from to is a path from to in whose edge labels strictly increase in traversal order; the path of length zero is allowed. The labeled graph is temporally connected if, for every ordered pair of vertices , there is a strict temporal path from to . The instance of Gossiping is a yes-instance if some labeling makes temporally connected.
Interpreting each edge as a call between its endpoints and each label as the time of the call, a labeling is an ordering of the calls, and it is temporally connected exactly when every participant learns every secret.
1 import Mathlib.Combinatorics.Graph.Basic 2 import Mathlib.Order.Fin.Basic 3 import Mathlib.Order.Monotone.Basic 4 … module docstring, 30 lines 35 36 namespace Lax630294.Gossiping 37 38 open Graph 39 40 variable {α β : Type*} 41 42 /-- A strict temporal path from `u` to `v` with respect to the labeling `ℓ`: a path 43 of some length `k` whose edge labels strictly increase along the path. -/ 44 def HasTemporalPath (G : Graph α β) (ℓ : β → ℕ) (u v : α) : Prop := 45 ∃ (k : ℕ) (x : Fin (k + 1) → α) (e : Fin k → β), 46 x 0 = u ∧ x (Fin.last k) = v ∧ Function.Injective x ∧ 47 (∀ i : Fin k, G.IsLink (e i) (x i.castSucc) (x i.succ)) ∧ 48 StrictMono (fun i => ℓ (e i)) 49 50 /-- The labeling `ℓ` makes `G` temporally connected: every vertex reaches every 51 vertex by a strict temporal path. -/ 52 def IsTemporallyConnected (G : Graph α β) (ℓ : β → ℕ) : Prop := 53 ∀ u ∈ V(G), ∀ v ∈ V(G), HasTemporalPath G ℓ u v 54 55 /-- `G` is label-connected, i.e. a yes-instance of Gossiping: some labeling makes it temporally connected. -/ 56 def IsLabelConnected (G : Graph α β) : Prop := 57 ∃ ℓ : β → ℕ, IsTemporallyConnected G ℓ 58 59 end Lax630294.Gossiping 60 -
T-Graph
A -witness of a multigraph is a pair of spanning trees of that share at most one edge. A multigraph is a -graph if it has a -witness.
1 import Lax630294.SpanningStructures 2 … module docstring, 15 lines 18 19 namespace Lax630294.TGraph 20 21 open Graph Lax630294.SpanningStructures 22 23 variable {α β : Type*} 24 25 /-- `T₁, T₂` are spanning trees of `G` sharing at most one edge. -/ 26 def IsTWitness (G : Graph α β) (T₁ T₂ : Set β) : Prop := 27 IsSpanningTree G T₁ ∧ IsSpanningTree G T₂ ∧ (T₁ ∩ T₂).encard ≤ 1 28 29 /-- `G` is a `T`-graph: it has a `T`-witness. -/ 30 def IsTGraph (G : Graph α β) : Prop := 31 ∃ T₁ T₂ : Set β, IsTWitness G T₁ T₂ 32 33 end Lax630294.TGraph 34 -
M-Witness and M-Graph
An -witness of a multigraph consists of pairwise edge-disjoint subgraphs , , of , where is a cycle of length at least four and each is a spanning forest of with exactly four components, each of which contains a vertex of . A multigraph admits an -witness if it has one, and it is an -graph if it admits an -witness and is not a -graph.
1 import Lax630294.TGraph 2 … module docstring, 18 lines 21 22 namespace Lax630294.MGraph 23 24 open Graph Lax630294.SpanningStructures Lax630294.TGraph 25 26 variable {α β : Type*} 27 28 /-- `F` is a spanning forest of `G` with four components, each containing a vertex 29 of the cycle `C`. -/ 30 def IsFourComponentForestMeeting (G : Graph α β) (C F : Set β) : Prop := 31 IsSpanningForest G F 4 ∧ 32 ∀ x : V(G), ∃ c : V(G), (c : α) ∈ incidentVertices G C ∧ (underlying G F).Reachable x c 33 34 /-- `C, F₁, F₂` is an `M`-witness of `G`. -/ 35 def IsMWitness (G : Graph α β) (C F₁ F₂ : Set β) : Prop := 36 IsCycle G C ∧ 4 ≤ C.encard ∧ 37 IsFourComponentForestMeeting G C F₁ ∧ IsFourComponentForestMeeting G C F₂ ∧ 38 Disjoint C F₁ ∧ Disjoint C F₂ ∧ Disjoint F₁ F₂ 39 40 /-- `G` admits an `M`-witness. -/ 41 def AdmitsMWitness (G : Graph α β) : Prop := 42 ∃ C F₁ F₂ : Set β, IsMWitness G C F₁ F₂ 43 44 /-- `G` is an `M`-graph: it admits an `M`-witness and is not a `T`-graph. -/ 45 def IsMGraph (G : Graph α β) : Prop := 46 AdmitsMWitness G ∧ ¬ IsTGraph G 47 48 end Lax630294.MGraph 49 -
Characterization of Label-Connected Multigraphs
Let be a finite multigraph. Then is a yes-instance of Gossiping (label-connected) if and only if at least one of the following holds:
- has at most one vertex;
- is a -graph;
- is an -graph.
1 import Lax630294.Gossiping 2 import Lax630294.TGraph 3 import Lax630294.MGraph 4 … module docstring, 20 lines 25 26 namespace Lax630294.Characterization 27 28 open Graph Lax630294.Gossiping Lax630294.TGraph Lax630294.MGraph 29 30 universe u v 31 32 /-- A finite multigraph is label-connected if and only if it has at most one vertex, 33 is a `T`-graph, or is an `M`-graph. -/ 34 axiom isLabelConnected_iff {α : Type u} {β : Type v} (G : Graph α β) 35 (hV : V(G).Finite) (hE : E(G).Finite) : 36 IsLabelConnected G ↔ V(G).Subsingleton ∨ IsTGraph G ∨ IsMGraph G 37 38 end Lax630294.Characterization 39 -
no assumptions