Distributed Computation of a Spanning Tree Without Local Detection of the Global Termination
Proof:
TerminationThis system is noetherian because executing a rewriting step implies that |G|N is decreasing for >.
Correctness
- Every edge incident with N-labelled vertex is labelled 0,
- a A-labelled vertex has a 1-labelled incident edge,
- The subgraph induced by the 1-labelled edges is a tree,