TY - JOUR
T1 - Specifiable robustness in reactive synthesis
AU - Bloem, Roderick
AU - Chockler, Hana
AU - Ebrahimi, Masoud
AU - Strichman, Ofer
N1 - Funding Information:
This work was supported by the Austrian Research Promotion Agency (FFG) through Project TRUSTED (867558) and the Graz University of Technology’s LEAD project “Dependable Internet of Things in Adverse Environments”. It was also partially supported by the Coleman-Cohen Foundation, by the Royal Society grant IES\R2\170021, the UKRI Trust-worthy Autonomous Systems Hub (EP/V00784X/1) the UKRI Strategic Priorities Fund to the UKRI Research Node on Trustworthy Autonomous Systems Governance and Regulation (EP/V026607/1), and by the European Union (IMMORTAL, Grant 644905), and by the ECSEL Joint Undertaking (ENABLE-S3, Grant 692455).
Publisher Copyright:
© 2023, The Author(s).
PY - 2023/3/23
Y1 - 2023/3/23
N2 - 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
AB - 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
UR - http://www.scopus.com/inward/record.url?scp=85150620040&partnerID=8YFLogxK
U2 - 10.1007/s10703-023-00418-x
DO - 10.1007/s10703-023-00418-x
M3 - Article
SN - 0925-9856
VL - 60
SP - 259
EP - 276
JO - FORMAL METHODS IN SYSTEM DESIGN
JF - FORMAL METHODS IN SYSTEM DESIGN
IS - 2
ER -