SyntechX: The Benchmark for Evaluating GR(1) Incremental Reactive Synthesis Methods
Abstract
SyntechX is the first benchmark produced to evaluate GR(1) Incremental Reactive Synthesis algorithms. It was introduced in the paper "IncreGR1: An Incremental Reactive Synthesis Framework for GR(1) Formulae". The default subset is collected from SYNTECH (covering 15, 17, 19, 20, and 21), AMBA, GenBuf, etc, all of which have gained widespread recognition in assessing the efficacy of reactive synthesis methods. Subsequently, we considered seven types of modifications to the existing benchmark, which cover all possible modifications, and implemented these modifications using LLMs. All specifications follow the Spectra language and are written in *.spectra files in text format.
Fields of Study & Subjects
Formal Methods in Verification
Embedded Systems Design Techniques
semigroups and automata theory
Publication details
- Journal / source
- Zenodo (CERN European Organization for Nuclear Research)
- Publication date
- 4 March 2026
- Language
- EN
- Document type
- Dataset