A Reduction Theorem for the Verification of Round-Based Distributed Algorithms - Inria - Institut national de recherche en sciences et technologies du numérique Access content directly
Conference Papers Year : 2009

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.

Dates and versions

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

Identifiers

Cite

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⟩
182 View
0 Download

Altmetric

Share

Gmail Facebook X LinkedIn More