Performance heuristics for GR(1) synthesis and related algorithms

Area of Science:

• Formal methods in computer science
• Automated synthesis of reactive systems

Background:

• Reactive synthesis for the Linear Temporal Logic (LTL) GR(1) fragment is a well-researched area.
• Existing algorithms face challenges with scalability and running times for complex specifications.

Purpose of the Study:

• To present and evaluate a novel list of heuristics aimed at reducing computation times for GR(1) synthesis.
• To integrate these heuristics into the Spectra Tools synthesis environment.
• To assess the effectiveness of these heuristics on diverse benchmarks, including student-generated robot specifications.

Main Methods:

• Implementation of heuristics for controlled predecessor computation, BDDs, early fixed-point detection, fixed-point recycling, and unrealizable core computations.
• Integration into the Spectra Tools software.
• Empirical evaluation on SYNTECH15, SYNTECH17 robot specifications, and literature benchmarks.
• Comparative analysis against existing tools (RATSY, Slugs).

Main Results:

• All implemented heuristics, when applied together, demonstrate positive results in reducing GR(1) synthesis running times.
• Heuristic effectiveness varies across different specification sets.
• Spectra Tools, incorporating these heuristics, outperforms RATSY and Slugs on most benchmarks, with performance gains increasing for larger specifications.

Conclusions:

• The proposed heuristics offer a significant improvement for GR(1) synthesis and related algorithms.
• Spectra Tools provides a competitive and scalable solution for reactive synthesis.
• The findings highlight the importance of tailored heuristics for optimizing automated synthesis tools.