Specifiable robustness in reactive synthesis

Roderick Bloem, Hana Chockler, Masoud Ebrahimi, Ofer Strichman

Research output: Contribution to journalArticlepeer-review

21 Downloads (Pure)

Abstract

When synthesizing a system from a given specification, there is room for automatically adding various requirements, hence improving the resulting system. One such requirement covered extensively in past literature is that of robustness. In particular, the system can fail to read the inputs correctly from the environment, and the environment can fail to satisfy our assumptions about its behavior. Nevertheless, we want the system to still satisfy the specification even under these failures, in some limited way. It has to be limited because it is typically too strong of a requirement to realize the property regardless of the inputs and the environment’s assumptions. In this work, we propose a simple and flexible frame‑work for synthesizing robust systems, where the user defines the required robustness via a temporal robustness specification. For example, the user may specify that the environment is eventually reliable, or input misreadings cannot occur more than k consecutive steps and synthesize a system under this assumption. Furthermore, our framework enables us to specify a temporal recovery specification, which describes how the designer expects the system to recover after a failure of the environment assumptions. We show examples of robust systems that we synthesized with this method using our synthesis tool Party
Original languageEnglish
Pages (from-to)259-276
Number of pages18
JournalFORMAL METHODS IN SYSTEM DESIGN
Volume60
Issue number2
DOIs
Publication statusPublished - 23 Mar 2023

Fingerprint

Dive into the research topics of 'Specifiable robustness in reactive synthesis'. Together they form a unique fingerprint.

Cite this