Compositional synthesis of modular systems
Bernd Finkbeiner, Noemi Passing
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.
Innovations in Systems and Software Design, ATVA 2021 Special Issue (ISSE 2022).
The final publication is available at link.springer.com. This is the extended journal version of the ATVA 2021 paper.