Abstract | ||
---|---|---|
Self-stabilization in distributed systems is a technique to guarantee convergence to a set of legitimate states without external intervention when a transient fault or bad initialization occurs. Recently, there has been a surge of efforts in designing techniques for automated synthesis of self-stabilizing algorithms that are correct by construction. Most of these techniques, however, are not parameterized, meaning that they can only synthesize a solution for a fixed and predetermined number of processes. In this paper, we report a breakthrough in parameterized synthesis of self-stabilizing algorithms in symmetric networks, including ring, line, mesh, and torus. First, we develop cutoffs that guarantee (1) closure in legitimate states, and (2) deadlock-freedom outside the legitimate states. We also develop a sufficient condition for convergence in self-stabilizing systems. Since some of our cutoffs grow with the size of the local state space of processes, scalability of the synthesis procedure is still a problem. We address this problem by introducing a novel SMT-based technique for counterexample-guided synthesis of self-stabilizing algorithms in symmetric networks. We have fully implemented our technique and successfully synthesized solutions to maximal matching, three coloring, and maximal independent set problems for ring and line topologies. |
Year | DOI | Venue |
---|---|---|
2020 | 10.1007/s00236-019-00361-7 | Acta Informatica |
DocType | Volume | Issue |
Journal | 57 | 1 |
ISSN | Citations | PageRank |
0001-5903 | 0 | 0.34 |
References | Authors | |
0 | 4 |
Name | Order | Citations | PageRank |
---|---|---|---|
Nahal Mirzaie | 1 | 0 | 0.34 |
Fathiyeh Faghih | 2 | 11 | 4.33 |
Swen Jacobs | 3 | 208 | 17.43 |
Borzoo Bonakdarpour | 4 | 490 | 45.02 |