{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T14:06:38Z","timestamp":1743084398689,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642279393"},{"type":"electronic","value":"9783642279409"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-27940-9_19","type":"book-chapter","created":{"date-parts":[[2012,1,19]],"date-time":"2012-01-19T02:29:29Z","timestamp":1326940169000},"page":"283-298","source":"Crossref","is-referenced-by-count":9,"title":["Effective Synthesis of Asynchronous Systems from GR(1) Specifications"],"prefix":"10.1007","author":[{"given":"Uri","family":"Klein","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nir","family":"Piterman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Amir","family":"Pnueli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"19_CR1","doi-asserted-by":"crossref","unstructured":"Bloem, R., Galler, S., Jobstmann, B., Piterman, N., Pnueli, A., Weiglhofer, M.: Automatic hardware synthesis from specifications: A case study. In: DATE, pp. 1188\u20131193 (2007)","DOI":"10.1109\/DATE.2007.364456"},{"key":"19_CR2","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1090\/S0002-9947-1969-0280205-0","volume":"138","author":"J.R. B\u00fcchi","year":"1969","unstructured":"B\u00fcchi, J.R., Landweber, L.H.: Solving sequential conditions by finite-state strategies. Trans. AMS\u00a0138, 295\u2013311 (1969)","journal-title":"Trans. AMS"},{"key":"19_CR3","unstructured":"Church, A.: Logic, arithmetic and automata. In: Proc. 1962 Int. Congr. Math., Upsala, pp. 23\u201325 (1963)"},{"key":"19_CR4","unstructured":"Clarke, E.C., Grumberg, O., Peled, D.: Model Checking. MIT Press (1999)"},{"key":"19_CR5","doi-asserted-by":"crossref","unstructured":"Conner, D.C., Kress-Gazit, H., Choset, H., Rizzi, A., Pappas, G.J.: Valet parking without a valet. In: IRSES, pp. 572\u2013577. IEEE (2007)","DOI":"10.1109\/IROS.2007.4399374"},{"key":"19_CR6","doi-asserted-by":"crossref","unstructured":"D\u2019Ippolito, N., Braberman, V., Piterman, N., Uchitel, S.: Synthesis of live behavior models for fallible domains. In: ICSE. ACM (2011)","DOI":"10.1145\/1985793.1985823"},{"key":"19_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/11874683_26","volume-title":"Computer Science Logic","author":"T.A. Henzinger","year":"2006","unstructured":"Henzinger, T.A., Piterman, N.: Solving Games Without Determinization. In: \u00c9sik, Z. (ed.) CSL 2006. LNCS, vol.\u00a04207, pp. 395\u2013410. Springer, Heidelberg (2006)"},{"key":"19_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/978-3-642-00593-0_6","volume-title":"Fundamental Approaches to Software Engineering","author":"H. Kugler","year":"2009","unstructured":"Kugler, H., Plock, C., Pnueli, A.: Controller Synthesis from LSC Requirements. In: Chechik, M., Wirsing, M. (eds.) FASE 2009. LNCS, vol.\u00a05503, pp. 79\u201393. Springer, Heidelberg (2009)"},{"key":"19_CR9","doi-asserted-by":"crossref","unstructured":"Klein, U., Piterman, N., Pnueli, A.: Effective Synthesis of Asynchronous Systems from GR(1) Specifications. Tech Rep TR2011-944, Courant Inst of Math Sci, NYU","DOI":"10.1007\/978-3-642-27940-9_19"},{"key":"19_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-642-00768-2_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H. Kugler","year":"2009","unstructured":"Kugler, H., Segall, I.: Compositional Synthesis of Reactive Systems from Live Sequence Chart Specifications. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol.\u00a05505, pp. 77\u201391. Springer, Heidelberg (2009)"},{"key":"19_CR11","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: FOCS (2005)","DOI":"10.1109\/SFCS.2005.66"},{"key":"19_CR12","doi-asserted-by":"crossref","unstructured":"Piterman, N., Pnueli, A.: Faster solution of Rabin and Streett games. In: LICS, IEEE. IEEE Press (2006)","DOI":"10.1109\/LICS.2006.23"},{"key":"19_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11609773_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"N. Piterman","year":"2005","unstructured":"Piterman, N., Pnueli, A., Sa\u2019ar, Y.: Synthesis of Reactive(1) Designs. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 364\u2013380. Springer, Heidelberg (2005)"},{"key":"19_CR14","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Klein, U.: Synthesis of programs from temporal property specifications. In: MEMOCODE, pp. 1\u20137. IEEE Press (2009)","DOI":"10.1109\/MEMCOD.2009.5185372"},{"key":"19_CR15","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL, pp. 179\u2013190 (1989)","DOI":"10.1145\/75277.75293"},{"key":"19_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"652","DOI":"10.1007\/BFb0035790","volume-title":"Automata, Languages and Programming","author":"A. Pnueli","year":"1989","unstructured":"Pnueli, A., Rosner, R.: On the Synthesis of an Asynchronous Reactive Module. In: Ronchi Della Rocca, S., Ausiello, G., Dezani-Ciancaglini, M. (eds.) ICALP 1989. LNCS, vol.\u00a0372, pp. 652\u2013671. Springer, Heidelberg (1989)"},{"key":"19_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-14295-6_18","volume-title":"Computer Aided Verification","author":"A. Pnueli","year":"2010","unstructured":"Pnueli, A., Sa\u2019ar, Y., Zuck, L.D.: Jtlv: A Framework for Developing Verification Algorithms. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 171\u2013174. Springer, Heidelberg (2010)"},{"key":"19_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1007\/978-3-540-69850-0_11","volume-title":"25MC Festschrift","author":"A. Pnueli","year":"2008","unstructured":"Pnueli, A., Zaks, A.: On the Merits of Temporal Testers. In: Grumberg, O., Veith, H. (eds.) 25MC Festschrift. LNCS, vol.\u00a05000, pp. 172\u2013195. Springer, Heidelberg (2008)"},{"key":"19_CR19","doi-asserted-by":"crossref","unstructured":"Rabin, M.O.: Automata on Infinite Objects and Church\u2019s Problem. AMS (1972)","DOI":"10.1090\/cbms\/013"},{"key":"19_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/978-3-540-71410-1_10","volume-title":"Logic-Based Program Synthesis and Transformation","author":"S. Schewe","year":"2007","unstructured":"Schewe, S., Finkbeiner, B.: Synthesis of Asynchronous Systems. In: Puebla, G. (ed.) LOPSTR 2006. LNCS, vol.\u00a04407, pp. 127\u2013142. Springer, Heidelberg (2007)"},{"key":"19_CR21","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0304-3975(87)90008-9","volume":"49","author":"A.P. Sistla","year":"1987","unstructured":"Sistla, A.P., Vardi, M.Y., Wolper, P.: The complementation problem for B\u00fcchi autamata with application to temporal logic. TCS\u00a049, 217\u2013237 (1987)","journal-title":"TCS"},{"key":"19_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/3-540-60045-0_56","volume-title":"Computer Aided Verification","author":"M.Y. Vardi","year":"1995","unstructured":"Vardi, M.Y.: An Automata-Theoretic Approach to Fair Realizability and Synthesis. In: Wolper, P. (ed.) CAV 1995. LNCS, vol.\u00a0939, pp. 267\u2013278. Springer, Heidelberg (1995)"},{"issue":"1","key":"19_CR23","first-page":"1","volume":"115","author":"M.Y. Vardi","year":"1994","unstructured":"Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. I&C\u00a0115(1), 1\u201337 (1994)","journal-title":"I&C"},{"key":"19_CR24","doi-asserted-by":"crossref","unstructured":"Wongpiromsarn, T., Topcu, U., Murray, R.M.: Receding horizon control for temporal logic specifications. In: Johansson, K.H., Yi, W. (eds.) Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2010, Stockholm, Sweden, April 12-15, 2010, pp. 101\u2013110. ACM (2010) ISBN 978-1-60558-955-8","DOI":"10.1145\/1755952.1755968"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-27940-9_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,22]],"date-time":"2019-06-22T13:42:55Z","timestamp":1561210975000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-27940-9_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642279393","9783642279409"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-27940-9_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}