Infinite-state games provide a framework for the synthesis of reactive systems with unbounded data domains. Solving such games typically relies on computing symbolic fixpoints, particularly symbolic attractors. However, these computations may not terminate, and while recent acceleration techniques have been proposed to address this issue, they often rely on acceleration arguments of limited expressiveness. In this work, we propose an approach for the modular computation of acceleration arguments. It enables the construction of complex acceleration arguments by composing simpler ones, thereby improving both scalability and flexibility. In addition, we introduce a summarization technique that generalizes discovered acceleration arguments, allowing them to be efficiently reused across multiple contexts. Together, these contributions improve the efficiency of solving infinite-state games in reactive synthesis, as demonstrated by our experimental evaluation.

翻译：无限状态博弈为具有无界数据域的反应式系统综合提供了理论框架。求解此类博弈通常依赖于计算符号不动点，特别是符号吸引子。然而，这些计算可能无法终止，尽管近期已提出加速技术以解决此问题，但这些技术往往依赖于表达能力有限的加速论证。本文提出一种模块化计算加速论证的方法。该方法通过组合更简单的加速论证来构建复杂的加速论证，从而同时提升可扩展性与灵活性。此外，我们引入了一种概括化技术，能够对已发现的加速论证进行泛化，使其能够在多种上下文中高效复用。实验评估表明，这些贡献共同提升了在反应式综合中求解无限状态博弈的效率。