  This paper considers the problem of assumptions refinement in the context of
unrealizable specifications for reactive systems. We propose a new
counterstrategy-guided synthesis approach for GR(1) specifications based on
Craig's interpolants. Our interpolation-based method identifies causes for
unrealizability and computes assumptions that directly target unrealizable
cores, without the need for user input. Thereby, we discuss how this property
reduces the maximum number of steps needed to converge to realizability
compared with other techniques. We describe properties of interpolants that
yield helpful GR(1) assumptions and prove the soundness of the results.
Finally, we demonstrate that our approach yields weaker assumptions than
baseline techniques, and finds solutions in case studies that are unsolvable
via existing techniques.
