Performance Heuristics for GR(1) Synthesis and Related Algorithms
arXiv:1712.01103 · doi:10.4204/EPTCS.260.7
Abstract
Reactive synthesis for the GR(1) fragment of LTL has been implemented and studied in many works. In this workshop paper we present and evaluate a list of heuristics to potentially reduce running times for GR(1) synthesis and related algorithms. The list includes early detection of fixed-points and unrealizability, fixed-point recycling, and heuristics for unrealizable core computations. We evaluate the presented heuristics on SYNTECH15, a total of 78 specifications of 6 autonomous Lego robots, written by 3rd year undergraduate computer science students in a project class we have taught, as well as on several benchmarks from the literature. The evaluation investigates not only the potential of the suggested heuristics to improve computation times, but also the difference between existing benchmarks and the robot's specifications in terms of the effectiveness of the heuristics.
arXiv commentIn Proceedings SYNT 2017, arXiv:1711.10224
References in corpus (9)
- Synthesizing a Lego Forklift Controller in GR(1): A Case Study
- The First Reactive Synthesis Competition (SYNTCOMP 2014)
- Developing a Practical Reactive Synthesis Tool: Experience and Lessons Learned
- The Second Reactive Synthesis Competition (SYNTCOMP 2015)
- A multi-paradigm language for reactive synthesis
- The 3rd Reactive Synthesis Competition (SYNTCOMP 2016): Benchmarks, Participants & Results
- Symbolic BDD and ADD Algorithms for Energy Games
- Proceedings Fifth Workshop on Synthesis
- Proceedings Fourth Workshop on Synthesis