CISPA
Browse
cispa_all_3207.pdf (521.88 kB)

Dependency-based Compositional Synthesis

Download (521.88 kB)
conference contribution
posted on 2023-11-29, 18:13 authored by Bernd FinkbeinerBernd Finkbeiner, Noemi Passing
Despite many recent advances, reactive synthesis is still not really a practical technique. The grand challenge is to scale from small transition systems, where synthesis performs well, to complex multi-component designs. Compositional methods, such as the construction of dominant strategies for individual components, reduce the complexity significantly, but are usually not applicable without extensively rewriting the specification. In this paper, we present a refinement of compositional synthesis that does not require such an intervention. Our algorithm decomposes the system into a sequence of components, such that every component has a strategy that is dominant, i.e., performs at least as good as any possible alternative, provided that the preceding components follow their (already synthesized) strategies. The decomposition of the system is based on a dependency analysis, for which we provide semantic and syntactic techniques. We establish the soundness and completeness of the approach and report on encouraging experimental results.

History

Preferred Citation

Bernd Finkbeiner and Noemi Passing. Dependency-based Compositional Synthesis. In: International Symposium on Automated Technology for Verification and Analysis (ATVA). 2020.

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

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

Legacy Posted Date

2020-10-19

Open Access Type

  • Unknown

BibTeX

@inproceedings{cispa_all_3207, title = "Dependency-based Compositional Synthesis", author = "Finkbeiner, Bernd and Passing, Noemi", booktitle="{International Symposium on Automated Technology for Verification and Analysis (ATVA)}", year="2020", }

Usage metrics

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC