Synthesizing optimal bias in randomized self-stabilization

Distributed Computing, vol. 35, pp. 37–57

Abstract

Abstract Randomization is a key concept in distributed computing to tackle impossibility results. This also holds for self-stabilization in anonymous networks where coin flips are often used to break symmetry. Although the use of randomization in self-stabilizing algorithms is rather common, it is unclear what the optimal coin bias is so as to minimize the expected convergence time. This paper proposes a technique to automatically synthesize this optimal coin bias. Our algorithm is based on a parameter synthesis approach from the field of probabilistic model checking. It over- and under-approximates a given parameter region and iteratively refines the regions with minimal convergence time up to the desired accuracy. We describe the technique in detail and present a simple parallelization that gives an almost linear speed-up. We show the applicability of our technique to determine the optimal bias for the well-known Herman’s self-stabilizing token ring algorithm. Our synthesis obtains that for small rings, a fair coin is optimal, whereas for larger rings a biased coin is optimal where the bias grows with the ring size. We also analyze a variant of Herman’s algorithm that coincides with the original algorithm but deviates for biased coins. Finally, we show how using speed reducers in Herman’s protocol improve the expected convergence time.

Authors 4

1. Matthias Volk corresponding Aachen Software Modeling and Verification Group

   RWTH Aachen University · University of Twente

   Affiliation as printed

   Present Address: Formal Methods and Tools, University of Twente, Enschede, The Netherlands

   Software Modeling and Verification Group, RWTH Aachen University, Aachen, Germany

   Formal Methods and Tools, University of Twente, Enschede, The Netherlands

2. Borzoo Bonakdarpour

   Michigan State University

   Affiliation as printed

   Department of Computer Science, Michigan State University, East Lansing, USA

3. Joost-Pieter Katoen Aachen Software Modeling and Verification Group

   RWTH Aachen University

   Affiliation as printed

   Software Modeling and Verification Group, RWTH Aachen University, Aachen, Germany

4. Saba Aflaki
   Affiliation as printed

   Index Exchange, Toronto, Canada