Synthesis of Hierarchical Systems

  • Benjamin Aminof
  • Fabio Mogavero
  • Aniello Murano
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7253)


In automated synthesis, given a specification, we automatically create a system that is guaranteed to satisfy the specification. In the classical temporal synthesis algorithms, one usually creates a “flat” system “from scratch”. However, real-life software and hardware systems are usually created using preexisting 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” approach to system design. Our algorithm works by synthesizing in many rounds, when at each round the system designer provides the specification of the currently 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 hierarchical components is Exptime-complete for μ-calculus, and 2Exptime-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.


Temporal Logic Computation Tree Linear Temporal Logic Hierarchical System Input Tree 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Alur, R., Arenas, M., Barceló, P., Etessami, K., Immerman, N., Libkin, L.: First-Order and Temporal Logics for Nested Words. In: Logical Methods in Computer Science, vol. 4 (2008)Google Scholar
  2. 2.
    Alur, R., Benedikt, M., Etessami, K., Godefroid, P., Reps, T.W., Yannakakis, M.: Analysis of recursive state machines. ACM Trans. Program. Lang. Syst. 27(4), 786–818 (2005)CrossRefGoogle Scholar
  3. 3.
    Alur, R., Chaudhuri, S., Etessami, K., Madhusudan, P.: On-the-Fly Reachability and Cycle Detection for Recursive State Machines. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 61–76. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  4. 4.
    Alur, R., Chaudhuri, S., Madhusudan, P.: A fixpoint calculus for local and global program flows. In: POPL 2006, pp. 153–165. ACM (2006)Google Scholar
  5. 5.
    Alur, R., Yannakakis, M.: Model checking of hierarchical state machines. ACM Trans. Program. Lang. Syst. 23(3), 273–303 (2001)CrossRefGoogle Scholar
  6. 6.
    Aminof, B., Kupferman, O., Murano, A.: Improved Model Checking of Hierarchical Systems. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol. 5944, pp. 61–77. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  7. 7.
    Church, A.: Logic, arithmetics, and automata. In: Proc. International Congress of Mathematicians, 1962, pp. 23–35. Institut Mittag-Leffler (1963)Google Scholar
  8. 8.
    de Alfaro, L., Henzinger, T.A.: Interface-based design. In: Engineering Theories of Software-Intensive Systems. NATO Science Series: Mathematics, Physics, and Chemistry, vol. 195, pp. 83–104. Springer (2005)Google Scholar
  9. 9.
    Eisner, C., Fisman, D., Havlicek, J., Lustig, Y., McIsaac, A., Van Campenhout, D.: Reasoning with Temporal Logic on Truncated Paths. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 27–39. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  10. 10.
    Emerson, E.A.: Temporal and modal logic. In: Van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, ch. 16, vol. B, pp. 997–1072. Elsevier, MIT Press (1990)Google Scholar
  11. 11.
    Emerson, E.A., Jutla, C.: Tree automata, μ-calculus and determinacy. In: FOCS 1991, pp. 368–377 (1991)Google Scholar
  12. 12.
    Göller, S., Lohrey, M.: Fixpoint Logics on Hierarchical Structures. In: Sarukkai, S., Sen, S. (eds.) FSTTCS 2005. LNCS, vol. 3821, pp. 483–494. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  13. 13.
    Guelev, D.P., Ryan, M.D., Schobbens, P.Y.: Synthesising features by games. Electr. Notes Theor. Comput. Sci. 145, 79–93 (2006)CrossRefGoogle Scholar
  14. 14.
    Janin, D., Walukiewicz, I.: Automata for the Modal μ-Calculus and Related Results. In: Hájek, P., Wiedermann, J. (eds.) MFCS 1995. LNCS, vol. 969, pp. 552–562. Springer, Heidelberg (1995)CrossRefGoogle Scholar
  15. 15.
    Kupferman, O., Vardi, M.Y.: μ-Calculus Synthesis. In: Nielsen, M., Rovan, B. (eds.) MFCS 2000. LNCS, vol. 1893, pp. 497–507. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  16. 16.
    Kupferman, O., Vardi, M.Y., Wolper, P.: An automata-theoretic approach to branching-time model checking. J. of the ACM 47(2), 312–360 (2000)MathSciNetzbMATHCrossRefGoogle Scholar
  17. 17.
    Lanotte, R., Maggiolo-Schettini, A., Peron, A.: Structural Model Checking for Communicating Hierarchical Machines. In: Fiala, J., Koubek, V., Kratochvíl, J. (eds.) MFCS 2004. LNCS, vol. 3153, pp. 525–536. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  18. 18.
    Lustig, Y., Vardi, M.Y.: Synthesis from Component Libraries. In: de Alfaro, L. (ed.) FOSSACS 2009. LNCS, vol. 5504, pp. 395–409. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  19. 19.
    Lustig, Y., Vardi, M.Y.: Synthesis from Recursive-Components libraries. In: GandALF 2011. EPTCS, vol. 54, pp. 1–16 (2011)Google Scholar
  20. 20.
    Muller, D.E., Schupp, P.E.: Alternating automata on infinite trees. J. of Theor. Comp. Sc. 54, 267–276 (1987)MathSciNetzbMATHCrossRefGoogle Scholar
  21. 21.
    Müller, P.: Modular specification and verification of object-oriented programs. Springer (2002)Google Scholar
  22. 22.
    Piterman, N., Pnueli, A., Sa’ar, Y.: Synthesis of Reactive(1) Designs. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 364–380. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  23. 23.
    Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL 1989, pp. 179–190. ACM Press (1989)Google Scholar
  24. 24.
    Rabin, M.O.: Weakly definable relations and special automata. In: Proc. Symp. Math. Logic and Foundations of Set Theory, pp. 1–23. North Holland (1970)Google Scholar
  25. 25.
    Rosner, R.: Modular Synthesis of Reactive Systems. PhD thesis, Weizmann Institute of Science (1992)Google Scholar
  26. 26.
    Sifakis, J.: A framework for component-based construction extended abstract. In: SEFM 2005, pp. 293–300. IEEE Computer Society (2005)Google Scholar
  27. 27.
    Bliudze, S., Sifakis, J.: Synthesizing Glue Operators from Glue Constraints for the Construction of Component-Based Systems. In: Apel, S., Jackson, E. (eds.) SC 2011. LNCS, vol. 6708, pp. 51–67. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  28. 28.
    Wilke, T.: Alternating tree automata, parity games, and modal μ-calculus. Bull. Soc. Math. Belg. 8(2) (2001)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • Benjamin Aminof
    • 1
  • Fabio Mogavero
    • 2
  • Aniello Murano
    • 2
  1. 1.Hebrew UniversityJerusalemIsrael
  2. 2.Università degli Studi di Napoli “Federico II”NapoliItaly

Personalised recommendations