# Parameterized Synthesis

arXiv: https://arxiv.org/abs/1401.3588 · HTML: https://mlsanity.com/paper/1401.3588/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 15 Jan 2014.

## Built on by (most cited first, 2 of 2)

- [Learning Broadcast Protocols](https://mlsanity.com/paper/2306.14284/) (2023)
- [Natural Synthesis: Outperforming Reactive Synthesis Tools with Large Reasoning Models](https://mlsanity.com/paper/2605.15131/) (2026)

## Abstract (arXiv)

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.