Back to Search
Start Over
Relation-Algebraic Verification of Prim’s Minimum Spanning Tree Algorithm
- Source :
- Theoretical Aspects of Computing – ICTAC 2016 ISBN: 9783319467498, ICTAC
- Publication Year :
- 2016
- Publisher :
- Springer International Publishing, 2016.
-
Abstract
- We formally prove the correctness of Prim’s algorithm for computing minimum spanning trees. We introduce new generalisations of relation algebras and Kleene algebras, in which most of the proof can be carried out. Only a small part needs additional operations, for which we introduce a new algebraic structure. We instantiate these algebras by matrices over extended reals, which model the weighted graphs used in the algorithm. 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.
- Subjects :
- Discrete mathematics
Correctness
Spanning tree
Edmonds' algorithm
Prim's algorithm
0102 computer and information sciences
02 engineering and technology
Minimum spanning tree
Hoare logic
01 natural sciences
Distributed minimum spanning tree
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES
010201 computation theory & mathematics
Kruskal's algorithm
TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
Computer Science::Logic in Computer Science
ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION
0202 electrical engineering, electronic engineering, information engineering
020201 artificial intelligence & image processing
Mathematics
Subjects
Details
- ISBN :
- 978-3-319-46749-8
- ISBNs :
- 9783319467498
- Database :
- OpenAIRE
- Journal :
- Theoretical Aspects of Computing – ICTAC 2016 ISBN: 9783319467498, ICTAC
- Accession number :
- edsair.doi...........050f59b611094c6329e13a21bf91c0ad