{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:24:26Z","timestamp":1740122666516,"version":"3.37.3"},"reference-count":33,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2016,11,25]],"date-time":"2016-11-25T00:00:00Z","timestamp":1480032000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2016,11,25]],"date-time":"2016-11-25T00:00:00Z","timestamp":1480032000000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1138996"],"award-info":[{"award-number":["CCF-1138996"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Discrete Event Dyn Syst"],"published-print":{"date-parts":[[2017,6]]},"DOI":"10.1007\/s10626-016-0232-7","type":"journal-article","created":{"date-parts":[[2016,11,25]],"date-time":"2016-11-25T17:26:07Z","timestamp":1480094767000},"page":"371-405","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Automated generation of dynamics-based runtime certificates for high-level control"],"prefix":"10.1007","volume":"27","author":[{"given":"Jonathan","family":"DeCastro","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"R\u00fcdiger","family":"Ehlers","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matthias","family":"Rungger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ay\u00e7a","family":"Balkan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hadas","family":"Kress-Gazit","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,11,25]]},"reference":[{"key":"#cr-split#-232_CR1.1","unstructured":"Alur R, Moarref S, Topcu U (2013) Counter-strategy guided refinement of gr"},{"key":"#cr-split#-232_CR1.2","unstructured":"(1) temporal logic specifications. In: Formal methods in computer-aided design (FMCAD 2013), pp 26-33"},{"key":"232_CR2","doi-asserted-by":"crossref","unstructured":"Bhatia A, Kavraki L, Vardi M (2010) Sampling-based motion planning with temporal goals. In: IEEE International conference on robotics and automation (ICRA 2010). IEEE, pp 2689\u20132696","DOI":"10.1109\/ROBOT.2010.5509503"},{"key":"232_CR3","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1007\/978-3-642-14295-6_37","volume-title":"RATSY \u2013 a new requirements analysis tool with synthesis","author":"R Bloem","year":"2010","unstructured":"Bloem R, Cimatti A, Greimel K, Hofferek G, K\u00f6nighofer R, Roveri M, Schuppan V, Seeber R (2010) RATSY \u2013 a new requirements analysis tool with synthesis. Springer Berlin Heidelberg, Berlin Heidelberg, pp 425\u2013429 doi:\n                    10.1007\/978-3-642-14295-6_37"},{"issue":"3","key":"232_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 (2012) Synthesis of reactive (1) designs. J Comput Syst Sci 78(3):911\u2013938","journal-title":"J Comput Syst Sci"},{"key":"232_CR5","unstructured":"DeCastro JA, Ehlers R, Rungger M, Balkan A, Tabuada P, Kress-Gazit H (2014) Dynamics-based reactive synthesis and automated revisions for high-level robot control. CoRR arXiv:\n                    1410.6375"},{"key":"232_CR6","doi-asserted-by":"publisher","unstructured":"DeCastro JA, Kress-Gazit H (2015) Synthesis of nonlinear continuous controllers for verifiably-correct high-level, reactive behaviors. Int J Robot Res 34(3):378\u2013394. doi:\n                    10.1177\/0278364914557736\n                    \n                  . \n                    http:\/\/ijr.sagepub.com\/content\/34\/3\/378","DOI":"10.1177\/0278364914557736"},{"key":"232_CR7","doi-asserted-by":"crossref","unstructured":"DeCastro JA, Kress-Gazit H (2016) Nonlinear controller synthesis and automatic workspace partitioning for reactive high-level behaviors. In: Proceedings of the 19th ACM international conference on hybrid systems: computation and control (HSCC). Vienna","DOI":"10.1145\/2883817.2883832"},{"key":"232_CR8","doi-asserted-by":"publisher","unstructured":"Ehlers R, Raman V (2016) Slugs: extensible GR(1) synthesis. In: Computer aided verification - 28th international conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II, pp 333\u2013339. doi:\n                    10.1007\/978-3-319-41540-6_18","DOI":"10.1007\/978-3-319-41540-6_18"},{"key":"232_CR9","doi-asserted-by":"crossref","unstructured":"Fainekos GE (2011) Revising temporal logic specifications for motion planning. In: Proceedings of the IEEE conference on robotics and automation","DOI":"10.1109\/ICRA.2011.5979895"},{"key":"232_CR10","doi-asserted-by":"publisher","unstructured":"Fainekos GE, Girard A, Kress-Gazit H, Pappas GJ (2009) Temporal logic motion planning for dynamic robots. Automatica 45(2):343\u2013352. doi:\n                    10.1016\/j.automatica.2008.08.008","DOI":"10.1016\/j.automatica.2008.08.008"},{"issue":"1","key":"232_CR11","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1109\/TAC.2009.2034922","volume":"55","author":"A Girard","year":"2010","unstructured":"Girard A, Pola G, Tabuada P (2010) Approximately bisimilar symbolic models for incrementally stable switched systems. IEEE Trans Autom Control 55(1):116\u2013126","journal-title":"IEEE Trans Autom Control"},{"key":"232_CR12","doi-asserted-by":"crossref","unstructured":"Kloetzer M, Belta C (2008) Dealing with nondeterminism in symbolic control. In: Egerstedt M, Mishra B (eds) Hybrid systems: computation and control, 11th international workshop (HSCC 2008), lecture notes in computer science, vol 4981. Springer, pp 287\u2013300","DOI":"10.1007\/978-3-540-78929-1_21"},{"key":"232_CR13","doi-asserted-by":"crossref","unstructured":"K\u00f6nighofer R, Hofferek G, Bloem R (2009) Debugging formal specifications using simple counterstrategies. In: Proceedings of 9th International conference on formal methods in computer-aided design, FMCAD 2009, pp 152\u2013159","DOI":"10.1109\/FMCAD.2009.5351127"},{"issue":"6","key":"232_CR14","doi-asserted-by":"publisher","first-page":"1370","DOI":"10.1109\/TRO.2009.2030225","volume":"25","author":"H Kress-Gazit","year":"2009","unstructured":"Kress-Gazit H, Fainekos GE, Pappas GJ (2009) Temporal logic based reactive mission and motion planning. IEEE Trans Robot 25(6):1370\u20131381","journal-title":"IEEE Trans Robot"},{"key":"232_CR15","doi-asserted-by":"crossref","unstructured":"Li W, Dworkin L, Seshia SA (2011) Mining assumptions for synthesis. In: 9th IEEE\/ACM International conference on formal methods and models for Codesign, MEMOCODE 2011, pp 43\u201350","DOI":"10.1109\/MEMCOD.2011.5970509"},{"key":"232_CR16","doi-asserted-by":"crossref","unstructured":"Li W, Sadigh D, Sastry SS, Seshia SA (2014) Synthesis for human-in-the-loop control systems. In: Tools and algorithms for the construction and analysis of systems - 20th international conference, TACAS 2014, pp 470\u2013484","DOI":"10.1007\/978-3-642-54862-8_40"},{"key":"232_CR17","doi-asserted-by":"publisher","unstructured":"Liu J, Ozay N (2014) Abstraction, discretization, and robustness in temporal logic control of dynamical systems. In: Proc. of the 17th int. conf. on hybrid systems: computation and control (HSCC\u201914), pp 293\u2013302. doi:\n                    10.1145\/2562059.2562137","DOI":"10.1145\/2562059.2562137"},{"issue":"7","key":"232_CR18","doi-asserted-by":"publisher","first-page":"1771","DOI":"10.1109\/TAC.2013.2246095","volume":"58","author":"J Liu","year":"2013","unstructured":"Liu J, Ozay N, Topcu U, Murray RM (2013) Synthesis of reactive switching protocols from temporal logic specifications. IEEE Trans Automat Contr 58 (7):1771\u20131785","journal-title":"IEEE Trans Automat Contr"},{"key":"232_CR19","doi-asserted-by":"crossref","unstructured":"Maly M, Lahijanian M, Kavraki L E, Kress-Gazit H, Vardi M Y (2013) Iterative temporal motion planning for hybrid systems in partially unknown environments. In: ACM International conference on hybrid systems: computation and control (HSCC). ACM, Philadelphia, pp 353\u2013362","DOI":"10.1145\/2461328.2461380"},{"key":"232_CR20","doi-asserted-by":"publisher","unstructured":"Nilsson P, Ozay N (2014) Incremental synthesis of switching protocols via abstraction refinement. In: 53rd IEEE conference on decision and control, CDC 2014, Los Angeles, CA, USA, December 15-17, 2014. IEEE, pp 6246\u20136253. doi:\n                    10.1109\/CDC.2014.7040368","DOI":"10.1109\/CDC.2014.7040368"},{"issue":"10","key":"232_CR21","doi-asserted-by":"publisher","first-page":"2508","DOI":"10.1016\/j.automatica.2008.02.021","volume":"44","author":"G Pola","year":"2008","unstructured":"Pola G, Girard A, Tabuada P (2008) Approximately bisimilar symbolic models for nonlinear control systems. Automatica 44(10):2508\u20132516","journal-title":"Automatica"},{"key":"232_CR22","doi-asserted-by":"crossref","unstructured":"Raman V, Kress-Gazit H (2013) Towards minimal explanations of unsynthesizability for high-level robot behaviors. In: Proc. of the IEEE\/RSJ int. conf. on intelligent robots and systems (IROS 2013)","DOI":"10.1109\/IROS.2013.6696436"},{"key":"232_CR23","doi-asserted-by":"crossref","unstructured":"Raman V, Piterman N, Kress-Gazit H (2013) Provably correct continuous control for high-level robot behaviors with actions of arbitrary execution durations. In: IEEE International conference on robotics and automation. Karlsruhe, pp 4075\u20134081","DOI":"10.1109\/ICRA.2013.6631152"},{"issue":"11","key":"232_CR24","doi-asserted-by":"publisher","first-page":"2583","DOI":"10.1109\/TAC.2011.2118950","volume":"56","author":"G Rei\u00dfig","year":"2011","unstructured":"Rei\u00dfig G (2011) Computing abstractions of nonlinear systems. IEEE Trans Autom Control 56(11):2583\u20132598","journal-title":"IEEE Trans Autom Control"},{"issue":"12","key":"232_CR25","doi-asserted-by":"publisher","first-page":"1862","DOI":"10.1109\/TAC.2006.886494","volume":"51","author":"P Tabuada","year":"2006","unstructured":"Tabuada P, Pappas GJ (2006) Linear time logic control of discrete-time linear systems. IEEE Trans Autom Contr 51(12):1862\u20131877","journal-title":"IEEE Trans Autom Contr"},{"key":"232_CR26","doi-asserted-by":"publisher","unstructured":"Tarjan R (1972) Depth-first search and linear graph algorithms. SIAM J Comput 1(2):146\u2013160. doi:\n                    10.1137\/0201010","DOI":"10.1137\/0201010"},{"key":"232_CR27","doi-asserted-by":"publisher","unstructured":"Tumova J, Yordanov B, Belta C, Cerna I, Barnat J (2010) A symbolic approach to controlling piecewise affine systems. In: 49th IEEE Conference on decision and control (CDC), pp 4230\u20134235. doi:\n                    10.1109\/CDC.2010.5717316\n                    \n                  . \n                    pdf\/cdc10b.pdf","DOI":"10.1109\/CDC.2010.5717316"},{"key":"232_CR28","doi-asserted-by":"crossref","unstructured":"Vardi MY (1996) An automata-theoretic approach to linear temporal logic. In: Logics for concurrency. Springer, pp 238\u2013266","DOI":"10.1007\/3-540-60915-6_6"},{"key":"232_CR29","doi-asserted-by":"crossref","unstructured":"Wolff E M, Topcu U, Murray RM (2013) Automaton-guided controller synthesis for nonlinear systems with temporal logic. In: Proc. of the IEEE\/RSJ int. conf. on intelligent robots and systems (IROS 2013)","DOI":"10.1109\/IROS.2013.6696978"},{"key":"232_CR30","doi-asserted-by":"crossref","unstructured":"Wongpiromsarn T, Topcu U, Murray RM (2010) Receding horizon control for temporal logic specifications. In: Proc. of the 13th Int. conf. on hybrid systems: computation and control (HSCC\u201910)","DOI":"10.1145\/1755952.1755968"},{"issue":"6","key":"232_CR31","doi-asserted-by":"publisher","first-page":"1491","DOI":"10.1109\/TAC.2011.2178328","volume":"57","author":"B Yordanov","year":"2012","unstructured":"Yordanov B, Tumova J, Cerna I, Barnat J, Belta C (2012) Temporal logic control of discrete-time piecewise affine systems. IEEE Trans Autom Control 57 (6):1491\u20131504","journal-title":"IEEE Trans Autom Control"},{"issue":"7","key":"232_CR32","doi-asserted-by":"publisher","first-page":"1804","DOI":"10.1109\/TAC.2011.2176409","volume":"57","author":"M Zamani","year":"2012","unstructured":"Zamani M, Pola G, Mazo M, Tabuada P (2012) Symbolic models for nonlinear control systems without stability assumptions. IEEE Trans Autom Control 57(7):1804\u20131809","journal-title":"IEEE Trans Autom Control"}],"container-title":["Discrete Event Dynamic Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10626-016-0232-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10626-016-0232-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10626-016-0232-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,17]],"date-time":"2020-05-17T15:03:06Z","timestamp":1589727786000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10626-016-0232-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,11,25]]},"references-count":33,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2017,6]]}},"alternative-id":["232"],"URL":"https:\/\/doi.org\/10.1007\/s10626-016-0232-7","relation":{},"ISSN":["0924-6703","1573-7594"],"issn-type":[{"type":"print","value":"0924-6703"},{"type":"electronic","value":"1573-7594"}],"subject":[],"published":{"date-parts":[[2016,11,25]]},"assertion":[{"value":"11 February 2016","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"3 November 2016","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"25 November 2016","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}