Revisited Convergence of Dolev et al BFS Spanning Tree Algorithm
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866910842548649984 |
|---|---|
| author | Altisen, Karine Bozga, Marius |
| author_facet | Altisen, Karine Bozga, Marius |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2502_17035 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Revisited Convergence of Dolev et al BFS Spanning Tree Algorithm Altisen, Karine Bozga, Marius Distributed, Parallel, and Cluster Computing Logic in Computer Science 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. |
| title | Revisited Convergence of Dolev et al BFS Spanning Tree Algorithm |
| topic | Distributed, Parallel, and Cluster Computing Logic in Computer Science |
| url | https://arxiv.org/abs/2502.17035 |