Swen Jacobs ; Roderick Bloem - Parameterized Synthesis

lmcs:736 - Logical Methods in Computer Science, February 13, 2014, Volume 10, Issue 1 - https://doi.org/10.2168/LMCS-10(1:12)2014
Parameterized Synthesis

Authors: Swen Jacobs ORCID-iD; Roderick Bloem ORCID-iD

    We study the synthesis problem for distributed architectures with a parametric number of finite-state components. Parameterized specifications arise naturally in a synthesis setting, but thus far it was unclear how to detect realizability and how to perform synthesis in a parameterized setting. Using a classical result from verification, we show that for a class of specifications in indexed LTL\X, parameterized synthesis in token ring networks is equivalent to distributed synthesis in a network consisting of a few copies of a single process. Adapting a well-known result from distributed synthesis, we show that the latter problem is undecidable. We describe a semi-decision procedure for the parameterized synthesis problem in token rings, based on bounded synthesis. We extend the approach to parameterized synthesis in token-passing networks with arbitrary topologies, and show applicability on a simple case study. Finally, we sketch a general framework for parameterized synthesis based on cutoffs and other parameterized verification techniques.

    Volume: Volume 10, Issue 1
    Published on: February 13, 2014
    Accepted on: June 25, 2015
    Submitted on: September 30, 2012
    Keywords: Computer Science - Logic in Computer Science
    Fundings :
      Source : OpenAIRE Research Graph
    • Diagnosis, Error Modelling and Correction for Reliable Systems Design; Funder: European Commission; Code: 248613

    Linked data

    Source : ScholeXplorer IsReferencedBy DOI 10.1007/978-3-662-49122-5_23
    • 10.1007/978-3-662-49122-5_23
    • 10.1007/978-3-662-49122-5_23
    • 10.1007/978-3-662-49122-5_23
    Tight Cutoffs for Guarded Protocols with Fairness
    Außerlechner, Simon ; Jacobs, Swen ; Khalimov, Ayrat ;

    18 Documents citing this article


    Consultation statistics

    This page has been seen 532 times.
    This article's PDF has been downloaded 431 times.