一句话：提出 best-effort GR(1) 合成，在不可实现规约下利用环境合作并量化不可实现程度。
GR(1) 合成广泛使用，但大量规约不可实现，传统工具仅报告失败。本文提出 best-effort GR(1) 合成，利用环境常受自身目标驱动而非纯对抗，要求系统策略满足 best-effort extensibility 并保持环境假设可满足。对不可实现但 well-separated 的规约，构造 3 嵌套 µ-演算不动点公式刻画 best-effort 获胜区域，证明 soundness 与 completeness；算法需 O(n|Q|) 次符号后继计算，优于标准 GR(1) 的 O(mn|Q|^2)。文章还通过有限合作可达性分层分类依赖环境合作的程度，量化不可实现性。作者在 Spectra 中实现检查、控制器构造与分类，并在 SYNTECH、AMBA、GenBuf 语料上评估，发现 best-effort 可实现性常见，所有顶层不可实现类别均出现。
Reactive synthesis automatically derives correct-by-construction controllers from temporal logic specifications. GR(1) synthesis is widely adopted due to its polynomial-time complexity and practical expressiveness. In practice, however, a significant proportion of GR(1) specifications are unrealizable. Conventional synthesis tools report failure in such cases, yet real-world environments are often governed by their own objectives rather than purely adversarial behavior, presenting opportunities for the system to leverage environmental cooperation toward satisfying its justice guarantees. For unrealizable GR(1) specifications, this paper proposes best-effort GR(1) synthesis. The approach requires the system strategy to satisfy two properties: best-effort extensibility, which preserves at every state reached by the play the possibility of satisfying all system justice guarantees, and persistent satisfiability of environment assumptions, which ensures that environmental cooperation does not preclude the environment from satisfying its own justice assumptions. For unrealizable but well-separated specifications, we construct a 3-nested µ-calculus fixpoint formula that characterizes the best-effort system winning region and prove its soundness and completeness. The resulting algorithm performs O(n|Q|) symbolic next-state computations, compared with O(mn|Q|2) for standard GR(1) synthesis. We further analyze the relationship between the best-effort and standard GR(1) winning regions through finite cooperative reachability, yielding a hierarchical classification of dependence on environmental cooperation at the region and initial-state levels for well-separated but unrealizable specifications, thereby quantifying the degree of unrealizability. We implement best-effort checking, controller construction, and classification in the Spectra GR(1) synthesizer and evaluate the approach on a diversified corpus of SYNTECH, AMBA, and GenBuf specifications. Experimental results demonstrate that best-effort realizability is common among well-separated but unrealizable specifications and that all top-level unrealizability categories occur in the combined benchmark corpus.