Gal Amram - Extensions of GR(1): efficient synthesis for meaningful specifications

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.