Reactive synthesis is an automated procedure to obtain a correct-by-construction reactive system from its temporal logic specification. GR(1) is an expressive assume-guarantee fragment of LTL that enables efficient synthesis and has been recently used in different contexts and application domains.
In this work we present just-in-time synthesis (JITS) for GR(1). Rather than constructing a controller at synthesis time, we compute next states during system execution, and only when they are required. We prove that JITS does not compromise the correctness of the synthesized system execution. We further show that the basic algorithm can be extended to enable several variants.
We have implemented JITS in the Spectra synthesizer. Our evaluation, comparing JITS to existing tools over known benchmark specifications, shows that JITS reduces (1) total synthesis time, (2) the size of the synthesis output, and (3) the loading time for system execution, all while having little to no effect on system execution performance.
Conference DayWed 23 SepDisplayed time zone: (UTC) Coordinated Universal Time change
09:10 - 10:10
|Just-In-Time Reactive Synthesis|
|FlashRegex: Deducing Anti-ReDoS Regexes from Examples|
Yeting LiInstitute of Software, Chinese Academy of Sciences; University of Chinese Academy of Sciences, Zhiwu XuShenzhen University, Jialun CaoDepartment of Computer Science and Engineering, The Hong Kong University of Science and Technology, Haiming ChenInstitute of Software, Chinese Academy of Sciences, Tingjian GeUniversity of Massachusetts, Lowell, Shing-Chi CheungHong Kong University of Science and Technology, China, Haoren ZhaoShaanxi Normal University, Xi'an, China