  One of the main challenges of reactive synthesis, an automated procedure to
obtain a correct-by-construction reactive system, is to deal with unrealizable
specifications. One means to deal with unrealizability, in the context of
GR(1), an expressive assume-guarantee fragment of LTL that enables efficient
synthesis, is the computation of an unrealizable core, which can be viewed as a
fault-localization approach. Existing solutions, however, are computationally
costly, are limited to computing a single core, and do not correctly support
specifications with constructs beyond pure GR(1) elements.
  In this work we address these limitations. First, we present QuickCore, a
novel algorithm that accelerates unrealizable core computations by relying on
the monotonicity of unrealizability, on an incremental computation, and on
additional properties of GR(1) specifications. Second, we present Punch, a
novel algorithm to efficiently compute all unrealizable cores of a
specification. Finally, we present means to correctly handle specifications
that include higher-level constructs beyond pure GR(1) elements.
  We implemented our ideas on top of Spectra, an open-source language and
synthesis environment. Our evaluation over benchmarks from the literature shows
that QuickCore is in most cases faster than previous algorithms, and that its
relative advantage grows with scale. Moreover, we found that most
specifications include more than one core, and that Punch finds all the cores
significantly faster than a competing naive algorithm.
