Recent work has proposed algorithms for decomposing reactive synthesis specifications into simpler and independent subspecifications. Motivated by the DecomposeContract algorithm introduced by Antonio Iannopollo, we revisit this approach and provide a mathematical account of the notion of independence on which it is based. The central idea in this setting is to identify independence among system-controlled variables in linear temporal logic formulae by exploiting the power of a model checker. Although the original DecomposeContract algorithm is sound, it is not complete. We support this observation by presenting a concrete counterexample, and we then propose a refined decomposition procedure that preserves the model-checking-based nature of the original method while ensuring completeness. Beyond this algorithmic result, our main contribution is a rigorous semantic analysis of the method, which reveals the principles behind it and makes its limitations explicit.

翻译：近期研究提出了将反应式合成规约分解成更简单且独立子规约的算法。受Antonio Iannopollo提出的DecomposeContract算法启发，我们重新审视了该方法，并对其所依赖的独立性概念给出了数学化解释。该场景的核心思想是通过利用模型检查器的能力，在线性时序逻辑公式中识别系统控制变量间的独立性。尽管原始DecomposeContract算法是可靠的，但它并不完备。我们通过给出具体反例来支持这一观察，随后提出了一种改进的分解过程，该过程在保持原始方法基于模型检查特性的同时保证了完备性。除算法成果外，我们的主要贡献在于对方法进行了严格的语义分析，揭示了其背后的原理并明确指出了其局限性。