CISPA
Browse
cispa_all_2805.pdf (516.5 kB)

Parameterized Synthesis of Self-Stabilizing Protocols in Symmetric Rings

Download (516.5 kB)
conference contribution
posted on 2023-11-29, 18:09 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 rings. First, we develop tight cutoffs that guarantee (1) closure in legitimate states, and (2) deadlock-freedom outside the legitimates states. We also develop a sufficient condition for convergence in silent self-stabilizing systems. Since some of our cutoffs grow with the size of local state space of processes, we also present an automated technique that significantly increases the scalability of synthesis in symmetric networks. Our technique is based on SMT-solving and incorporates a loop of synthesis and verification guided by counterexamples. We have fully implemented our technique and successfully synthesized solutions to maximal matching, three coloring, and maximal independent set problems.

History

Preferred Citation

Nahal Mirzaie, Fathiyeh Faghih, Swen Jacobs and Borzoo Bonakdarpour. Parameterized Synthesis of Self-Stabilizing Protocols in Symmetric Rings. In: International Conference on Principles of Distributed Systems (OPODIS). 2018.

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

International Conference on Principles of Distributed Systems (OPODIS)

Legacy Posted Date

2019-02-28

Open Access Type

  • Unknown

BibTeX

@inproceedings{cispa_all_2805, title = "Parameterized Synthesis of Self-Stabilizing Protocols in Symmetric Rings", author = "Mirzaie, Nahal and Faghih, Fathiyeh and Jacobs, Swen and Bonakdarpour, Borzoo", booktitle="{International Conference on Principles of Distributed Systems (OPODIS)}", year="2018", }

Usage metrics

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC