Compositional High-Quality Synthesis

(2023) Compositional High-Quality Synthesis. (In Press)

Text main.pdf - Accepted Version Download (466kB)

Abstract

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.

Item Type:	Conference or Workshop Item (A Paper) (Paper)
Divisions:	Rayna Dimitrova (RD)
Conference:	ATVA International Symposium on Automated Technology for Verification and Analysis
Depositing User:	Rayna Dimitrova
Date Deposited:	29 Aug 2023 06:19
Last Modified:	29 Aug 2023 06:19
Primary Research Area:	NRA2: Reliable Security Guarantees
URI:	https://publications.cispa.saarland/id/eprint/4021

Actions

Actions (login required)

View Item