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 SynthesisArticle

Authors: Swen Jacobs ORCID; Roderick Bloem ORCID

    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
    Imported on: September 30, 2012
    Keywords: Computer Science - Logic in Computer Science
    Funding:
      Source : OpenAIRE Graph
    • Diagnosis, Error Modelling and Correction for Reliable Systems Design; Funder: European Commission; Code: 248613

    20 Documents citing this article

    Consultation statistics

    This page has been seen 1177 times.
    This article's PDF has been downloaded 488 times.