CISPA
Browse
cispa_all_3441.pdf (319.56 kB)

Compositional Synthesis of Modular Systems

Download (319.56 kB)
conference contribution
posted on 2023-11-29, 18:16 authored by Bernd FinkbeinerBernd Finkbeiner, Noemi Passing
Given the advances in reactive synthesis, it is a natural next step to consider more complex multi-process systems. Distributed synthesis, however, is not yet scalable. Compositional approaches can be a game changer. Here, the challenge is to decompose a given specification of the global system behavior into requirements on the individual processes. In this paper, we introduce a compositional synthesis algorithm that, for each process, constructs, in addition to the implementation, a certificate that captures the necessary interface between the processes. The certificates then allow for constructing separate requirements for the individual processes. By bounding the size of the certificates, we can bias the synthesis procedure towards solutions that are desirable in the sense that the assumptions between the processes are small. Our experimental results show that our approach is much faster than standard methods for distributed synthesis as long as reasonably small certificates exist.

History

Preferred Citation

Bernd Finkbeiner and Noemi Passing. Compositional Synthesis of Modular Systems. In: International Symposium on Automated Technology for Verification and Analysis (ATVA). 2021.

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

International Symposium on Automated Technology for Verification and Analysis (ATVA)

Legacy Posted Date

2021-07-09

Open Access Type

  • Unknown

BibTeX

@inproceedings{cispa_all_3441, title = "Compositional Synthesis of Modular Systems", author = "Finkbeiner, Bernd and Passing, Noemi", booktitle="{International Symposium on Automated Technology for Verification and Analysis (ATVA)}", year="2021", }

Usage metrics

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC