Controller Synthesis for Reactive Systems with Communication Delay by Formula Translation
The problem of automated reactive synthesis has been well studied by researchers. We consider a setting that is common in practice, wherein there is a communication delay between the (synthesized) controller and the (controlled) plant, such that symbols emitted by either component reach the other component after a delay. We address the problem of synthesizing a controller that can assure the given temporal property at the remote plant despite delay. We consider two variants of this setting, one where the delay is a constant over the entire trace, and the other where the delay could increase over time (upto an upper bound), and propose approaches for both these settings. We state and prove soundness and completeness results for both our approaches. We have implemented our approaches, and evaluated them on the standard SYNTCOMP 2022 suite of temporal properties. The results provide evidence for the robustness and practicality of our approaches.
Mon 27 OctDisplayed time zone: Chennai, Kolkata, Mumbai, New Delhi change
| 09:30 - 10:30 | |||
| 09:3030m Talk | Regular Theories and How to Decide Them NIER Umang Mathur National University of Singapore, Singapore | ||
| 10:0030m Talk | Controller Synthesis for Reactive Systems with Communication Delay by  Formula Translation NIER | ||
