Revisited Convergence of Dolev et al BFS Spanning Tree Algorithm

TL;DR

This paper provides a constructive proof of the convergence of Dolev et al's BFS spanning tree algorithm under general unfair daemon assumptions, formalized in a Coq-based certification framework.

Contribution

It introduces a constructive, formal proof of convergence applicable to broad daemon conditions, improving upon previous non-constructive or restricted proofs.

Findings

Constructive proof of convergence under unfair daemon

Formalization in Coq-based PADEC framework

Addresses limitations of previous proofs

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.