A Reduction Theorem for the Verification of Round-Based Distributed Algorithms - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2009

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

Résumé

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.

Dates et versions

inria-00408908 , version 1 (04-08-2009)

Identifiants

Citer

Mouna Chaouch-Saad, Bernadette Charron-Bost, Stephan Merz. A Reduction Theorem for the Verification of Round-Based Distributed Algorithms. Reachability Problems 2009, Sep 2009, Palaiseau, France. pp.93-106, ⟨10.1007/978-3-642-04420-5_10⟩. ⟨inria-00408908⟩
183 Consultations
0 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More