  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.
