Revisiting the specification decomposition for synthesis based on LTL solvers

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.