Resolving Goal-Conflicts and Scaling Synthesis through Mode-Based Decomposition

Reactive synthesis, with its roots in the work of A. Church, presents a transformative approach for the formal methods community. It seeks to translate system behaviors expressed in Linear-Time Temporal Logic (LTL) into correct-by-construction models using synthesis tools. However, this approach faces substantial challenges. Among these challenges is the high computational complexity of LTL synthesis, which constrains its application to large-scale systems. Additionally, unrealizable specifications present a significant obstacle as they act as barriers, impeding the synthesis process. Furthermore, the presence of goal-conflicts within requirements introduces contradictions and ambiguity, further complicating the synthesis process. These issues collectively make synthesis demanding, often resulting in suboptimal or unviable systems.