Performance Heuristics for GR(1) Unrealizable Core Computation

Abstract A major challenge of reactive synthesis, an automated process for deriving correct-by-construction reactive systems from temporal specifications, is debugging unrealizable specifications. One way to debug them in the context of GR(1), an LTL fragment that balances efficient synthesis complexity and expressiveness, is the computation of unrealizable cores. Although work has been done to accelerate core computation, it remains a costly operation, despite being commonly used during specification development. In this paper, we first examine a version of the existing core computation algorithm, where we replace the classic algorithm with , a state-of-the-art domain-agnostic minimization algorithm. Then, we present two novel GR(1)-specific heuristics to improve the core computation time by exploiting attributes of the realizability checking algorithm. These heuristics include (1) quickly discarding unneeded justice guarantees, and (2) reusing realizability check results to make subsequent checks faster. We implemented our work on top of the Spectra language and synthesizer and evaluated it over hundreds of specifications. Our evaluation shows that while using CDD in our context was ineffective, the new heuristics improve core computation times for 80% of the specifications, with an average improvement of more than three times compared to the baseline algorithm.