Projects per year
Abstract
Synthesis of program parts is particularly useful for concurrent systems. However, most 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 under partial information. 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.
Original language | English |
---|---|
Title of host publication | Tools and Algorithms for the Construction and Analysis of Systems (TACAS) - 21st International Conference |
Place of Publication | Berlin Heidelberg |
Publisher | Springer |
Pages | 517-532 |
ISBN (Print) | 978-3-662-46680-3 |
DOIs | |
Publication status | Published - 2015 |
Event | 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems: TACAS 2015 - London, United Kingdom Duration: 13 Apr 2015 → 17 Apr 2015 |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Publisher | Springer |
Volume | 9035 |
Conference
Conference | 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems |
---|---|
Abbreviated title | TACAS 2015 |
Country/Territory | United Kingdom |
City | London |
Period | 13/04/15 → 17/04/15 |
Fields of Expertise
- Information, Communication & Computing
Treatment code (Nähere Zuordnung)
- Application
- Theoretical
Fingerprint
Dive into the research topics of 'Assume-Guarantee Synthesis for Concurrent Reactive Programs with Partial Information'. Together they form a unique fingerprint.Projects
- 3 Finished
-
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
-
FWF - 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
-
Formal Methods for Design & Verification
Jacobs, S., Bloem, R., Könighofer, R., Könighofer, B., Khalimov, A., Hofferek, G. & Braud-Santoni, N.
1/02/08 → 15/07/19
Project: Research area