Synthesis from Component Libraries

Abstract. Synthesis is the automatic construction of a system from its specification. In the classical synthesis algorithms it is always assumed the system is “constructed from scratch” rather than “composed” from reusable components. This, of course, rarely happens in real life. In real life, almost every non-trivial commercial system, either in hardware or in software system, relies heavily on using libraries of reusable components. Furthermore, other contexts, such as webservice orchestration, can be modeled as synthesis of a system from a library of components. In this work we define and study the problem of LTL synthesis from libraries of reusable components. We define two notions of composition: functional composition, for which we prove the problem is undecidable, and structural composition, for which we prove the problem is 2EXPTIME-complete. As a side benefit we derive an explicit characterization of the information needed by the synthesizer on the underlying compo...

• Type: Conference
• Year: 2009
• Where: FOSSACS
• Authors: Yoad Lustig, Moshe Y. Vardi
• Keywords: Applied Computing, FOSSACS 2009, Non-trivial Commercial System, Real Life, Reusable Components