arXiv · 2502.17035
Revisited Convergence of Dolev et al BFS Spanning Tree Algorithm
Abstract
We provide a constructive proof for the convergence of Dolev et al's BFS spanning tree algorithm running under the general assumption of an unfair daemon. Already known proofs of this algorithm are either using non-constructive principles (e.g., proofs by contradiction) or are restricted to less general execution daemons (e.g., weakly fair). In this work, we address these limitations by defining the well-founded orders and potential functions ensuring convergence in the general case. The proof has been fully formalized in PADEC, a Coq-based framework for certification of self-stabilization algorithm.
Explore related subjects
Keep this discovery
Karine Altisen, Marius Bozga. 2025-02-24. Revisited Convergence of Dolev et al BFS Spanning Tree Algorithm. https://arxiv.org/abs/2502.17035
Cite the original work for its findings. Save a collection to share your selection of sources.