M.Sc Student | Shimony Benny |
---|---|

Subject | A New Correctness Proof of Gallager, Humblet and Spira's Minimum Spanning Tree Protocol |

Department | Department of Electrical and Computers Engineering |

Supervisor | PROF. Yoram Moses |

A new correctness proof
of the celebrated distributed Minimum Spanning Tree protocol of Gallager,
Humblet and Spira (GHS) is presented. The protocol is fundamental and is
considered by many to have opened a new era in the theory of network
algorithms. While the protocol itself is very elegant and the arguments for why
the protocol should be correct are fairly convincing, a rigorous correctness
proof of the GHS protocol turns out to be a considerable challenge. The proof
presented in this thesis uses an
invariant assertion approach, supported by a new decomposition of the algorithm
into abstraction levels. In particular, the new intermediate-level abstraction,
we call by as the ** rainbow-construction**, refines an abstraction,
typically used to describe GHS, by the assignment of colors to nodes. The
construction mimics essential aspects of the search process in the GHS
algorithm, while completely abstracting details of communication and local
variables of processes. Thus, in the protocol level analysis, rather than using
a full refinement proof, an augmented
version of the GHS algorithm is defined, in which auxiliary