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

Mouna Chaouch-Saad, Bernadette Charron-Bost, and Stephan Merz

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.

© Springer-Verlag 2009

Available as: PDF

Reference

@InProceedings{saad:reduction,
  author = 	 {Mouna Chaouch-Saad and Bernadette Charron-Bost and Stephan Merz},
  title = 	 {A Reduction Theorem for the Verification of Round-Based Distributed Algorithms},
  booktitle = {Reachability Problems '09},
  pages = 	 {93--106},
  year = 	 2009,
  editor = 	 {Olivier Bournez and Igor Potapov},
  volume = 	 5797,
  series = 	 {Lecture Notes in Computer Science},
  address = 	 {Palaiseau, France},
  publisher = {Springer},
}