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 (2018), who designed the so-called (DC) algorithm, we present here our solution that takes his 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. Although the DC algorithm is sound, it is not complete, as its author already pointed out. In this paper, we provide a counterexample that shows this fact and propose relevant changes to adapt the original DC strategy to ensure its correctness. The modification of DC and the detailed proof of its soundness and completeness are the main contributions of this work.

翻译：近期，多项算法被提出用于将反应式综合规约分解为独立且更简单的子规约。受Antonio Iannopollo（2018）所设计的DC（分解算法）方法的启发，我们提出了本文的解决方案。该方案进一步发展了他的思想，并对DC背后的策略提供了数学形式化描述。我们严格定义了算法涉及的核心概念，阐述了技术细节，并通过示例展示了其应用。DC的核心技术在于利用模型检测器的强大能力与高效性，在线性时态逻辑公式中检测独立变量。尽管DC算法是可靠的，但其作者已指出其并不完备。本文给出了一个反例以证明这一缺陷，并提出了对原始DC策略的相关修正以确保其正确性。DC算法的改进及其正确性与完备性的详细证明构成了本研究的主要贡献。