GR(1) is a popular and applicative fragment of Linear Temporal Logic (LTL) for which a feasible reactive synthesis algorithm exists. In this talk, I will present some of my recent works that introduce extensions for GR(1). Specifically, I will speak about the addition of regular expressions and triggers, energy constraints, and existential guarantees to GR(1). We support the first two extensions by a reduction to GR(1), and I will present efficient and concise encodings thereof. In contrast, the third extension, termed GR(1)*, strictly adds expressive power to GR(1), and thus requires a novel synthesis technique. However, the synthesis technique we propose for GR(1)* formulas preserves the quadratic time complexity of GR(1) synthesis. All extensions are implemented in the Spectra language and synthesis environment. These are joint works with Shahar Maoz, Or Pistiner, and Jan Oliver Ringert.
Gal has completed in 2018 his Ph.D. in Computer Science at the Ben-Gurion University, continued to a postdoc in the Technion, hosted by Yoram Moses, in 2017-2018, and from 2018 he does a postdoc with Shahar Maoz at the Tel Aviv University.