Distributed Computation of a Spanning Tree With Local Detection of Termination, Each Process is Identified by a Unique Name
Proof:
TerminationThis system is noetherian because executing a rewriting step implies that
is decreasing for >2.
Correctness
- The labels of the edges incident to an (X,i)-labelled vertex are less or equal than i.
- There exists at most one vertex labelled (A,i), i>0.
- There is exactly one vertex with the label (A,n).
- A (F,i)-labelled vertex has only (X,i)-labelled vertex as neighbours.
- All the (X,n)-labelled vertices are connected by n-labelled edges.
- The (A,n)- and (A',n)-labelled vertices are connected by n-labelled edges.
- The subgraph of G(V,E) induced by the i-labelled edges has no cycle.
- Let G' be an irreducible graph obtained from G, exactly one vertex has (A,n) as label and all the others are labelled (F,n).