Jacobs, Swen and Bloem, Roderick - Parameterized Synthesis

lmcs:736 - Logical Methods in Computer Science, February 13, 2014, Volume 10, Issue 1
Parameterized Synthesis

Authors: Jacobs, Swen and Bloem, Roderick

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.


Source : oai:arXiv.org:1401.3588
DOI : 10.2168/LMCS-10(1:12)2014
Volume: Volume 10, Issue 1
Published on: February 13, 2014
Submitted on: September 30, 2012
Keywords: Computer Science - Logic in Computer Science


Share

Consultation statistics

This page has been seen 78 times.
This article's PDF has been downloaded 102 times.