{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,5]],"date-time":"2026-10-05T05:59:21Z","timestamp":1791179961147,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":37,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642403125","type":"print"},{"value":"9783642403132","type":"electronic"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-40313-2_6","type":"book-chapter","created":{"date-parts":[[2013,8,16]],"date-time":"2013-08-16T10:36:43Z","timestamp":1376649403000},"page":"45-49","source":"Crossref","is-referenced-by-count":1,"title":["Synthesis from Temporal Specifications: New Applications in Robotics and Model-Driven Development"],"prefix":"10.1007","author":[{"given":"Nir","family":"Piterman","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"6_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/11605157_22","volume-title":"Implementation and Application of Automata","author":"C.S. Althoff","year":"2006","unstructured":"Althoff, C.S., Thomas, W., Wallmeier, N.: Observations on determinization of B\u00fcchi automata. In: Farr\u00e9, J., Litovsky, I., Schmitz, S. (eds.) CIAA 2005. LNCS, vol.\u00a03845, pp. 262\u2013272. Springer, Heidelberg (2006)"},{"key":"6_CR2","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: Design Automation and Test in Europe, pp. 1188\u20131193 (2007)","DOI":"10.1109\/DATE.2007.364456"},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"Bloem, R., Galler, S., Jobstmann, B., Piterman, N., Pnueli, A., Weiglhofer, M.: Specify, compile, run: Hardware from PSL. In: 6th International Workshop on Compiler Optimization Meets Compiler Verification. Electronic Notes in Computer Science, vol.\u00a0190, pp. 3\u201316 (2007)","DOI":"10.1016\/j.entcs.2007.09.004"},{"issue":"3","key":"6_CR4","doi-asserted-by":"publisher","first-page":"911","DOI":"10.1016\/j.jcss.2011.08.007","volume":"78","author":"R. Bloem","year":"2012","unstructured":"Bloem, R., Jobstmann, B., Piterman, N., Pnueli, A., Sa\u2019ar, Y.: Synthesis of reactive(1) designs. Journal of Computer and Systems Science\u00a078(3), 911\u2013938 (2012)","journal-title":"Journal of Computer and Systems Science"},{"key":"6_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"652","DOI":"10.1007\/978-3-642-31424-7_45","volume-title":"Computer Aided Verification","author":"A. Bohy","year":"2012","unstructured":"Bohy, A., Bruy\u00e8re, V., Filiot, E., Jin, N., Raskin, J.-F.: Acacia+, a tool for LTL synthesis. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol.\u00a07358, pp. 652\u2013657. Springer, Heidelberg (2012)"},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"Braberman, V., D\u2019Ippolito, N., Piterman, N., Sykes, D., Uchitel, S.: Controller synthesis: From modelling to enactment. In: 35th International Conference on Software Engineering, San Francisco, USA (2013)","DOI":"10.1109\/ICSE.2013.6606714"},{"key":"6_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\u00a0138, 295\u2013311 (1969)","journal-title":"Trans. AMS"},{"key":"6_CR8","first-page":"3","volume-title":"Summaries of the Summer Institute of Symbolic Logic","author":"A. Church","year":"1957","unstructured":"Church, A.: Applications of recursive arithmetic to the problem of circuit synthesis. In: Summaries of the Summer Institute of Symbolic Logic, vol.\u00a0I, pp. 3\u201350. Cornell University, Ithaca (1957)"},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"Conner, D., Kress-Gazit, H., Choset, H., Rizzi, A., Pappas, G.: Valet parking without a valet. In: Proceedings IEEE\/RSJ International Conference on Intelligent Robots and Systems, pp. 572\u2013577. IEEE (2007)","DOI":"10.1109\/IROS.2007.4399374"},{"key":"6_CR10","doi-asserted-by":"crossref","unstructured":"D\u2019Ippolito, N., Braberman, V., Piterman, N., Uchitel, S.: Synthesis of live behavior models for fallible domains. In: 33rd International Conference on Software Engineering. ACM, ACM Press (2011)","DOI":"10.1145\/1985793.1985823"},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"D\u2019Ippolito, N., Braberman, V., Piterman, N., Uchitel, S.: Synthesising non-anomalous event-based controllers for liveness goals. Transactions on Software Engineering and Methodology\u00a022(1) (2012)","DOI":"10.1145\/2430536.2430543"},{"issue":"2","key":"6_CR12","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/s10703-011-0137-x","volume":"40","author":"R. Ehlers","year":"2012","unstructured":"Ehlers, R.: Symbolic bounded synthesis. Formal Methods in System Design\u00a040(2), 232\u2013262 (2012)","journal-title":"Formal Methods in System Design"},{"key":"6_CR13","doi-asserted-by":"crossref","unstructured":"Emerson, E., Jutla, C.: The complexity of tree automata and logics of programs. In: Proc. 29th IEEE Symp. on Foundations of Computer Science, pp. 328\u2013337 (1988)","DOI":"10.1109\/SFCS.1988.21949"},{"key":"6_CR14","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":"6_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/10722167_18","volume-title":"Computer Aided Verification","author":"J. V\u00f6ge","year":"2000","unstructured":"V\u00f6ge, J., Jurdzi\u0144ski, M.: A discrete strategy improvement algorithm for solving parity games. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 202\u2013215. Springer, Heidelberg (2000)"},{"key":"6_CR16","doi-asserted-by":"crossref","unstructured":"Jobstmann, B., Bloem, R.: Game-based and simulation-based improvements for ltl synthesis. In: 3nd Workshop on Games in Design and Verification (2006)","DOI":"10.1109\/FMCAD.2006.22"},{"issue":"3","key":"6_CR17","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/S0020-0190(98)00150-1","volume":"68","author":"M. Jurdzi\u0144ski","year":"1998","unstructured":"Jurdzi\u0144ski, M.: Deciding the winner in parity games is in up \u2229 co-up. Information Processing Letters\u00a068(3), 119\u2013124 (1998)","journal-title":"Information Processing Letters"},{"key":"6_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/11605157_17","volume-title":"Implementation and Application of Automata","author":"J. Klein","year":"2006","unstructured":"Klein, J., Baier, C.: Experiments with deterministic \u03c9-automata for formulas of linear temporal logic. In: Farr\u00e9, J., Litovsky, I., Schmitz, S. (eds.) CIAA 2005. LNCS, vol.\u00a03845, pp. 199\u2013212. Springer, Heidelberg (2006)"},{"key":"6_CR19","series-title":"Lecture Notes in Computer Science","first-page":"161","volume-title":"HVC 2010","author":"U. Klein","year":"2010","unstructured":"Klein, U., Pnueli, A.: Revisiting synthesis of GR(1) specifications. In: Barner, S., Kroening, D., Raz, O. (eds.) HVC 2010. LNCS, vol.\u00a06504, pp. 161\u2013181. Springer, Heidelberg (2010)"},{"key":"6_CR20","doi-asserted-by":"crossref","unstructured":"Kress-Gazit, H., Fainekos, G., Pappas, G.: From structured english to robot motion. In: Proceedings IEEE\/RSJ International Conference on Intelligent Robots and Systems, pp. 2717\u20132722. IEEE (2007)","DOI":"10.1109\/IROS.2007.4398998"},{"key":"6_CR21","doi-asserted-by":"crossref","unstructured":"Kress-Gazit, H., Fainekos, G., Pappas, G.: Where\u2019s waldo? sensor-based temporal logic motion planning. In: Proc. IEEE International Conference on Robotics and Automation, pp. 3116\u20133121. IEEE (2007)","DOI":"10.1109\/ROBOT.2007.363946"},{"key":"6_CR22","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":"6_CR23","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":"6_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/11817963_6","volume-title":"Computer Aided Verification","author":"O. Kupferman","year":"2006","unstructured":"Kupferman, O., Piterman, N., Vardi, M.Y.: Safraless compositional synthesis. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 31\u201344. Springer, Heidelberg (2006)"},{"key":"6_CR25","doi-asserted-by":"crossref","unstructured":"Piterman, N.: From nondeterministic B\u00fcchi and Streett automata to deterministic parity automata. Logical Methods in Computer Science 3(3), e5 (2007)","DOI":"10.2168\/LMCS-3(3:5)2007"},{"key":"6_CR26","unstructured":"Piterman, N., Pnueli, A.: Faster solution of Rabin and Streett games. In: Proc. 21st IEEE Symp. on Logic in Computer Science, pp. 275\u2013284. IEEE, IEEE Computer Society Press (2006)"},{"key":"6_CR27","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":"2006","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 (2006)"},{"key":"6_CR28","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proc. 16th ACM Symp. on Principles of Programming Languages, pp. 179\u2013190 (1989)","DOI":"10.1145\/75277.75293"},{"key":"6_CR29","first-page":"1","volume":"141","author":"M. Rabin","year":"1969","unstructured":"Rabin, M.: Decidability of second order theories and automata on infinite trees. Transaction of the AMS\u00a0141, 1\u201335 (1969)","journal-title":"Transaction of the AMS"},{"key":"6_CR30","doi-asserted-by":"crossref","unstructured":"Raman, V., Piterman, N., Kress-Gazit, H.: Provably correct continuous control for high-level robot behaviors with actions of arbitrary execution durations. In: IEEE International Conference on Robotics and Automation. IEEE, IEEE Computer Society Press (2013)","DOI":"10.1109\/ICRA.2013.6631152"},{"key":"6_CR31","doi-asserted-by":"crossref","unstructured":"Safra, S.: On the complexity of \u03c9-automata. In: Proc. 29th IEEE Symp. on Foundations of Computer Science, pp. 319\u2013327 (1988)","DOI":"10.1109\/SFCS.1988.21948"},{"key":"6_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1007\/978-3-540-77050-3_37","volume-title":"FSTTCS 2007: Foundations of Software Technology and Theoretical Computer Science","author":"S. Schewe","year":"2007","unstructured":"Schewe, S.: Solving parity games in big steps. In: Arvind, V., Prasad, S. (eds.) FSTTCS 2007. LNCS, vol.\u00a04855, pp. 449\u2013460. Springer, Heidelberg (2007)"},{"key":"6_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"474","DOI":"10.1007\/978-3-540-75596-8_33","volume-title":"Automated Technology for Verification and Analysis","author":"S. Schewe","year":"2007","unstructured":"Schewe, S., Finkbeiner, B.: Bounded synthesis. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol.\u00a04762, pp. 474\u2013488. Springer, Heidelberg (2007)"},{"key":"6_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/978-3-642-18098-9_28","volume-title":"Implementation and Application of Automata","author":"M.-H. Tsai","year":"2011","unstructured":"Tsai, M.-H., Fogarty, S., Vardi, M.Y., Tsay, Y.-K.: State of b\u00fcchi complementation. In: Domaratzki, M., Salomaa, K. (eds.) CIAA 2010. LNCS, vol.\u00a06482, pp. 261\u2013271. Springer, Heidelberg (2011)"},{"key":"6_CR35","doi-asserted-by":"crossref","unstructured":"Wongpiromsarn, T., Topcu, U., Murray, R.M.: Receding horizon temporal logic planning for dynamical systems. In: IEEE Conference on Decision and Control, pp. 5997\u20136004. IEEE Computer Society Press (2009)","DOI":"10.1109\/CDC.2009.5399536"},{"key":"6_CR36","unstructured":"Wongpiromsarn, T., Topcu, U., Murray, R.M.: Automatic synthesis of robust embedded control software. In: AAAI Spring Symposium on Embedded Reasoning: Intelligence in Embedded Systems (2010)"},{"key":"6_CR37","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, pp. 101\u2013110. ACM (2010)","DOI":"10.1145\/1755952.1755968"}],"container-title":["Lecture Notes in Computer Science","Mathematical Foundations of Computer Science 2013"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-40313-2_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T22:10:24Z","timestamp":1558303824000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-40313-2_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642403125","9783642403132"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-40313-2_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}