Specification decomposition for reactive synthesis

Area of Science:

• Computer Science
• Formal Methods
• Software Engineering

Background:

• Reactive synthesis automates the creation of correct implementations from specifications.
• Current reactive synthesis methods struggle with large, complex systems.
• Developing verified programs and hardware requires efficient synthesis techniques.

Purpose of the Study:

• To present a sound and complete modular synthesis algorithm.
• To address the scalability limitations of existing reactive synthesis approaches.
• To enable practical synthesis for complex specified systems.

Main Methods:

• A novel algorithm that decomposes specifications into smaller, independent subspecifications.
• Performing independent synthesis tasks on these subspecifications.
• Guaranteed composition of resulting implementations to satisfy the original specification.

Main Results:

• Significantly reduced complexity for individual synthesis tasks.
• Demonstrated independence of subspecifications allowing parallel synthesis.
• Modular synthesis approach leads to significant runtime decreases on benchmarks.
• The algorithm functions as a preprocessing technique compatible with existing synthesis tools.

Conclusions:

• The modular synthesis algorithm enhances the practicality of reactive synthesis for complex systems.
• This approach offers a scalable solution for verified program and hardware development.
• Modular synthesis is a viable preprocessing technique for state-of-the-art synthesis tools.