Distributed Computation of a Spanning Tree With Local Detection of Termination, Each Process is Identified by a Unique Name



Proof:

Termination



This system is noetherian because executing a rewriting step implies that





is decreasing for >2.







Correctness
  1. The labels of the edges incident to an (X,i)-labelled vertex are less or equal than i.
  2. There exists at most one vertex labelled (A,i), i>0.
  3. There is exactly one vertex with the label (A,n).
  4. A (F,i)-labelled vertex has only (X,i)-labelled vertex as neighbours.
  5. All the (X,n)-labelled vertices are connected by n-labelled edges.
  6. The (A,n)- and (A',n)-labelled vertices are connected by n-labelled edges.
  7. The subgraph of G(V,E) induced by the i-labelled edges has no cycle.
  8. 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).


Description

Proof

Snapshots