Projects per year
Abstract
A modern approach to engineering correct-by-construction systems is to synthesize them automatically from formal specifications. Oftentimes, a system can only satisfy its guarantees if certain environment assumptions hold, which motivates their inclusion in the system specification. Experience with modern synthesis approaches shows that synthesized systems tend to satisfy their specifications by actively working towards the violation of the assumptions rather than satisfying assumptions and guarantees together. Such uncooperative behavior is undesirable because it violates the aim of synthesis: the system should try to satisfy its guarantees and use the assumptions only when needed. Also, the assumptions often describe the valid behavior of other components in a bigger system, which should not be obstructed unnecessarily.
In this paper, we present a hierarchy of cooperation levels between system and environment. Each level describes how well the system enforces both the assumptions and guarantees. We show how to synthesize systems that achieve the highest possible cooperation level for a given specification in Linear Temporal Logic (LTL). The synthesized systems can also exploit cooperative environment behavior during operation to reach a higher cooperation level that is not enforceable by the system initially. The worst-case time complexity of our synthesis procedure is doubly-exponential, which matches the complexity of standard LTL synthesis
In this paper, we present a hierarchy of cooperation levels between system and environment. Each level describes how well the system enforces both the assumptions and guarantees. We show how to synthesize systems that achieve the highest possible cooperation level for a given specification in Linear Temporal Logic (LTL). The synthesized systems can also exploit cooperative environment behavior during operation to reach a higher cooperation level that is not enforceable by the system initially. The worst-case time complexity of our synthesis procedure is doubly-exponential, which matches the complexity of standard LTL synthesis
Original language | English |
---|---|
Title of host publication | Automated Technology for Verification and Analysis (ATVA'15) |
Place of Publication | Berlin-Heidelberg |
Publisher | Springer |
Pages | 394-410 |
ISBN (Print) | 978-3-319-24952-0 |
DOIs | |
Publication status | Published - 2015 |
Event | International Symposium on Automated Technology for Verification and Analysis - Shanghai, China Duration: 12 Oct 2015 → 15 Oct 2015 |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Publisher | Springer |
Volume | 9364 |
Conference
Conference | International Symposium on Automated Technology for Verification and Analysis |
---|---|
Country/Territory | China |
City | Shanghai |
Period | 12/10/15 → 15/10/15 |
Fields of Expertise
- Information, Communication & Computing
Treatment code (Nähere Zuordnung)
- Theoretical
Fingerprint
Dive into the research topics of 'Cooperative Reactive Synthesis'. Together they form a unique fingerprint.Projects
- 4 Finished
-
EU - IMMORTAL - IMMORTAL – Integrated Modelling, Fault Management, Verification and Reliable Design Environment for Cyber-Physical Systems
Bloem, R. & Könighofer, R.
1/03/15 → 28/02/18
Project: Research project
-
EU - STANCE - A Source code analysis Toolbox for software security AssuraNCE
Tögl, R., Könighofer, R. & Bloem, R.
1/10/12 → 30/09/15
Project: Research project
-
RiSE - Rigorous Systems Engineering
Könighofer, R., Khalimov, A., Bloem, R., Könighofer, B. & Jacobs, S.
1/03/11 → 31/08/19
Project: Research project