Assume-guarantee synthesis for concurrent reactive programs with partial information

DOI10.1007/978-3-662-46681-0_50MaRDI QIDQ5194960zbMATH OpenOpenAlexFDO

Authors Roderick Bloem, Krishnendu Chatterjee, Swen Jacobs, Robert Könighofer

Publication date 17 September 2019

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

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

zbMATH Keywords

critical sectiongraph gamepartial informationperfect informationtree automaton

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: Synthesis of program parts is very useful for concurrent systems. However, most synthesis approaches do not support common design tasks, like modifying a single process without having to re-synthesize or verify the whole system. Assume-guarantee synthesis (AGS) provides robustness against modifications of system parts, but thus far has been limited to the perfect information setting. This means that local variables cannot be hidden from other processes, which renders synthesis results cumbersome or even impossible to realize. We resolve this shortcoming by defining AGS in a partial information setting. We analyze the complexity and decidability in different settings, showing that the problem has a high worst-case complexity and is undecidable in many interesting cases. Based on these observations, we present a pragmatic algorithm based on bounded synthesis, and demonstrate its practical applicability on several examples.

Recommendations

• scientific article; zbMATH DE number 1444727
• Church's Problem Revisited
• Assume-Guarantee Synthesis
• Compositional synthesis of modular systems
• Synthesizing reactive programs

Cited in

(6)

• Distributed synthesis for parameterized temporal logics
• Compositional synthesis of modular systems
• scientific article; zbMATH DE number 6774232 (Why is no real title available?)
• Security-aware synthesis using delayed-action games
• Information Flow Guided Synthesis
• Contract-based distributed logical controller synthesis

This page was built for publication: Assume-guarantee synthesis for concurrent reactive programs with partial information

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