King's College London

Research portal

Synthesizing reactive systems using robustness and recovery specifications

Research output: Chapter in Book/Report/Conference proceedingConference paper

Roderick Bloem, Hana Chockler, Masoud Ebrahimi, Ofer Strichman

Original languageEnglish
Title of host publicationProceedings of the 19th Conference on Formal Methods in Computer-Aided Design, FMCAD 2019
EditorsClark Barrett, Jin Yang
PublisherInstitute of Electrical and Electronics Engineers Inc.
Number of pages5
ISBN (Electronic)9780983567899
Publication statusPublished - 1 Oct 2019
Event19th Conference on Formal Methods in Computer-Aided Design, FMCAD 2019 - San Jose, United States
Duration: 22 Oct 201925 Oct 2019


Conference19th Conference on Formal Methods in Computer-Aided Design, FMCAD 2019
CountryUnited States
CitySan Jose

King's Authors


Past literature on synthesis identified the need to synthesize systems that are robust to failures of the system in reading the inputs from the environment, and also to failures of the environment itself to satisfy our assumptions about its behavior. In this work, we propose a simple and flexible framework 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, also, a temporal recovery specification, i.e., describing the way the system is expected to recover after a failure of the environment assumptions. We show examples of robust systems that we have synthesized with this method by our synthesis tool PARTY.

View graph of relations

© 2018 King's College London | Strand | London WC2R 2LS | England | United Kingdom | Tel +44 (0)20 7836 5454