Synthesizing a Lego Forklift Controller in GR(1)

A Case Study

Abstract

Reactive synthesis is an automated procedure to obtain a correct-by-construction reactive system from a given specification. GR(1) is a well-known fragment of linear temporal logic where synthesis is possible using a polynomial symbolic algorithm. We conducted a case study to learn about chal- lenges of GR(1) synthesis by software engineers for the development of a reactive robotic system. In the case study we developed two variants 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, an examination of two specification variants for execution scheduling, tracing from the synthesized controller to constraints in the specification, and generated counter strategies to support understand- ing reasons for unrealizability. We present the specifications we developed, our observations, and challenges faced during the case study.

S. Maoz and J. O. Ringert, Synthesizing a Lego Forklift Controller in GR(1): A Case Study. In SYNT 2015. Pages 58-72. 2015

Supporting materials