In: J. Esparza, C. Lakos (Eds.): Lecture Notes in Computer Science, Vol. 2360: 23rd International Conference on Applications and Theory of Petri Nets, Adelaide, Australia, June 24-30, 2002, pages 1-374pp. Springer Verlag, June 2002.
Abstract: The algorithm of Gallager, Humblet, and Spira computes the minimum spanning tree of a weighted graph in a distributed fashion. Though based on a simple mathematical idea, this algorithm is hard to understand because of the complex communication between the distributed agents.
There are several attempts to prove the correctness of this algorithm but most of the proofs are either incomplete or extremely long and technical and, therefore, difficult to comprehend.
This paper reports on a new model and a new correctness proof for the algorithm. Model and proof are given in a sequence of 12 property preserving refinement steps, starting with a simple non-distributed algorithm. All algorithms are modelled by Algebraic Petri nets. We justify 8 of the refinement steps using well-known refinement methods for distributed algorithms. The other four steps can not be justified using traditional refinement methods. Their correctness is proved by using the new concept of transition refinement which we introduced before.