Efficient Incremental GR(1) Synthesis via Monotonic Fixed-Point Reuse

Although reactive synthesis guarantees correct-by-construction implementations, its practical adoption is limited by a performance bottleneck in the iterative design-and-refinement cycle of formal specifications. GR(1) synthesizers perform redundant, from-scratch computations for each specification modification, severely slowing the development workflow. To address this inefficiency, we propose an incremental synthesis method that exploits the monotonicity of the underlying fixed-point computations. By reusing the system winning region from the preceding check, our method significantly accelerates realizability check. Our work applies an incremental method to iterative GR(1) specification development covering the full GR(1) scope, including system guarantees and environment assumptions, to accelerate realizability checking. Furthermore, we introduce two heuristics for early fixed-point detection during incremental realizability checking. Finally, we analyze why prior work failed to integrate an incremental technique limited to system guarantees into the unrealizable core minimization algorithm DDMin , further establishing iterative development as a suitable application setting for incremental methods. Evaluated on a large-scale benchmark of 8,282 specifications, our method exhibits a strong positive correlation between performance gain and specification complexity. For the most challenging specifications, which constitute the primary bottlenecks in development, our approach achieves speedups of several orders of magnitude, reducing computation times in some cases from nearly an hour to just seconds.