Sequential Computation of a Spanning Tree, Each Process is Identified by a Unique Name



Proof:

Termination



This system is noetherian because executing a rewriting step implies that





is decreasing for >3.







Correctness
  1. The labels of the edges incident to an (X,i)-labelled vertex are less or equal than i.
  2. There exists at most one vertex labelled (A,i), for a fixed i>0.
  3. There exists at least one vertex with the label (X,j) neighbour of a (N,i)-labelled vertex with j>i.
  4. A (F,i)-labelled vertex has no (X,j)-labelled vertex as a neighbour, where j != i.
  5. All the (X,n)-labelled vertices are connected by n-labelled edges.
  6. The subgraph of G(V,E) induced by the i-labelled edges has no cycle (i>0).
  7. The (M,n)-labelled vertices form a simple path which edges are labelled n. Moreover, one of the endvertices of this path is connected to a vertex labelled (A,n) by an edge labelled n.
  8. Let G' be an irreducible graph obtained from G, only one vertex has (A,n) as label and all the others are labelled (F,n).


Description

Proof

Snapshots