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 software engineering practice are its very high worst-case complexity -- for linear temporal logics (LTL) it is double exponential in the length of the formula, and the difficulty of writing declarative specifications using basic LTL operators. To address the first challenge, Piterman et al. have suggested the General Reactivity of Rank 1 (GR(1)) fragment of LTL, which has an efficient polynomial time symbolic synthesis algorithm. To address the second challenge, Dwyer et al. have identified 55 LTL specification patterns, which are common in industrial specifications and make writing specifications easier.
In this work we show that almost all of the 55 LTL specification patterns identified by Dwyer et al. can be expressed in the GR(1) fragment of LTL. Specifically, we present an automated, sound and complete translation of the patterns to the GR(1) form, which effectively results in an efficient reactive synthesis procedure for any specification that is written using the patterns.
We have validated the correctness of the catalog of GR(1) templates we have created. The work is implemented in our reactive synthesis environment. It provides positive, promising evidence, for the potential feasibility of using reactive synthesis in practice.
- Catalog of patterns and GR(1) templates
- Archive with GR(1) templates for
- 52 supported LTL specification patterns
- 41 supported negated LTL specification patterns
- Archive with verification code for correctness of GR(1) templates
- verification code generated for NuSMV
- verification results included in archive
- Archive with DBW2GR1 and complete toolchain (submitted for artifact evaluation)
- translation from LTL to automata
- scripts and example usages
- DBW2GR1 tool to translate minimized automata to GR(1) fragment