Compositional synthesis of modular systems

DOI10.1007/978-3-030-88885-5_20MaRDI QIDQ2147209zbMATH OpenOpenAlexFDO

Authors Bernd Finkbeiner, Noemi Passing

Publication date 22 June 2022

Full work available at URL https://arxiv.org/abs/2106.14783

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: 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.

Recommendations

• Dependency-Based Compositional Synthesis
• Automated Technology for Verification and Analysis
• SEMI-AUTOMATIC DISTRIBUTED SYNTHESIS
• Synthesis: words and traces
• Assume-guarantee synthesis for concurrent reactive programs with partial information

Cites work

• Assume-Guarantee Synthesis
• Assume-admissible synthesis
• Assume-guarantee synthesis for concurrent reactive programs with partial information
• Bounded Synthesis
• Compositional algorithms for LTL synthesis
• Encodings of bounded synthesis
• On the structure of non-manipulable equilibria
• Pattern-based refinement of assume-guarantee specifications in reactive synthesis
• Safraless Compositional Synthesis
• Testing language containment for \(\omega\)-automata using BDDs

Cited in

(13)

• scientific article; zbMATH DE number 5201482 (Why is no real title available?)
• Compositional synthesis of reactive controllers for multi-agent systems
• Synthesis of succinct systems
• A methodology of structured-modular composition programming
• Composition for component-based modeling
• Dependency-Based Compositional Synthesis
• scientific article; zbMATH DE number 1390331 (Why is no real title available?)
• Assume-guarantee synthesis for concurrent reactive programs with partial information
• scientific article; zbMATH DE number 2113972 (Why is no real title available?)
• Foundations of rule-based design of modular systems
• Information Flow Guided Synthesis
• ESM systems and the composition of their computations
• scientific article; zbMATH DE number 1955871 (Why is no real title available?)

Describes a project that uses

Uses Software

• BoSy

This page was built for publication: Compositional synthesis of modular systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2147209)