Parameterized synthesis

DOI10.1007/978-3-642-28756-5_25zbMATH Open1352.68155arXiv1401.3588OpenAlexW2913930975MaRDI QIDQ2894282FDOQ2894282

Authors: Swen Jacobs, Roderick Bloem 

Publication date: 29 June 2012

Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Abstract: 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 LTLX, 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.

Full work available at URL: https://arxiv.org/abs/1401.3588

Recommendations

• Parameterized Synthesis
• Towards efficient parameterized synthesis
• Distributed synthesis for parameterized temporal logics
• Parameterized synthesis with safety properties
• Bounded Synthesis

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Distributed systems (68M14)

Cited In (15)

• Symmetric synthesis
• Synthesis problems for one-counter automata
• Parameterized model checking of rendezvous systems
• Parameterized synthesis with safety properties
• Towards efficient parameterized synthesis
• Automated synthesis of distributed self-stabilizing protocols
• Compositional parameter synthesis
• Distributed synthesis for parameterized temporal logics
• Distributed PROMPT-LTL synthesis
• Synchronous counting and computational algorithm design
• Graph Games and Reactive Synthesis
• Parameterized Synthesis
• Round-bounded control of parameterized systems
• Accelerating parameter synthesis using semi-algebraic constraints
• Synthesis of distributed algorithms with parameterized threshold guards

This page was built for publication: Parameterized synthesis

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2894282)