Symbolic repairs for GR(1) specifications
conference contributionposted on 2019-06-20, 08:41 authored by Shahar Maoz, Jan Oliver Ringert, Rafi Shalom
Unrealizability is a major challenge for GR(1), an expressive assume-guarantee fragment of LTL that enables efficient 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. In this work 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. We implemented our work, validated its correctness, and evaluated it on benchmarks from the literature. The evaluation shows the strength of our algorithms, in their ability to suggest repairs and in their performance and scalability compared to previous solutions.
This project has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No 638049, SYNTECH).
CitationProceedings of the 41st International Conference on Software Engineering, ICSE 2019, Montreal, QC, Canada, 2019, pp. 1016-1026
Author affiliation/Organisation/COLLEGE OF SCIENCE AND ENGINEERING/Department of Informatics
SourceICSE '19 Proceedings of the 41st International Conference on Software Engineering, Montreal, Quebec, Canada
- AM (Accepted Manuscript)