Compositional synthesis of modular systems

DOI10.1007/978-3-030-88885-5_20zbMATH Open1497.68300arXiv2106.14783OpenAlexW3178776999MaRDI QIDQ2147209FDOQ2147209

Bernd Finkbeiner, Noemi Passing

Publication date: 22 June 2022

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.

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

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

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)

Cites Work

• Bounded Synthesis
• Safraless Compositional Synthesis
• Encodings of Bounded Synthesis
• Compositional Algorithms for LTL Synthesis
• Assume-admissible synthesis
• Assume-Guarantee Synthesis
• Pattern-Based Refinement of Assume-Guarantee Specifications in Reactive Synthesis
• On the structure of non-manipulable equilibria
• Assume-Guarantee Synthesis for Concurrent Reactive Programs with Partial Information
• Testing language containment for \(\omega\)-automata using BDDs

Cited In (11)

• Title not available (Why is that?)
• Synthesis of succinct systems
• Dependency-Based Compositional Synthesis
• A methodology of structured-modular composition programming
• Composition for component-based modeling
• Title not available (Why is that?)
• Title not available (Why is that?)
• Foundations of rule-based design of modular systems
• Information Flow Guided Synthesis
• ESM systems and the composition of their computations
• Title not available (Why is that?)

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)