Reactive synthesis aims to automatically generate systems from high-level formal specifications, but its inherent complexity limits its scalability to real-world scenarios. This limitation can be addressed 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.
The following link provides access to the code and detailed instructions for installing and replicating the tool and experiments from the paper “Mode-Based Reactive Synthesis” accepted in NFM 2025:
Link to the paper: https://link.springer.com/chapter/10.1007/978-3-031-93706-4_8
PDF: Link
https://drive.google.com/drive/folders/1-dJhioGvCWuDg1jiKKOqCx0fHOc7-PGT?usp=sharing
The artifact contains two main files:
moby.tar: This is a Docker image that includes the complete project. Please refer to the README file for instructions on how to install and run the tool using this image.
Source Code: If you prefer, you can install everything from scratch using the provided source code, with or without Docker. Again, please consult the README file for detailed setup instructions.