A Reduction Theorem for the Verification of Round-Based Distributed Algorithms

Abstract : We consider the verification of algorithms expressed in the Heard-Of Model, a round-based computational model for fault-tolerant distributed computing. Rounds in this model are communication-closed, and we show that every execution recording individual events corresponds to a coarser-grained execution based on global rounds such that the local views of all processes are identical in the two executions. This result helps us to substantially mitigate state-space explosion and verify Consensus algorithms using standard model checking techniques.
Type de document :
Communication dans un congrès
Olivier Bournez and Igor Potapov. Reachability Problems 2009, Sep 2009, Palaiseau, France. Springer Berlin / Heidelberg, 5797, pp.93-106, 2009, Lecture Notes in Computer Science. 〈10.1007/978-3-642-04420-5_10〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00408908
Contributeur : Stephan Merz <>
Soumis le : mardi 4 août 2009 - 12:09:50
Dernière modification le : jeudi 11 janvier 2018 - 06:19:52

Identifiants

Collections

Citation

Mouna Chaouch-Saad, Bernadette Charron-Bost, Stephan Merz. A Reduction Theorem for the Verification of Round-Based Distributed Algorithms. Olivier Bournez and Igor Potapov. Reachability Problems 2009, Sep 2009, Palaiseau, France. Springer Berlin / Heidelberg, 5797, pp.93-106, 2009, Lecture Notes in Computer Science. 〈10.1007/978-3-642-04420-5_10〉. 〈inria-00408908〉

Partager

Métriques

Consultations de la notice

295