Constrained synthesis from component libraries

No Thumbnail Available

Access rights

openAccess
publishedVersion

URL

Journal Title

Journal ISSN

Volume Title

A1 Alkuperäisartikkeli tieteellisessä aikakauslehdessä

Date

2019-02-15

Major/Subject

Mcode

Degree programme

Language

en

Pages

21

Series

Science of Computer Programming, Volume 171, pp. 21-41

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.

Description

Embargo 24 kk

Keywords

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

Other note

Citation

Iannopollo, A, Tripakis, S & Sangiovanni-Vincentelli, A 2019, ' Constrained synthesis from component libraries ', Science of Computer Programming, vol. 171, pp. 21-41 . https://doi.org/10.1016/j.scico.2018.10.003