Speaker: Jan Oliver Ringert

Title: On Challenges in Reactive Synthesis for Software Engineers: Support
for LTL Specification Patterns and a Case Study

Abstract
Reactive synthesis is an automated procedure to obtain a
correct-by-construction reactive system from a given specification.
Despite recent advancements on the theory and algorithms of reactive
synthesis, many challenges remain in bringing reactive synthesis
technologies to the hands of software engineers.

GR(1) is a well-known fragment of linear temporal logic introduced by
Piterman et al. where synthesis is possible using a polynomial
symbolic algorithm.   One challenge in making the GR(1) fragment
useful for software engineers is its restricted syntax.  Further
challenges relate to the change from writing code to writing
specifications, and the development of tools to support a
specification-centric rather than a code-centric development process.

We report on our work in progress to investigate whether the
well-known high-level specification patterns identified by Dwyer et
al., which are common in industrial specifications and make writing
specifications easier, can be supported in GR(1) synthesis.
Specifically, we show that 52 out of the 55 patterns of Dwyer et al.
can be supported, and present an automated, sound and complete
translation of supported patterns to the GR(1) form, which effectively
results in a catalogue and an efficient reactive synthesis procedure
for any specification that is written using the patterns.

Next, we report on a case study we have conducted to learn about the
challenges of using GR(1) synthesis in the development of a reactive
robotic system. In the case study we developed a specification of a
forklift controller, deployed on a Lego robot. The case study employs
LTL specification patterns as an extension of the GR(1) specification
language and an examination of two specification variants for
execution scheduling. We present the specifications we developed, our
observations, and challenges faced during the case study.

Joint work with Shahar Maoz.  Supported by ERC StG SYNTECH.