Sequential Computation of a Spanning Tree, Each Process is Identified by a Unique Name
Proof:
TerminationThis system is noetherian because executing a rewriting step implies that
is decreasing for >3.
Correctness
- The labels of the edges incident to an (X,i)-labelled vertex are less or equal than i.
- There exists at most one vertex labelled (A,i), for a fixed i>0.
- There exists at least one vertex with the label (X,j) neighbour of a (N,i)-labelled vertex with j>i.
- A (F,i)-labelled vertex has no (X,j)-labelled vertex as a neighbour, where j != i.
- All the (X,n)-labelled vertices are connected by n-labelled edges.
- The subgraph of G(V,E) induced by the i-labelled edges has no cycle (i>0).
- 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.
- 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).