×

zbMATH — the first resource for mathematics

Verifying minimum spanning tree algorithms with Stone relation algebras. (English) Zbl 1401.68247
Summary: We study a generalisation of relation algebras in which the underlying Boolean algebra structure is replaced with a Stone algebra. Many theorems of relation algebras generalise with no or small changes. Weighted graphs represented as matrices over extended real numbers form an instance. Relational concepts and methods can thus be applied to weighted graphs. We formally specify the problem of computing minimum spanning forests and express Kruskal’s algorithm in relation-algebraic terms. We give a total-correctness proof of the algorithm. All results are formally verified in Isabelle/HOL.
This paper is an extended version of [the author, Lect. Notes Comput. Sci. 10226, 127–143 (2017; Zbl 1402.03099)].

MSC:
68R10 Graph theory (including graph drawing) in computer science
03B35 Mechanization of proofs and logical operations
03G15 Cylindric and polyadic algebras; relation algebras
05C22 Signed and weighted graphs
68Q60 Specification and verification (program logics, model checking, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Abrial, J.-R.; Cansell, D.; Méry, D., Formal derivation of spanning trees algorithms, (Bert, D.; Bowen, J. P.; King, S.; Waldén, M., ZB 2003: Formal Specification and Development in Z and B, LNCS, vol. 2651, (2003), Springer), 457-476 · Zbl 1028.68945
[2] Aho, A. V.; Hopcroft, J. E.; Ullman, J. D., The design and analysis of computer algorithms, (1974), Addison-Wesley Publishing Company · Zbl 0326.68005
[3] Andréka, H.; Mikulás, Sz., Axiomatizability of positive algebras of binary relations, Algebra Univers., 66, 1-2, 7-34, (2011) · Zbl 1253.03091
[4] Armstrong, A.; Foster, S.; Struth, G.; Weber, T., Relation algebra, (2016), Archive of Formal Proofs, first version 2014
[5] Armstrong, A.; Gomes, V. B.F.; Struth, G.; Weber, T., Kleene algebra, (2016), Archive of Formal Proofs, first version 2013
[6] Asplund, T., Formalizing the Kleene star for square matrices, (2014), Uppsala Universitet, Department of Information Technology, Bachelor Thesis IT 14 002
[7] Backhouse, R. C.; Carré, B. A., Regular algebra applied to path-finding problems, J. Inst. Math. Appl., 15, 2, 161-186, (1975) · Zbl 0304.68082
[8] Balbes, R.; Dwinger, P., Distributive lattices, (1974), University of Missouri Press · Zbl 0321.06012
[9] Balbes, R.; Grätzer, G., Injective and projective stone algebras, Duke Math. J., 38, 2, 339-347, (1971) · Zbl 0219.06005
[10] Berghammer, R.; Fischer, S., Combining relation algebra and data refinement to develop rectangle-based functional programs for reflexive-transitive closures, J. Log. Algebraic Methods Program., 84, 3, 341-358, (2015) · Zbl 1329.68062
[11] 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
[12] Berghammer, R.; von Karger, B., Relational semantics of functional programs, (Brink, C.; Kahl, W.; Schmidt, G., Relational Methods in Computer Science, (1997), Springer Wien), 115-130, chapter 8 · Zbl 0884.68077
[13] Berghammer, R.; von Karger, B.; Wolf, A., Relation-algebraic derivation of spanning tree algorithms, (Jeuring, J., MPC 1998, LNCS, vol. 1422, (1998), Springer), 23-43 · Zbl 0905.68020
[14] Bird, R.; de Moor, O., Algebra of programming, (1997), Prentice Hall · Zbl 0867.68042
[15] Birkhoff, G., Lattice theory, Colloquium Publications, vol. XXV, (1967), American Mathematical Society · Zbl 0126.03801
[16] Bistarelli, S.; Santini, F., C-semiring frameworks for minimum spanning tree problems, (Corradini, A.; Montanari, U., Recent Trends in Algebraic Development Techniques, LNCS, vol. 5486, (2009), Springer), 56-70 · Zbl 1253.68370
[17] Blanchette, J. C.; Böhme, S.; Paulson, L. C., Extending sledgehammer with SMT solvers, (Bjørner, N.; Sofronie-Stokkermans, V., CADE 2011, LNCS, vol. 6803, (2011), Springer), 116-130 · Zbl 1314.68271
[18] Blanchette, J. C.; Nipkow, T., Nitpick: a counterexample generator for higher-order logic based on a relational model finder, (Kaufmann, M.; Paulson, L. C., ITP 2010, LNCS, vol. 6172, (2010), Springer), 131-146 · Zbl 1291.68326
[19] Blyth, T. S., Lattices and ordered algebraic structures, (2005), Springer · Zbl 1073.06001
[20] Bredihin, D. A.; Schein, B. M., Representations of ordered semigroups and lattices by binary relations, Colloq. Math., 39, 1, 1-12, (1978) · Zbl 0389.06013
[21] Comer, S. D., On connections between information systems, rough sets and algebraic logic, (Rauszer, C., Algebraic Methods in Logic and in Computer Science, Banach Center Publications, vol. 28, (1993), Institute of Mathematics, Polish Academy of Sciences), 117-124 · Zbl 0793.03074
[22] Conway, J. H., Regular algebra and finite machines, (1971), Chapman and Hall · Zbl 0231.94041
[23] Cormen, T. H.; Leiserson, C. E.; Rivest, R. L., Introduction to algorithms, (1990), MIT Press · Zbl 1158.68538
[24] Curry, H. B., Foundations of mathematical logic, (1977), Dover Publications · Zbl 0396.03001
[25] Desharnais, J.; Grinenko, A.; Möller, B., Relational style laws and constructs of linear algebra, J. Log. Algebraic Methods Program., 83, 2, 154-168, (2014) · Zbl 1434.15016
[26] Desharnais, J.; Struth, G., Internal axioms for domain semirings, Sci. Comput. Program., 76, 3, 181-203, (2011) · Zbl 1211.68242
[27] Düntsch, I.; Gediga, G.; Orłowska, E., Relational attribute systems II: reasoning with relations in information structures, (Peters, J. F.; Skowron, A.; Marek, V. W.; Orłowska, E.; Słowiński, R.; Ziarko, W., Transactions on Rough Sets VII, LNCS, vol. 4400, (2007), Springer), 16-35 · Zbl 1187.68190
[28] Düntsch, I.; Winter, M., Rough relation algebras revisited, Fundam. Inform., 74, 2-3, 283-300, (2006) · Zbl 1110.03061
[29] Fraer, R., Minimum spanning tree, (Sekerinski, E.; Sere, K., Program Development by Refinement, (1999), Springer), 79-114, chapter 3
[30] Freyd, P. J.; Ščedrov, A., Categories, allegories, North-Holland Mathematical Library, vol. 39, (1990), Elsevier Science Publishers · Zbl 0698.18002
[31] Frias, M. F.; Aguayo, N.; Novak, B., Development of graph algorithms with fork algebras, (XIX Conferencia Latinoamericana de Informática, (1993)), 529-554
[32] Fried, E.; Hansoul, G. E.; Schmidt, E. T.; Varlet, J. C., Perfect distributive lattices, (Eigenthaler, G.; Kaiser, H. K.; Müller, W. B.; Nöbauer, W., Contributions to General Algebra, vol. 3, (1985), Hölder-Pichler-Tempsky), 125-142 · Zbl 0572.06009
[33] Goguen, J. A., L-fuzzy sets, J. Math. Anal. Appl., 18, 1, 145-174, (1967) · Zbl 0145.24404
[34] Gondran, M.; Minoux, M., Graphs, dioids and semirings, (2008), Springer · Zbl 1201.16038
[35] Grätzer, G., Lattice theory: first concepts and distributive lattices, (1971), W. H. Freeman and Co · Zbl 0232.06001
[36] Guttmann, W., Algebras for iteration and infinite computations, Acta Inform., 49, 5, 343-359, (2012) · Zbl 1279.68078
[37] Guttmann, W., Relation-algebraic verification of Prim’s minimum spanning tree algorithm, (Sampaio, A.; Wang, F., ICTAC 2016, LNCS, vol. 9965, (2016), Springer), 51-68 · Zbl 1400.68155
[38] Guttmann, W., Stone algebras, (2016), Archive of Formal Proofs
[39] Guttmann, W., Stone-Kleene relation algebras, (2017), Archive of Formal Proofs
[40] Guttmann, W., Stone relation algebras, (Höfner, P.; Pous, D.; Struth, G., Relational and Algebraic Methods in Computer Science, LNCS, vol. 10226, (2017), Springer), 127-143 · Zbl 1402.03099
[41] Guttmann, W., Stone relation algebras, (2017), Archive of Formal Proofs · Zbl 1402.03099
[42] Guttmann, W., An algebraic framework for minimum spanning tree problems, Theor. Comput. Sci., (2018) · Zbl 1401.68246
[43] Hirsch, R.; Hodkinson, I., Relation algebras by games, (2002), Elsevier Science B.V. · Zbl 1018.03002
[44] Höfner, P.; Möller, B., Dijkstra, floyd and warshall meet Kleene, Form. Asp. Comput., 24, 4, 459-476, (2012) · Zbl 1259.68243
[45] Kawahara, Y.; Furusawa, H., Crispness in Dedekind categories, Bull. Inform. Cybernet., 33, 1-2, 1-18, (2001) · Zbl 1270.18008
[46] Kawahara, Y.; Furusawa, H.; Mori, M., Categorical representation theorems of fuzzy relations, Inf. Sci., 119, 3-4, 235-251, (1999) · Zbl 0943.03042
[47] Killingbeck, D.; Teixeira, M. S.; Winter, M., Relations among matrices over a semiring, (Kahl, W.; Winter, M.; Oliveira, J. N., RAMiCS 2015, LNCS, vol. 9348, (2015), Springer), 101-118 · Zbl 06527603
[48] Kozen, D., A completeness theorem for Kleene algebras and the algebra of regular events, Inf. Comput., 110, 2, 366-390, (1994) · Zbl 0806.68082
[49] Kozen, D., Kleene algebra with tests, ACM Trans. Program. Lang. Syst., 19, 3, 427-443, (1997)
[50] Kruskal, J. B., 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
[51] Macedo, H. D.; Oliveira, J. N., A linear algebra approach to OLAP, Form. Asp. Comput., 27, 2, 283-307, (2015) · Zbl 1331.68055
[52] Maddux, R. D., Relation-algebraic semantics, Theor. Comput. Sci., 160, 1-2, 1-85, (1996) · Zbl 0872.68106
[53] Maddux, R. D., Relation algebras, (2006), Elsevier B.V. · Zbl 1197.03051
[54] Nipkow, T., Winskel is (almost) right: towards a mechanized semantics textbook, Form. Asp. Comput., 10, 2, 171-186, (1998) · Zbl 0910.68138
[55] Nipkow, T., Hoare logics in isabelle/HOL, (Schwichtenberg, H.; Steinbrüggen, R., Proof and System-Reliability, (2002), Kluwer Academic Publishers), 341-367 · Zbl 1097.68632
[56] Nipkow, T.; Klein, G., Concrete semantics, (2014), Springer · Zbl 1410.68004
[57] Nipkow, T.; Paulson, L. C.; Wenzel, M., Isabelle/HOL: A proof assistant for higher-order logic, LNCS, vol. 2283, (2002), Springer · Zbl 0994.68131
[58] Orłowska, E.; Radzikowska, A. M., Double residuated lattices and their applications, (de Swart, H. C.M., Relational Methods in Computer Science, LNCS, vol. 2561, (2002), Springer), 171-189 · Zbl 1027.68117
[59] Paulson, L. C.; Blanchette, J. C., Three years of experience with sledgehammer, a practical link between automatic and interactive theorem provers, (Sutcliffe, G.; Ternovska, E.; Schulz, S., Proceedings of the 8th International Workshop on the Implementation of Logics, (2010)), 3-13
[60] Pawlak, Z., Rough sets, rough relations and rough functions, Fundam. Inform., 27, 2-3, 103-108, (1996) · Zbl 0854.04008
[61] Schirmer, N., Verification of sequential imperative programs in isabelle/HOL, (2006), TU München, PhD thesis
[62] Schmid, J., Algebraically closed distributive p-algebras, Algebra Univers., 15, 126-141, (1982) · Zbl 0507.06009
[63] Schmidt, G.; Ströhlein, T., Relationen und graphen, (1989), Springer · Zbl 0705.68083
[64] Struth, G., Abstract abstract reduction, J. Log. Algebraic Program., 66, 2, 239-270, (2006) · Zbl 1086.68068
[65] Tarski, A., On the calculus of relations, J. Symb. Log., 6, 3, 73-89, (1941) · JFM 67.0973.02
[66] Winter, M., A new algebraic approach to L-fuzzy relations convenient to study crispness, Inf. Sci., 139, 3-4, 233-252, (2001) · Zbl 0992.18004
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.