TY - GEN
T1 - A reduction theorem for the verification of round-based distributed algorithms
AU - Chaouch-Saad, Mouna
AU - Charron-Bost, Bernadette
AU - Merz, Stephan
PY - 2009/1/1
Y1 - 2009/1/1
N2 - 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.
AB - 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.
U2 - 10.1007/978-3-642-04420-5_10
DO - 10.1007/978-3-642-04420-5_10
M3 - Conference contribution
AN - SCOPUS:70349969703
SN - 3642044190
SN - 9783642044199
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 93
EP - 106
BT - Reachability Problems - 3rd International Workshop, RP 2009, Proceedings
PB - Springer Verlag
T2 - 3rd International Workshop on Reachability Problems, RP 2009
Y2 - 23 September 2009 through 25 September 2009
ER -