Developing critical components, such as mission controllers or embedded systems, is a challenging task. Reactive synthesis is a technique to automatically produce correct controllers. Given a high-level specification written in LTL, reactive synthesis consists of computing a system that satisfies the specification as long as the environment respects the assumptions. Unfortunately, LTL synthesis suffers from high computational complexity which precludes its use for many large cases. A promising approach to improve synthesis scalability consists of decomposing a safety specification into smaller specifications, that can be processed independently and composed into a solution for the original specification. Previous decomposition methods focus on identifying independent parts of the specification whose systems are combined via simultaneous execution. In this work, we propose a novel decomposition algorithm based on modes, which consists of decomposing a complex safety specification into smaller problems whose solution is then composed sequentially (instead of simultaneously). The input to our algorithm is the original specification and the description of the modes. We show how to generate sub-specifications automatically and we prove that if all sub-problems are realizable then the full specification is realizable. Moreover, we show how to construct a system for the original specification from sub-systems for the decomposed specifications. We finally illustrate the feasibility of our approach with multiple case studies using off-the-self synthesis tools to process the obtained sub-problems.

翻译：开发关键组件（如任务控制器或嵌入式系统）是一项具有挑战性的任务。反应式综合是一种自动生成正确控制器的技术。给定用线性时态逻辑（LTL）编写的高层规约，反应式综合旨在计算一个系统，只要环境满足假设条件，该系统就能满足规约。然而，LTL综合面临计算复杂度高的难题，这限制了其在许多大规模案例中的应用。一种提升综合可扩展性的有效方法是将安全规约分解为若干较小的规约，这些子规约可独立处理，并组合成原规约的解。以往的分解方法侧重于识别规约中可独立的部分，通过并行执行方式组合其系统。在本工作中，我们提出了一种基于模式的新型分解算法，该算法将复杂的安全规约分解为若干较小的问题，其解以顺序（而非并行）方式组合。我们算法的输入包括原始规约和模式的描述。我们展示了如何自动生成子规约，并证明了若所有子问题均可实现，则完整规约也必然可解。此外，我们还展示了如何由分解规约的子系统构造出原始规约的系统。最后，通过使用现成综合工具处理所获子问题的多个案例研究，验证了我们方法的可行性。