Abstract
This paper provides a proof of correctness for the celebrated Minimum Spanning Tree protocol of Gallager, Humblet and Spira [GHS83]. Both the protocol and the quest for a natural correctness proof have had considerable impact on the literature concerning network protocols and verification. We present an invariance proof that is based on a new intermediate-level abstraction of the protocol. A central role of the intermediate-level configurations in the proof is to facilitate the statement of invariants and other properties of the executions of GHS at the low level. This provides a powerful tool for both the statement and the proof of properties of the algorithm. The result is the first proof that follows the spirit of the informal arguments made in the original paper.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Bollobás, B.: Graph theory, An introductory course. Graduate Texts in Mathematics 63, 1–180 (1979)
Borūvka, O.: O jistém problému minimálním. Práce Mor. Prírodoved Spol. v Brne (Acta Societ. Scient. Natur. Moravicae) 3, 37–58 (1926) (Czech language)
Chou, C.-T.: A Bug in the Distributed Minimum Spanning Tree Algorithms of Gallager, Humblet, and Spira (unpublished manuscript, 1988)
Chou, C.-T., Gafni, E.: Understanding and Verifying Distributed Algorithms Using Stratified Decomposition. In: PODC 1988, pp. 44–65 (1988)
Gallager, R.G., Humblet, P.A., Spira, P.M.: A Distributed Algorithm for Minimum-Weight Spanning Trees. TOPLAS 5(1), 66–77 (1983)
Harary, F.: Graph Theory. Addison-Wesley, Reading (1969)
Hesselink, W.H.: The Verified Incremental Design of a Distributed Spanning Tree Algorithm: Extended Abstract. Formal Aspects of Computing 11(1), 45–55 (1999)
Janssen, W., Zwiers, J.: From Sequential Layers to Distributed Processes: Deriving a Distributed Minimum Weight Spanning Tree Algorithm (Extended Abstract). In: PODC 1992, pp. 215–227 (1992)
Prim, R.C.: On the shortest subtree of a graph and the traveling salesman problem. Proc. Am. Math. Soc. 7, 48–50 (1956)
Lynch, N.A.: Distributed Algorithms. Morgan Kaufmann, San Francisco (1996)
Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems ⊙ Safety ⊙. Springer, Heidelberg (1995)
Prim, R.C.: Shortest connection networks and some generalizations. Bell System Technical Journal 36, 1389–1401 (1957)
Stomp, F.A., de Roever, W.P.: A Correctness Proof of a Distributed Minimum-Weight Spanning Tree Algorithm (extended abstract). In: ICDCS 1987, pp. 440–447 (1987)
Peuker, S.: Halbordnungsbasierte Verfeinerung zur Verifikation verteilter Algorithmen. Ph.D. thesis, Humboldt University of Berlin (April 2001)
Peuker, S.: Transition Refinement for Deriving a Distributed Minimum Weight Spanning Tree Algorithm. In: Esparza, J., Lakos, C.A. (eds.) ICATPN 2002. LNCS, vol. 2360, pp. 374–393. Springer, Heidelberg (2002)
Welch, J.L.: Topics in Distributed Computing: The Impact of Partial Synchrony, and Modular Decomposition of Algorithms. Ph.D. thesis. MIT (June 1988)
Welch, J.L., Lamport, L., Lynch, N.A.: A Lattice-Structured Proof Technique Applied to a Minimum Spanning Tree Algorithm (Extended Abstract). In: PODC 1988, pp. 28–43 (1988)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Moses, Y., Shimony, B. (2006). A New Proof of the GHS Minimum Spanning Tree Algorithm. In: Dolev, S. (eds) Distributed Computing. DISC 2006. Lecture Notes in Computer Science, vol 4167. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11864219_9
Download citation
DOI: https://doi.org/10.1007/11864219_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-44624-8
Online ISBN: 978-3-540-44627-9
eBook Packages: Computer ScienceComputer Science (R0)Springer Nature Proceedings Computer Science
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
