Paper Info
Title
An algebraic framework for minimum spanning tree problems.
Abstract
We formally prove that Prim's minimum spanning tree algorithm is correct for various optimisation problems with different aggregation functions. The original minimum weight spanning tree problem and the minimum bottleneck spanning tree problem are special cases, but the framework covers many other problems. To this end we work in new generalisations of relation algebras and Kleene algebras and in new algebraic structures that capture key operations used in Prim's algorithm and its specification. Weighted graphs form instances of these algebraic structures, where edge weights are taken from a linear order with a binary aggregation operation. Many existing results from relation algebras and Kleene algebras generalise from the relation model to the weighted-graph model with no or small changes. The overall structure of the proof uses Hoare logic. All results are formally verified in Isabelle/HOL heavily using its integrated automated theorem provers. This paper is an extended version of [36].
Year
DOI
Venue
2018
10.1016/j.tcs.2018.04.012
Theoretical Computer Science
Keywords
Field
DocType
Aggregation,Correctness proof,Formal methods,Kleene algebras,Relations,Stone algebras,Weighted graphs
HOL,Discrete mathematics,Minimum bottleneck spanning tree,Algebraic number,Algebraic structure,Hoare logic,Minimum weight,Spanning tree,Mathematics,Minimum spanning tree
Journal
Volume
ISSN
Citations 
744
0304-3975
1
PageRank 
References 
Authors
0.36
19
1
Name
Order
Citations
PageRank
Walter Guttmann119616.53