Prefer a chat interface with context about you and your work?
Synthesizing a Lego Forklift Controller in GR(1): A Case Study
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 (LTL) where synthesis is possible using a polynomial symbolic algorithm. We conducted a case study to learn about the challenges that software engineers may face …