Yoad Lustig, Moshe Y. Vardi
12th International Conference Foundations of Software Science and Computational Structures (FOSSACS), York, UK, 2009, pages 395-409
Used by the Cassting project
Synthesis is the automated construction of a system from its specification. In the classical temporal 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 web-service orchestration, can be modeled as synthesis of a system from a library of components. This work defines and studies the synthesis problem from libraries of reusable components. It considers two notions of composition: data-flow composition, for which the problem is undecidable, and control-flow composition, for which the problem is 2EXPTIME-complete. As a side benefit, an explicit characterization of the information needed by the synthesizer on the underlying components is obtained. This characterization can be used as a specification formalism between component providers and integrators.