Constrained synthesis from component libraries

Antonio Iannopollo*, Stavros Tripakis, Alberto Sangiovanni-Vincentelli

*Corresponding author for this work

Research output: Contribution to journalArticleScientificpeer-review

1 Citation (Scopus)

Abstract

Synthesis from component libraries is the problem of building a network of components from a given library, such that the network realizes a given specification. This problem is undecidable in general. It becomes decidable if we impose a bound on the number of chosen components. However, the bounded problem remains computationally hard and brute-force approaches do not scale. In this paper, we study scalable methods for solving the problem of bounded synthesis from libraries, proposing a solution based on the Counterexample-Guided Inductive Synthesis paradigm. Although our synthesis algorithm does not assume a specific formalism a priori, we present a parallel implementation which instantiates components defined as Linear Temporal Logic-based Assume/Guarantee Contracts. We show the potential of our approach and evaluate our implementation by applying it to two industrial-relevant case studies.

Original languageEnglish
Pages (from-to)21-41
Number of pages21
JournalScience of Computer Programming
Volume171
DOIs
Publication statusPublished - 15 Feb 2019
MoE publication typeA1 Journal article-refereed

Keywords

  • Assume-guarantee contracts
  • Component libraries
  • Counterexample-guided inductive synthesis
  • Linear temporal logic
  • Platform-based design

Fingerprint Dive into the research topics of 'Constrained synthesis from component libraries'. Together they form a unique fingerprint.

  • Cite this