(2022) Compositional synthesis of modular systems.
Abstract
In contrast to the breakthroughs in reactive synthesis of monolithic systems, distributed synthesis is not yet practical. Compositional approaches can be a key technique for scalable algorithms. Here, the challenge is to decompose a specification of the global system into local requirements on the individual processes. In this paper, we present and extend a sound and complete compositional synthesis algorithm that constructs for each process, in addition to the strategy, a certificate that captures the necessary interface between the processes. The certificates define an assume-guarantee contract that allows for formulating individual process requirements. By bounding the size of the certificates, we then bias the synthesis procedure towards solutions that are desirable in the sense that they have a small interface. We have implemented our approach and evaluated it on scalable benchmarks: It is much faster than standard methods for distributed synthesis as long as reasonably small certificates exist. Otherwise, the overhead of synthesizing additional certificates is small.
| Item Type: | Article |
|---|---|
| Additional Information: | Journal Version of the ATVA 2021 paper "Compositional Synthesis of Modular Systems". |
| Divisions: | Bernd Finkbeiner (Reactive Systems Group, RSG) |
| Depositing User: | Noemi Passing |
| Date Deposited: | 06 May 2022 09:02 |
| Last Modified: | 06 May 2022 09:02 |
| Primary Research Area: | NRA2: Reliable Security Guarantees |
| URI: | https://publications.cispa.saarland/id/eprint/3664 |
Actions
Actions (login required)
 |
View Item |