{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,29]],"date-time":"2025-11-29T07:49:28Z","timestamp":1764402568873,"version":"3.40.3"},"reference-count":23,"publisher":"Springer Science and Business Media LLC","issue":"5-6","license":[{"start":{"date-parts":[[2012,6,8]],"date-time":"2012-06-08T00:00:00Z","timestamp":1339113600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2013,10]]},"DOI":"10.1007\/s10009-012-0236-z","type":"journal-article","created":{"date-parts":[[2012,7,9]],"date-time":"2012-07-09T01:33:18Z","timestamp":1341797598000},"page":"603-618","source":"Crossref","is-referenced-by-count":24,"title":["Synthesis from component libraries"],"prefix":"10.1007","volume":"15","author":[{"given":"Yoad","family":"Lustig","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,6,8]]},"reference":[{"key":"236_CR1","unstructured":"Church, A.: Logic, arithmetics, and automata. In: Proceedings of International Congress of Mathematicians, 1962, pp. 23\u201335. Institut Mittag-Leffler (1963)"},{"key":"236_CR2","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proceedings of 16th ACM Symposium on Principles of Programming Languages, pp. 179\u2013190 (1989)","DOI":"10.1145\/75277.75293"},{"key":"236_CR3","doi-asserted-by":"crossref","unstructured":"Sifakis, J.: A framework for component-based construction extended abstract. In: Proceedings of 3rd International Conference on Software Engineering and Formal Methods (SEFM 2005), pp 293\u2013300. IEEE Computer Society (2005)","DOI":"10.1109\/SEFM.2005.3"},{"key":"236_CR4","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-10876-5","volume-title":"Web Services\u2014Concepts, Architectures and Applications","author":"G. Alonso","year":"2004","unstructured":"Alonso G., Casati F., Kuno H.A., Machiraju V.: Web Services\u2014Concepts, Architectures and Applications. Springer, Berlin (2004)"},{"key":"236_CR5","doi-asserted-by":"crossref","unstructured":"Berardi, D., Calvanese, D., Giacomo, G.D., Lenzerini, M., Mecella, M.: Automatic composition of e-services that export their behavior. In: ICSOC, pp. 43\u201358 (2003)","DOI":"10.1007\/978-3-540-24593-3_4"},{"key":"236_CR6","unstructured":"Sardi\u00f1a, S., Patrizi, F., Giacomo, G.D.: Automatic synthesis of a global behavior from multiple distributed behaviors. In: AAAI, pp. 1063\u20131069 (2007)"},{"key":"236_CR7","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1090\/S0002-9947-1969-0280205-0","volume":"138","author":"J. B\u00fcchi","year":"1969","unstructured":"B\u00fcchi J., Landweber L.: Solving sequential conditions by finite-state strategies. Trans. AMS 138, 295\u2013311 (1969)","journal-title":"Trans. AMS"},{"key":"236_CR8","doi-asserted-by":"crossref","DOI":"10.1090\/cbms\/013","volume-title":"Automata on infinite objects and Church\u2019s problem","author":"M. Rabin","year":"1972","unstructured":"Rabin M.: Automata on infinite objects and Church\u2019s problem. American Mathematical Society, New York (1972)"},{"key":"236_CR9","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: Distributed reactive systems are hard to synthesize. In: Proceedings of 31st IEEE Symposium on Foundations of Computer Science, pp. 746\u2013757 (1990)","DOI":"10.1109\/FSCS.1990.89597"},{"key":"236_CR10","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.: Safraless decision procedures. In: Proceedings of 46th IEEE Symposium on Foundations of Computer Science, pp 531\u2013540 (2005)","DOI":"10.1109\/SFCS.2005.66"},{"key":"236_CR11","doi-asserted-by":"crossref","unstructured":"Krishnamurthi, S., Fisler, K.: Foundations of incremental aspect model-checking. ACM Trans. Softw. Eng. Methods 16(2) (2007)","DOI":"10.1145\/1217295.1217296"},{"key":"236_CR12","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1007\/1-4020-3532-2_3","volume-title":"Engineering Theories of Software-Intensive Systems. NATO Science Series: Mathematics, Physics, and Chemistry, vol. 195","author":"L. Alfaro de","year":"2005","unstructured":"de Alfaro L., Henzinger T.: Interface-based design. In: Broy, M., Gr\u00fcnbauer, J., Harel, D., Hoare, C. (eds) Engineering Theories of Software-Intensive Systems. NATO Science Series: Mathematics, Physics, and Chemistry, vol. 195. pp. 83\u2013104. Springer, Berlin (2005)"},{"key":"236_CR13","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proceedings of 18th IEEE Symposium on Foundations of Computer Science, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"236_CR14","doi-asserted-by":"crossref","unstructured":"Gabbay, D., Pnueli, A., Shelah, S., Stavi, J.: On the temporal analysis of fairness. In: Proceedings of 7th ACM Symposium on Principles of Programming Languages, pp. 163\u2013173 (1980)","DOI":"10.1145\/567446.567462"},{"key":"236_CR15","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1016\/0304-3975(87)90133-2","volume":"54","author":"D. Muller","year":"1987","unstructured":"Muller D., Schupp P.: Alternating automata on infinite trees. Theor. Comput. Sci. 54, 267\u2013276 (1987)","journal-title":"Theor. Comput. Sci."},{"key":"236_CR16","doi-asserted-by":"crossref","unstructured":"Muller, D., Saoudi, A., Schupp, P.: Alternating automata, the weak monadic theory of the tree and its complexity. In: Proceedings of 13th International Colloqium on Automata, Languages, and Programming. Lecture Notes in Computer Science, vol. 226, pp. 275\u2013283. Springer, Berlin (1986)","DOI":"10.1007\/3-540-16761-7_77"},{"key":"236_CR17","volume-title":"Introduction to Automata Theory, Languages, and Computation","author":"J. Hopcroft","year":"1979","unstructured":"Hopcroft J., Ullman J.: Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, New York (1979)"},{"key":"236_CR18","doi-asserted-by":"crossref","unstructured":"Nain, S., Vardi, M.Y.: Branching vs. linear time: semantical perspective. In: 5th international symposium on automated technology for verification and analysis. Lecture Notes in Computer Science, vol. 4762, pp. 19\u201334. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-75596-8_4"},{"key":"236_CR19","volume-title":"Model Checking","author":"E. Clarke","year":"1999","unstructured":"Clarke E., Grumberg O., Peled D.: Model Checking. MIT Press, Cambridge (1999)"},{"issue":"6","key":"236_CR20","doi-asserted-by":"crossref","first-page":"307","DOI":"10.1016\/0020-0190(86)90071-2","volume":"22","author":"K. Apt","year":"1986","unstructured":"Apt K., Kozen D.: Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett. 22(6), 307\u2013309 (1986)","journal-title":"Inf. Process. Lett."},{"key":"236_CR21","unstructured":"Rosner, R.: Modular Synthesis of Reactive Systems. PhD thesis, Weizmann Institute of Science (1992)"},{"issue":"1","key":"236_CR22","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M. Vardi","year":"1994","unstructured":"Vardi M., Wolper P.: Reasoning about infinite computations. Inf. Comput. 115(1), 1\u201337 (1994)","journal-title":"Inf. Comput."},{"key":"236_CR23","doi-asserted-by":"crossref","unstructured":"Gr\u00e4del, E., Thomas, W., Wilke, T.: Automata, logics, and infinite games: a guide to current research. Lecture Notes in Computer Science, vol. 2500. Springer, Berlin (2002)","DOI":"10.1007\/3-540-36387-4"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-012-0236-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-012-0236-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-012-0236-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,3]],"date-time":"2025-04-03T16:19:50Z","timestamp":1743697190000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-012-0236-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,6,8]]},"references-count":23,"journal-issue":{"issue":"5-6","published-print":{"date-parts":[[2013,10]]}},"alternative-id":["236"],"URL":"https:\/\/doi.org\/10.1007\/s10009-012-0236-z","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2012,6,8]]}}}