Modularization of Formal Specifications or Efficient Synthesis of Reactive Systems

Reactive systems respond to requests from an environment with appropriate timing. Because reactive systems are used widely in infrastructure, it is necessary that they are developed without flaws. Automatic synthesis of reactive systems from particular specifications is an ideal technique for ensuring development without flaws. Several tools for synthesis have been proposed, e.g., Lily, AcaciaPlus and Unbeast. Among them, AcaciaPlus can synthesize systems compositionally, and enables synthesis from large-scale specifications that could not previously be treated. However, the modularization of specifications depends largely on the computation time required for synthesis; this is not a trivial problem. In this paper, we discuss the modularization of specifications to enable efficient synthesis of reactive systems.