Synthesizing Robust Systems with RATSY

TL;DR

This paper extends the RATSY tool to synthesize robust reactive systems from GR(1) specifications, ensuring finite safety guarantee violations even when assumptions are temporarily violated.

Contribution

It introduces a method to synthesize robust systems by transforming specifications into Streett games and computing winning strategies for robustness.

Findings

Successfully extended RATSY for robustness synthesis.

Demonstrated the approach with experimental results.

Ensured finite safety violations under assumption violations.

Abstract

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.