Specification Decomposition for Reactive Synthesis

TL;DR

This paper introduces a modular synthesis algorithm that decomposes specifications into smaller parts, enabling more efficient reactive system synthesis while guaranteeing correctness and independence of subspecifications.

Contribution

It presents a sound and complete decomposition method for reactive synthesis that improves scalability by enabling independent synthesis of subspecifications.

Findings

Significant reduction in synthesis runtime with modular approach

Guarantees correctness and independence of subspecifications

Applicable as a preprocessing step to various synthesis tools

Abstract

Reactive synthesis is the task of automatically deriving a correct implementation from a specification. It is a promising technique for the development of verified programs and hardware. Despite recent advances in terms of algorithms and tools, however, reactive synthesis is still not practical when the specified systems reach a certain bound in size and complexity. In this paper, we present a sound and complete modular synthesis algorithm that automatically decomposes the specification into smaller subspecifications. For them, independent synthesis tasks are performed, significantly reducing the complexity of the individual tasks. Our decomposition algorithm guarantees that the subspecifications are independent in the sense that completely separate synthesis tasks can be performed for them. Moreover, the composition of the resulting implementations is guaranteed to satisfy the original specification. Our algorithm is a preprocessing technique that can be applied to a wide range of synthesis tools. We evaluate our approach with state-of-the-art synthesis tools on established benchmarks: The runtime decreases significantly when synthesizing implementations modularly.