1. Parameterized synthesis of self-stabilizing protocols in symmetric networks.
- Author
-
Mirzaie, Nahal, Faghih, Fathiyeh, Jacobs, Swen, and Bonakdarpour, Borzoo
- Subjects
- *
COMPUTER network protocols , *DESIGN techniques , *INDEPENDENT sets , *LEVEL set methods , *MATCHING theory , *TORUS , *SCALABILITY - 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. [ABSTRACT FROM AUTHOR]
- Published
- 2020
- Full Text
- View/download PDF