Synthesis of Hierarchical Systems

In automated synthesis, given a specification, we automatically cre- ate a system that is guaranteed to satisfy the specification. In the classical tem- poral synthesis algorithms, one usually creates a “flat” system “from scratch”. However, real-life software and hardware systems are usually created using pre- existing libraries of reusable components, and are not “flat” since repeated sub- systems are described only once. In this work we describe an algorithm for the synthesis of a hierarchical system from a library of hierarchical components, which follows the “bottom-up” ap- proach to system design. Our algorithm works by synthesizing in many rounds, when at each round the system designer provides the specification of the cur- rently desired module, which is then automatically synthesized using the initial library and the previously constructed modules. To ensure that the synthesized module actually takes advantage of the available high-level modules, we guide the algorithm by enforcing certain modularity criteria. We show that the synthesis of a hierarchical system from a library of hierarchi- cal components is E XPTIME-complete for μ-calculus, and 2E XPTIME-complete for LTL, both in the cases of complete and incomplete information. Thus, in all cases, it is not harder than the classical synthesis problem (of synthesizing flat systems “from scratch”), even though the synthesized hierarchical system may be exponentially smaller than a flat one