Distributed Computation of a Spanning Tree Without Local Detection of the Global Termination



Proof:

Termination



This system is noetherian because executing a rewriting step implies that |G|N is decreasing for >.





Correctness
  1. Every edge incident with N-labelled vertex is labelled 0,
  2. a A-labelled vertex has a 1-labelled incident edge,
  3. The subgraph induced by the 1-labelled edges is a tree,


Description

Proof

Snapshots


An animated example