Mode-Based Reactive Synthesis

Abstract

Reactive synthesis aims to automatically generate systems from high-level formal specifications, but its inherent complexity limits its scalability to real-world scenarios. Scalability can be improved by decomposing the specification into independent parts for parallel synthesis, but the dependency between variables limits this approach. At the same time, specifications used in Requirements Engineering (RE) often include high-level state machine descriptions, known as modes, which structure the specification. This paper introduces a novel method for the sequential decomposition of reactive synthesis problems based on modes. Our approach automatically uses modes to break down a specification into smaller sub-specifications, synthesizes each independently, and then integrates the solutions into a cohesive global model. We present an algorithm that exploits mode transitions and ensures consistency across synthesized components leveraging off-the-shelf reactive synthesis tools. We prove the correctness of our approach and show empirically that our method significantly improves scalability when decomposing real-world specifications, outperforming state-of-the-art monolithic tools. As the first sequential decomposition approach, our method offers a promising alternative for scalable reactive synthesis.