Triggers for Reactive Synthesis Specifications
Abstract
Reactive synthesis is an automated procedure to obtain a
correct-by-construction reactive system from its temporal logic
specification. Two of the main challenges in bringing reactive
synthesis to practice are its very high worst-case complexity and
the difficulty of writing declarative specifications using basic
LTL operators. To address the first challenge, researchers have
suggested the GR(1) fragment of LTL, which has an efficient
polynomial time symbolic synthesis algorithm. To address the
second challenge, specification languages include higher-level
constructs that aim at allowing engineers to write succinct and
readable specifications. One such construct is the triggers
operator, as supported, e.g., in the Property Specification
Language (PSL).
In this work we introduce triggers into
specifications for reactive synthesis. The effectiveness of our
contribution relies on a novel encoding of regular expressions
using symbolic finite automata (SFA) and on a novel semantics for
triggers that, in contrast to PSL triggers, admits an efficient
translation into GR(1). We show that our triggers are expressive
and succinct, and prove that our encoding is optimal.
We have
implemented our ideas on top of the Spectra language and
synthesizer. We demonstrate the usefulness and effectiveness of
using triggers in specifications for synthesis, as well as the
challenges involved in using them, via a study of more than 300
triggers written by undergraduate students who participated in a
project class on writing specifications for synthesis.
To the best
of our knowledge, our work is the first to introduce triggers into
specifications for reactive synthesis.
Gal Amram, Dor Ma'ayan, Shahar Maoz, Or Pistiner, and Jan O. Ringert, Triggers for Reactive Synthesis Specifications. Proc. of ICSE 2023. To appear.