Relation-algebraic verification of Borůvka’s minimum spanning tree algorithm. (English) Zbl 07670521
Fahrenberg, Uli (ed.) et al., Relational and algebraic methods in computer science. 19th international conference, RAMiCS 2021, Marseille, France, November 2–5, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13027, 225-240 (2021).
Summary: Previous work introduced a relation-algebraic framework for reasoning about weighted-graph algorithms. We use this framework to prove partial correctness of a sequential version of Borůvka’s minimum spanning tree algorithm. This is the first formal proof of correctness for this algorithm. We also discuss new abstractions that make it easier to reason about weighted graphs.
For the entire collection see [Zbl 1507.68032].
For the entire collection see [Zbl 1507.68032].
MSC:
| 68Qxx | Theory of computing |
Keywords:
algorithm verification; formal methods; Kleene algebras; relation algebras; stone algebras; weighted graphsReferences:
| [1] | Balbes, R., Dwinger, P.: Distributive Lattices. University of Missouri Press (1974) · Zbl 0321.06012 |
| [2] | Berge, C., Ghouila-Houri, A.: Programming, Games and Transportation Networks. Wiley, Methuen (1965) |
| [3] | Berghammer, R.; von Karger, B.; Wolf, A.; Jeuring, J., Relation-algebraic derivation of spanning tree algorithms, Mathematics of Program Construction, 23-43 (1998), Heidelberg: Springer, Heidelberg · Zbl 0905.68020 · doi:10.1007/BFb0054283 |
| [4] | Berghammer, R.; Rusinowska, A.; de Swart, H., Computing tournament solutions using relation algebra and RelView, Eur. J. Oper. Res., 226, 3, 636-645 (2013) · Zbl 1292.91060 · doi:10.1016/j.ejor.2012.11.025 |
| [5] | Birkhoff, G.: Lattice Theory, Colloquium Publications, vol. XXV, 3rd edn., American Mathematical Society (1967) · Zbl 0153.02501 |
| [6] | Borůvka, O., O jistém problému minimálním, Práce moravské přírodovědecké společnosti, 3, 3, 37-58 (1926) · JFM 57.1343.06 |
| [7] | Chazelle, B., A minimum spanning tree algorithm with inverse-Ackermann type complexity, J. ACM, 47, 6, 1028-1047 (2000) · Zbl 1094.68606 · doi:10.1145/355541.355562 |
| [8] | Choquet, G., Étude de certains réseaux de routes, C. R. Hebd. Seances Acad. Sci., 206, 310-313 (1938) · JFM 64.0707.02 |
| [9] | Conway, J.H.: Regular Algebra and Finite Machines. Chapman and Hall (1971) · Zbl 0231.94041 |
| [10] | Florek, K.; Łukaszewicz, J.; Perkal, J.; Steinhaus, H.; Zubrzycki, S., Sur la liaison et la division des points d’un ensemble fini, Colloq. Math., 2, 3-4, 282-285 (1951) · Zbl 0045.26103 · doi:10.4064/cm-2-3-4-282-285 |
| [11] | Frias, M.F., Aguayo, N., Novak, B.: Development of graph algorithms with fork algebras. In: XIX Conferencia Latinoamericana de Informática, pp. 529-554 (1993) |
| [12] | Graham, RL; Hell, P., On the history of the minimum spanning tree problem, Ann. Hist. Comput., 7, 1, 43-57 (1985) · Zbl 0998.68003 · doi:10.1109/MAHC.1985.10011 |
| [13] | Guttmann, W.; Sampaio, A.; Wang, F., Relation-algebraic verification of Prim’s minimum spanning tree algorithm, Theoretical Aspects of Computing - ICTAC 2016, 51-68 (2016), Cham: Springer, Cham · Zbl 1400.68155 · doi:10.1007/978-3-319-46750-4_4 |
| [14] | Guttmann, W., An algebraic framework for minimum spanning tree problems, Theoret. Comput. Sci., 744, 37-55 (2018) · Zbl 1401.68246 · doi:10.1016/j.tcs.2018.04.012 |
| [15] | Guttmann, W., Verifying minimum spanning tree algorithms with Stone relation algebras, J. Log. Algebraic Methods Program., 101, 132-150 (2018) · Zbl 1401.68247 · doi:10.1016/j.jlamp.2018.09.005 |
| [16] | Guttmann, W., Robinson-O’Brien, N.: Relational minimum spanning tree algorithms. Archive of Formal Proofs (2020). Formal proof development. https://isa-afp.org/entries/Relational_Minimum_Spanning_Trees.html |
| [17] | Haslbeck, M.P.L., Lammich, P., Biendarra, J.: Kruskal’s algorithm for minimum spanning forest. Archive of Formal Proofs (2019). Formal proof development. https://isa-afp.org/entries/Kruskal.html |
| [18] | Karger, DR; Klein, PN; Tarjan, RE, A randomized linear-time algorithm to find minimum spanning trees, J. ACM, 42, 2, 321-328 (1995) · Zbl 0886.68079 · doi:10.1145/201019.201022 |
| [19] | Kehden, B.; Neumann, F.; Gottlieb, J.; Raidl, GR, A relation-algebraic view on evolutionary algorithms for some graph problems, Evolutionary Computation in Combinatorial Optimization, 147-158 (2006), Heidelberg: Springer, Heidelberg · Zbl 1401.68291 · doi:10.1007/11730095_13 |
| [20] | Kozen, D., A completeness theorem for Kleene algebras and the algebra of regular events, Inf. Comput., 110, 2, 366-390 (1994) · Zbl 0806.68082 · doi:10.1006/inco.1994.1037 |
| [21] | Kruskal, JB Jr, On the shortest spanning subtree of a graph and the traveling salesman problem, Proc. Am. Math. Soc., 7, 1, 48-50 (1956) · Zbl 0070.18404 · doi:10.1090/S0002-9939-1956-0078686-7 |
| [22] | Lammich, P., Nipkow, T.: Proof pearl: purely functional, simple and efficient priority search trees and applications to Prim and Dijkstra. In: Harrison, J., O’Leary, J., Tolmach, A. (eds.) 10th International Conference on Interactive Theorem Proving (ITP 2019). LIPIcs: Leibniz International Proceedings in Informatics, vol. 141, pp. 23:1-23:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019) · Zbl 07649972 |
| [23] | Maddux, R.D.: Relation Algebras. Elsevier B.V. (2006) · Zbl 1197.03051 |
| [24] | Nešetřil, J.; Milková, E.; Nešetřilová, H., Otakar Borůvka on minimum spanning tree problem – translation of both the 1926 papers, comments, history, Discret. Math., 233, 1-3, 3-36 (2001) · Zbl 0999.01019 · doi:10.1016/S0012-365X(00)00224-7 |
| [25] | Nipkow, T., Winskel is (almost) right: towards a mechanized semantics textbook, Formal Aspects Comput., 10, 2, 171-186 (1998) · Zbl 0910.68138 · doi:10.1007/s001650050009 |
| [26] | Nipkow, T.: Hoare logics in Isabelle/HOL. In: Schwichtenberg, H., Steinbrüggen, R. (eds.) Proof and System-Reliability, pp. 341-367. Kluwer Academic Publishers (2002) · Zbl 1097.68632 |
| [27] | Nipkow, T.; Paulson, LC; Wenzel, M., Isabelle/HOL: A Proof Assistant for Higher-Order Logic (2002), Heidelberg: Springer, Heidelberg · Zbl 0994.68131 · doi:10.1007/3-540-45949-9 |
| [28] | Nipkow, T., Eberl, M., Haslbeck, M.P.L.: Verified textbook algorithms. A biased survey. In: Hung, D.V., Sokolsky, O. (eds.) Automated Technology for Verification and Analysis, ATVA 2020. LNCS, vol. 12302, pp. 25-53. Springer, Heidelberg (2020). doi:10.1007/978-3-030-59152-6_2 · Zbl 1517.68443 |
| [29] | Prim, RC, Shortest connection networks and some generalizations, Bell Syst. Tech. J., 36, 6, 1389-1401 (1957) · doi:10.1002/j.1538-7305.1957.tb01515.x |
| [30] | Robinson-O’Brien, N.: A formal correctness proof of Borůvka’s minimum spanning tree algorithm. Master’s thesis, University of Canterbury (2020). doi:10.26021/10196 |
| [31] | Schmidt, G., Ströhlein, T.: Relations and Graphs. Springer, Heidelberg (1993). doi:10.1007/978-3-642-77968-8 · Zbl 0900.68328 |
| [32] | Tarjan, R.E.: Data Structures and Network Algorithms, CBMS-NSF Regional Conference Series in Applied Mathematics, vol. 44. SIAM (1983) · Zbl 0584.68077 |
| [33] | Tarski, A., On the calculus of relations, J. Symbolic Logic, 6, 3, 73-89 (1941) · JFM 67.0973.02 · doi:10.2307/2268577 |
| [34] | Yao, ACC, An \(\text{O}(|E| \log \log |V|)\) algorithm for finding minimum spanning trees, Inf. Process. Lett., 4, 1, 21-23 (1975) · Zbl 0307.68028 · doi:10.1016/0020-0190(75)90056-3 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
