Recently, several algorithms have been proposed for decomposing reactive synthesis specifications into independent and simpler sub-specifications. Being inspired by one of the approaches, developed by Antonio Iannopollo, Stavros Tripakis, and Alberto Sangiovanni-Vincentelli (2018), who designed the so-called DecomposeContract (DC} algorithm, we present here our solution that takes their ideas further and provides mathematical formalisation of the strategy behind DC. We rigorously define the main notions involved in the algorithm, explain the technique, and demonstrate its application on examples. The core technique of DC is based on the detection of independent variables in linear temporal logic formulae by exploiting the power and efficiency of a model checker. While working on the problem, we discovered that the DC algorithm, which is very smart and not trivial, needs to be corrected - we illustrate this by providing a counterexample showing that DC is not sound. Introducing relevant corrections, we are able to adapt DC's original strategy securing its correctness. The modification of DC and the detailed proof of its soundness and completeness are the main contributions of this paper.

翻译：近期，多项算法被提出用于将反应式综合规约分解为独立且更简单的子规约。受Antonio Iannopollo、Stavros Tripakis与Alberto Sangiovanni-Vincentelli（2018）所设计的DecomposeContract（DC）算法启发，我们在此提出自己的解决方案，该方案进一步拓展了其思想，并为DC背后的策略提供了数学形式化。我们严格定义了算法涉及的主要概念，阐述了该技术，并通过示例展示其应用。DC的核心技术在于利用模型检查器的能力与效率，在线性时序逻辑公式中检测独立变量。在解决该问题的过程中，我们发现该算法虽极具巧思且非平凡，但需要修正——我们通过提供反例证明DC并非可靠。通过引入相关修正，我们能够调整DC的原始策略以确保其正确性。本文的主要贡献在于对DC的改进，以及对其可靠性与完备性的详细证明。