CISPA
Browse
cispa_all_3009.pdf (499.64 kB)

Parameterized synthesis of self-stabilizing protocols in symmetric networks

Download (499.64 kB)
journal contribution
posted on 2023-11-29, 18:07 authored by Nahal Mirzaie, Fathiyeh Faghih, Swen JacobsSwen Jacobs, Borzoo Bonakdarpour
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.

History

Preferred Citation

Nahal Mirzaie, Fathiyeh Faghih, Swen Jacobs and Borzoo Bonakdarpour. Parameterized synthesis of self-stabilizing protocols in symmetric networks. In: Acta Informatica. 2019.

Primary Research Area

  • Reliable Security Guarantees

Legacy Posted Date

2020-02-27

Journal

Acta Informatica

Open Access Type

  • Green

Sub Type

  • Article

BibTeX

@article{cispa_all_3009, title = "Parameterized synthesis of self-stabilizing protocols in symmetric networks", author = "Mirzaie, Nahal and Faghih, Fathiyeh and Jacobs, Swen and Bonakdarpour, Borzoo", journal="{Acta Informatica}", year="2019", }

Usage metrics

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC