Synthesizing Robust Systems with RATSY

Roderick Bloem
(IAIK, TU-Graz)
Hans-Jürgen Gamauf
(IAIK, TU-Graz)
Georg Hofferek
(IAIK, TU-Graz)
Bettina Könighofer
(IAIK, TU-Graz)
Robert Könighofer
(IAIK, TU-Graz)

Specifications for reactive systems often consist of environment assumptions and system guarantees. An implementation should not only be correct, but also robust in the sense that it behaves reasonably even when the assumptions are (temporarily) violated. We present an extension of the requirements analysis and synthesis tool RATSY that is able to synthesize robust systems from GR(1) specifications, i.e., system in which a finite number of safety assumption violations is guaranteed to induce only a finite number of safety guarantee violations. We show how the specification can be turned into a two-pair Streett game, and how a winning strategy corresponding to a correct and robust implementation can be computed. Finally, we provide some experimental results.

In Doron Peled and Sven Schewe: Proceedings First Workshop on Synthesis (SYNT 2012), Berkeley, California, USA, 7th and 8th July 2012, Electronic Proceedings in Theoretical Computer Science 84, pp. 47–53.
Published: 3rd July 2012.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: