Title: Symbolic Repairs for GR(1) Specifications
Speaker: Jan Oliver Ringert, Lecturer in Model-Based Software Development in the Department of Informatics at the University of Leicester
Abstract: Reactive synthesis is an automated procedure to obtain a correct-by-construction reactive system from a given specification. Examples include GR(1), an expressive assume-guarantee fragment of LTL, that enables efficient synthesis of the software controllers of robotic systems.
Unrealizability is a major challenge for synthesis. Some works attempt to help engineers deal with unrealizability by generating counter-strategies or computing an unrealizable core. Other works propose to repair the unrealizable specification by suggesting repairs in the form of automatically generated assumptions.
We present two novel symbolic algorithms for repairing unrealizable GR(1) specifications. The first algorithm infers new assumptions based on the recently introduced JVTS. The second algorithm infers new assumptions directly from the specification. Both algorithms are sound. The first is incomplete but can be used to suggest many different repairs. The second is complete but suggests a single repair. Both are symbolic and therefore efficient.
Joint work with Shahar Maoz and Rafi Shalom within the ERC StG SYNTECH project that addresses challenges related 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. http://smlab.cs.tau.ac.il/syntech/
Biography: Jan Oliver Ringert joined the Department of Informatics of the University of Leicester, Leicester, UK in February 2018 as a Lecturer in Model-Based Software Development. Previously, he was a PostDoc in the Software Modeling group of Shahar Maoz at the School of Computer Science, Tel Aviv University, Israel (12/2013-01/2018). Before, he worked in the Software Engineering group of Bernhard Rumpe at RWTH Aachen University, Germany (10/2008-11/2013). He received his Computer Science diploma (Dipl.-Inform.) from TU Braunschweig, Germany (2003-2008).
His research interests include model-based software engineering with a focus on software evolution and the software engineering aspects of synthesis of reactive systems.