Distributed Computation of a Spanning Tree Without 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 the sum.





is decreasing for >.







Correctness
  1. All edges incident to an i-labelled vertex have labels lower or equal than i.
  2. All vertices labelled n are connected by edges labelled n.
  3. The subgraph induced by the i-labelled edges has no cycle (i>0).
  4. If G' is an irreducible graph obtained from G, then all vertices are labelled n.


Description

Proof

Snapshots