Distributed Computation of a Spanning Tree Without Local Detection of Termination, Each Process is Identified by a Unique Name
Proof:
TerminationThis system is noetherian because executing a rewriting step implies that the sum.
is decreasing for >.
Correctness
- All edges incident to an i-labelled vertex have labels lower or equal than i.
- All vertices labelled n are connected by edges labelled n.
- The subgraph induced by the i-labelled edges has no cycle (i>0).
- If G' is an irreducible graph obtained from G, then all vertices are labelled n.