CISPA
Browse
cispa_all_4021.pdf (455.91 kB)

Compositional High-Quality Synthesis

Download (455.91 kB)
conference contribution
posted on 2024-03-05, 12:15 authored by Rafael DewesRafael Dewes, Rayna DimitrovaRayna Dimitrova
Over the last years, there has been growing interest in synthesizing reactive systems from quantitative specifications, with the goal of constructing correct and high-quality systems. Considering quantitative requirements in systems consisting of multiple components is challenging not only because of scalability limitations but also due to the intricate interplay between the different possibilities of satisfying a specification and the required cooperation between components. Compositional synthesis holds the promise of addressing these challenges. We study the compositional synthesis of reactive systems consisting of multiple components, from requirements specified in a fragment of the logic LTL[F], which extends LTL with quality operators. We consider specifications that are combinations of local and shared quantitative requirements. We present a sound decomposition rule that allows for synthesizing one component at a time. The decomposition requires assume-guarantee contracts between the components, and we provide a method for iteratively refining the assumptions and guarantees. We evaluate our approach with a prototype implementation, demonstrating its advantages over monolithic synthesis and ability to generate decompositions.

History

Preferred Citation

Rafael Dewes, Rayna Dimitrova. Compositional High-Quality Synthesis. In: Proceedings of the 21st International Symposium on Automated Technology for Verification and Analysis. 2023.

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

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

Legacy Posted Date

2023-08-29

Publisher

Springer

Open Access Type

  • Unknown

BibTeX

@inproceedings{cispa_all_4021, author = {Rafael Dewes AND Rayna Dimitrova}, title = {Compositional High-Quality Synthesis}, booktitle = {Proceedings of the 21st International Symposium on Automated Technology for Verification and Analysis}, year = {2023} }

Usage metrics

    Categories

    No categories selected

    Licence

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC