Revisiting the specification decomposition for synthesis based on LTL solvers

TL;DR

This paper formalizes and improves the DC algorithm for decomposing LTL specifications in reactive synthesis, ensuring its correctness and completeness through rigorous proofs and counterexamples.

Contribution

It provides a formal mathematical framework for the DC algorithm, introduces modifications for correctness, and proves its soundness and completeness.

Findings

The original DC algorithm is sound but not complete.

Counterexample demonstrates the incompleteness of the original DC.

Modified DC algorithm is both sound and complete.

Abstract

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.