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 provides a fundamental explanation for the failure of prior incremental approaches in the unrealizable core minimization algorithm \texttt{DDMin}, and successfully leverages this insight to accelerate iterative development, where specification changes are typically localized. We extend incremental analysis to the full GR(1) specification scope, encompassing both system guarantees and environment assumptions, and introduce two novel heuristics for early fixed-point detection.

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.