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



Proof:

Termination



This system is noetherian because executing a rewriting step implies that (|G|N,|G|M) is decreasing for >2 .





Correctness
  1. If an edge is incident with N-labelled vertex then it is labelled with 0,
  2. The set of vertices not labelld with N is connected by 1-edges,
  3. The graph defined by the set of 1-labelled edges and incident vertices is without cycles,
  4. There is exactly one A-labelled vertex,
  5. The set of M-labelled vertices is a simple path from the Root to the A-labelled vertex and every edge of this path is labelled with 1,
  6. A F-labelled vertex has no neighbours labelled with N.


Description

Proof

Snapshots