Synthesizing Reactive Systems Using Robustness and Recovery Specifications
Explore the challenges and solutions in synthesizing reactive systems by focusing on robustness and recovery specifications. Learn about the problem statements, existing research work, and definitions related to robustness in dealing with hidden inputs and assumption violations.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.
E N D
Presentation Transcript
Synthesizing Reactive Systems Using Robustness and Recovery Specifications Roderick Bloem, Hana Chockler, Masoud Ebrahimi, Ofer Strichman, Graz University of Technology King s College London Graz University of Technology Technion, Haifa FMCAD 19
The reactive synthesis problem Synthesize a system ? such that Environment spec System spec ? ???? ???? Problem: the specification is not tight . There is room for defining what is a good system , in the space of valid systems. Spec We will synthesize according to a different formula, ? . We need to guarantee soundness : ? (???? ????) 2
This problem has been addressed before Some examples: A small system A non-vacuous system A robust system Ehlers, Konighofer, Hofferek, FMCAD 12 Bloem, Chockler. Ebrahimi, Strichman, VMCAI 17 Bloem, Gamauf, Hofferek, Konighofer, Konighofer, SYNT 12, Ehlers, NFM 11, Also related: Tabuada, Balkan, Majumdar, EMSOFT 12, Topcu, Ozay, Liu, Murray, HSCC 12 3
Robustness Robustness measures the degree to which a system can function correctly in the presence of erroneous input or stressful environmental conditions ISO/IEC/IEEE International Standard Outputs Inputs Environment System We focus on robustness against two types of problems: Hidden inputs - ? fails to read (some of) the environment s signals 2. The environment does not satisfy the assumption ???? 1. 4
Various robustness definitions Hidden inputs ? should satisfy ??even if... 1. some of the inputs are hidden in a finite number of steps. 2. some of the inputs are hidden for ? time-steps consecutively. 3. some / all of the inputs are hidden occasionally. 5
Various robustness definitions Assumption violation ? should satisfy ????even if... 1. ...there is a finite number of violations of the assumption ???? 2. ...there are ? consecutive violations of the assumption ???? Note: with these definitions ????,????should be invariants i.e., ?? for a propositional ?. Our interpretation: ? is violated in a finite number of steps. 6
Various robustness definitions Assumption violation 3. ? satisfies its liveness guarantees, even if ????is violated infinitely often [Bloem, Gamauf, Hofferek, Konighofer, Konighofer, SYNT 12] 4. ? eventually returns to satisfy ????after a finite number of violations of the safety assumptions [Ehlers, NFM 11; Tabuada, Balkan, Majumdar, EMSOFT 12] Note: definition 4 includes a recovery specification 7
Contributions Prior work: For a given definition of robustness, tailors a synthesis algorithm. Bloem, Gamauf, Hofferek, Konighofer, Konighofer, SYNT 12: a tailored game graph Ehlers, NFM 11: A game based on a generalized Rabin automata This work: For a given definition of robustness, reduces it to normal synthesis. It takes as input a robustness LTL specification ????, a recovery LTL specification ???? ... and reduces the robust synthesis problem to a normal synthesis problem. 8
Synthesis with a robustness specification: Hidden Inputs An auxiliary synchronization bit ??: are the inputs visible in the current step ? Examples of robustness specifications: ????(??) Robustness specification ?? ?? Inputs are hidden for a finite number of steps Inputs are hidden for up to ? consecutive steps ?(?? (? ?? ????)) Inputs are hidden infinitely often ??(??) ?((??1= ??2) ??) We trust the inputs only if they are equal 9
Synthesis with a robustness specification: Hidden Inputs ? original inputs, ? - additional copy of ? (for simplicity, here there is no assumption) Instead of synthesizing ? ? ? ????(?,?) M ? We synthesize: yes ? = ? ?,? ,?? ?? ? ? ? ? ????(? ,?) M ?? satisfies ???? no 10
Synthesis with a robustness specification: Hidden Inputs ? original inputs, ? - additional copy of ? Synthesize: ?????? ? ?? ? = ? ????(? ,?) ?????,? (6) ?,? are equal when ?? is up Robustness specification Guarantees over ? ? ,?? are invisible to the system. Synthesis with incomplete information [Kupferman Vardi, 1997] 11
Synthesis with a robustness specification: Hidden Inputs ? original inputs, ? - additional copy of ? Synthesize: ?????? ? ?? ? = ? ????(? ,?) ?????,? (6) Problem: not necessarily sound. 12
Synthesis with a robustness specification: Hidden Inputs So what can be done ? We can try to enforce soundness by synthesizing ?????? ? ?? ? = ? ????(? ,?) (?????,? ?????,? ) ?????,? Not necessarily realizable We can just check if ? ????(?,?) ?????,? In the article we show a sufficient condition ( monotonicity ) for this relation to hold. 13
Synthesis with a robustness specification: Assumption violation We want to synthesize ? such that ? ????? ????? ????,????are propositional But we want to add a robustness spec, e.g., ? should satisfy ????even when the environment violates ????a finite # of times . An auxiliary synchronization bit ??: When true, the environment satisfies ????in the current step. Synthesize with: ? (?????? ? ?? ????) ????? (16) Here soundness is guaranteed 14
Synthesis with a robustness specification: Assumption violation But we want to add a robustness spec, e.g., ? should satisfy ????even when the environment violates ????a finite # of times . ???? ? ?? ???? ????? Synthesize with: ? (?????? ? ?? ????) ????? (16) 15
Synthesis with a robustness specification: Assumption violation Synthesize with: ? (?????? ? ?? ????) ????? (16) and now with a different robustness condition ? should satisfy ????only after a certain condition is met Example: Trust the inputs only after a password was given : ????= ??? ?? ? (??? ? ?? ) 16
Assume ? ?1 ?2 Guarantee ?( ?1 ?1 (?2 ?2) Example First, without a robustness spec: Sink state Assumption violated 17
Assume ? ?1 ?2 Guarantee ?( ?1 ?1 (?2 ?2) Example Now, add our robustness spec: Trust the inputs only after a password was given (pwd = ?1?2) : pwd Sink state Assumption violated Assumption violated 18
Recovery specification We can use a synchronization bit for supporting a recovery spec, e.g., The system can fault up to ? steps after the environment fails (i.e., ????) . Introduce a new synchronization bit ?? ????(????,?? ) = G G(???? ?1???? ?k???? ?k?? ) Synthesize ? ????????,?? G G (?? ????) Note: soundness depends on the choice of ????. 19
Conclusions A typical specification is not tight . Many systems can satisfy it. We can add additional default constraints , e.g., robustness, recovery, non- vacuousness, etc... In contrast to previous works, which suggested tailored synthesis algorithms... Here we showed that it can all be reduced to normal synthesis. The method is parameterized with LTL robustness and recovery specifications. We implemented this method in PARTY with bounded synthesis* * Finkbeiner, B., Schewe, 2012 22
