{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,21]],"date-time":"2026-02-21T20:29:55Z","timestamp":1771705795206,"version":"3.50.1"},"publisher-location":"Cham","reference-count":41,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319961446","type":"print"},{"value":"9783319961453","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-96145-3_19","type":"book-chapter","created":{"date-parts":[[2018,7,20]],"date-time":"2018-07-20T18:25:55Z","timestamp":1532111155000},"page":"347-366","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":20,"title":["Controller Synthesis Made Real: Reach-Avoid Specifications and Linear Dynamics"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4671-233X","authenticated-orcid":false,"given":"Chuchu","family":"Fan","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7610-0660","authenticated-orcid":false,"given":"Umang","family":"Mathur","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7082-5516","authenticated-orcid":false,"given":"Sayan","family":"Mitra","sequence":"additional","affiliation":[]},{"given":"Mahesh","family":"Viswanathan","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,7,18]]},"reference":[{"key":"19_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/978-3-540-71493-4_4","volume-title":"Hybrid Systems: Computation and Control","author":"A Abate","year":"2007","unstructured":"Abate, A., Amin, S., Prandini, M., Lygeros, J., Sastry, S.: Computational approaches to reachability analysis of stochastic hybrid systems. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol. 4416, pp. 4\u201317. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71493-4_4"},{"key":"19_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"462","DOI":"10.1007\/978-3-319-63387-9_23","volume-title":"Computer Aided Verification","author":"A Abate","year":"2017","unstructured":"Abate, A., et al.: Automated formal synthesis of digital controllers for state-space physical plants. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 462\u2013482. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_23"},{"key":"19_CR3","volume-title":"A Linear Systems Primer","author":"PJ Antsaklis","year":"2007","unstructured":"Antsaklis, P.J., Michel, A.N.: A Linear Systems Primer, vol. 1. Birkh\u00e4user Boston, Cambridge (2007)"},{"key":"19_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C Barrett","year":"2011","unstructured":"Barrett, C., et al.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171\u2013177. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_14"},{"key":"19_CR5","doi-asserted-by":"crossref","unstructured":"Boyd, S., Vandenberghe, L.: Convex Optimization (2004)","DOI":"10.1017\/CBO9780511804441"},{"key":"19_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"19_CR7","doi-asserted-by":"crossref","unstructured":"Ding, J., Tomlin, C.J.: Robust reach-avoid controller synthesis for switched nonlinear systems. In: Proceedings of the 49th IEEE Conference on Decision and Control, CDC 2010, 15\u201317 December 2010, Atlanta, Georgia, USA, pp. 6481\u20136486 (2010)","DOI":"10.1109\/CDC.2010.5717115"},{"key":"19_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"737","DOI":"10.1007\/978-3-319-08867-9_49","volume-title":"Computer Aided Verification","author":"B Dutertre","year":"2014","unstructured":"Dutertre, B.: Yices\u00a02.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737\u2013744. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_49"},{"key":"19_CR9","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1016\/j.automatica.2016.03.016","volume":"70","author":"PM Esfahani","year":"2016","unstructured":"Esfahani, P.M., Chatterjee, D., Lygeros, J.: The stochastic reach-avoid problem and set characterization for diffusions. Automatica 70, 43\u201356 (2016)","journal-title":"Automatica"},{"issue":"2","key":"19_CR10","doi-asserted-by":"crossref","first-page":"343","DOI":"10.1016\/j.automatica.2008.08.008","volume":"45","author":"GE Fainekos","year":"2009","unstructured":"Fainekos, G.E., Girard, A., Kress-Gazit, H., Pappas, G.J.: Temporal logic motion planning for dynamic robots. Automatica 45(2), 343\u2013352 (2009)","journal-title":"Automatica"},{"key":"19_CR11","doi-asserted-by":"crossref","unstructured":"Fainekos, G.E., Kress-Gazit, H., Pappas, G.J.: Hybrid controllers for path planning: a temporal logic approach. In: 2005 44th IEEE Conference on Decision and Control, and 2005 European Control Conference, CDC-ECC 2005, pp. 4885\u20134890. IEEE (2005)","DOI":"10.1109\/CDC.2005.1582935"},{"key":"19_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-540-24743-2_22","volume-title":"Hybrid Systems: Computation and Control","author":"A Fehnker","year":"2004","unstructured":"Fehnker, A., Ivan\u010di\u0107, F.: Benchmarks for hybrid systems verification. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 326\u2013341. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24743-2_22"},{"key":"19_CR13","doi-asserted-by":"crossref","unstructured":"Filippidis, I., Dathathri, S., Livingston, S.C., Ozay, N., Murray, R.M.: Control design for hybrid systems with tulip: the temporal logic planning toolbox. In: 2016 IEEE Conference on Control Applications, CCA 2016, Buenos Aires, Argentina, 19\u201322 September 2016, pp. 1030\u20131041 (2016)","DOI":"10.1109\/CCA.2016.7587949"},{"key":"19_CR14","doi-asserted-by":"crossref","unstructured":"Fisac, J.F., Chen, M., Tomlin, C.J., Sastry, S.S.: Reach-avoid problems with time-varying dynamics, targets and constraints. In: Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, HSCC 2015, Seattle, WA, USA, 14\u201316 April 2015, pp. 11\u201320 (2015)","DOI":"10.1145\/2728606.2728612"},{"issue":"5","key":"19_CR15","doi-asserted-by":"crossref","first-page":"947","DOI":"10.1016\/j.automatica.2012.02.037","volume":"48","author":"A Girard","year":"2012","unstructured":"Girard, A.: Controller synthesis for safety and reachability via approximate bisimulation. Automatica 48(5), 947\u2013953 (2012)","journal-title":"Automatica"},{"issue":"5","key":"19_CR16","doi-asserted-by":"crossref","first-page":"1163","DOI":"10.1109\/TAC.2013.2295664","volume":"59","author":"EA Gol","year":"2014","unstructured":"Gol, E.A., Lazar, M., Belta, C.: Language-guided controller synthesis for linear systems. IEEE Trans. Autom. Control 59(5), 1163\u20131176 (2014)","journal-title":"IEEE Trans. Autom. Control"},{"key":"19_CR17","volume-title":"Linear Systems Theory","author":"JP Hespanha","year":"2009","unstructured":"Hespanha, J.P.: Linear Systems Theory. Princeton University Press, Princeton (2009)"},{"key":"19_CR18","doi-asserted-by":"crossref","unstructured":"Huang, Z., Wang, Y., Mitra, S., Dullerud, G.E., Chaudhuri, S.: Controller synthesis with inductive proofs for piecewise linear systems: an SMT-based algorithm. In: 54th IEEE Conference on Decision and Control, CDC 2015, Osaka, Japan, 15\u201318 December 2015, pp. 7434\u20137439 (2015)","DOI":"10.1109\/CDC.2015.7403394"},{"key":"19_CR19","doi-asserted-by":"crossref","unstructured":"Jha, S., Seshia, S.A., Tiwari, A.: Synthesis of optimal switching logic for hybrid systems. In: Proceedings of the 11th International Conference on Embedded Software, EMSOFT 2011, Part of the Seventh Embedded Systems Week, ESWeek 2011, Taipei, Taiwan, 9\u201314 October 2011, pp. 107\u2013116 (2011)","DOI":"10.1145\/2038642.2038660"},{"issue":"1","key":"19_CR20","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1109\/TAC.2007.914952","volume":"53","author":"M Kloetzer","year":"2008","unstructured":"Kloetzer, M., Belta, C.: A fully automated framework for control of linear systems from temporal logic specifications. IEEE Trans. Autom. Control 53(1), 287\u2013297 (2008)","journal-title":"IEEE Trans. Autom. Control"},{"key":"19_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/3-540-45351-2_28","volume-title":"Hybrid Systems: Computation and Control","author":"TJ Koo","year":"2001","unstructured":"Koo, T.J., Pappas, G.J., Sastry, S.: Mode switching synthesis for reachability specifications. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A. (eds.) HSCC 2001. LNCS, vol. 2034, pp. 333\u2013346. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45351-2_28"},{"issue":"6","key":"19_CR22","doi-asserted-by":"crossref","first-page":"1370","DOI":"10.1109\/TRO.2009.2030225","volume":"25","author":"H Kress-Gazit","year":"2009","unstructured":"Kress-Gazit, H., Fainekos, G.E., Pappas, G.J.: Temporal logic based reactive mission and motion planning. IEEE Trans. Robot. 25(6), 1370\u20131381 (2009)","journal-title":"IEEE Trans. Robot."},{"key":"19_CR23","doi-asserted-by":"crossref","unstructured":"Kress-Gazit, H., Lahijanian, M., Raman, V.: Synthesis for robots: guarantees and feedback for robot behavior. Ann. Rev. Control Robot. Auton. Syst. 1(1) (2018)","DOI":"10.1146\/annurev-control-060117-104838"},{"issue":"1","key":"19_CR24","doi-asserted-by":"crossref","first-page":"26","DOI":"10.1109\/TAC.2006.887900","volume":"52","author":"AA Kurzhanskiy","year":"2007","unstructured":"Kurzhanskiy, A.A., Varaiya, P.: Ellipsoidal techniques for reachability analysis of discrete-time linear systems. IEEE Trans. Autom. Control 52(1), 26\u201338 (2007)","journal-title":"IEEE Trans. Autom. Control"},{"issue":"7","key":"19_CR25","doi-asserted-by":"crossref","first-page":"1771","DOI":"10.1109\/TAC.2013.2246095","volume":"58","author":"J Liu","year":"2013","unstructured":"Liu, J., Ozay, N., Topcu, U., Murray, R.M.: Synthesis of reactive switching protocols from temporal logic specifications. IEEE Trans. Autom. Control 58(7), 1771\u20131785 (2013)","journal-title":"IEEE Trans. Autom. Control"},{"key":"19_CR26","unstructured":"Majumdar, R., Mallik, K., Schmuck, A.-K.: Compositional synthesis of finite state abstractions. CoRR, abs\/1612.08515 (2016)"},{"key":"19_CR27","doi-asserted-by":"crossref","unstructured":"Mouelhi, S., Girard, A., G\u00f6ssler, G.: Cosyma: a tool for controller synthesis using multi-scale abstractions. In: Proceedings of The 16th International Conference on Hybrid Systems: Computation and Control, HSCC 2013, pp. 83\u201388, New York. ACM (2013)","DOI":"10.1145\/2461328.2461343"},{"issue":"2","key":"19_CR28","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1109\/TCSII.2006.886888","volume":"54\u2013II","author":"MA Rami","year":"2007","unstructured":"Rami, M.A., Tadeo, F.: Controller synthesis for positive linear systems with bounded controls. IEEE Trans. Circuits Syst. 54\u2013II(2), 151\u2013155 (2007)","journal-title":"IEEE Trans. Circuits Syst."},{"key":"19_CR29","doi-asserted-by":"crossref","unstructured":"Ravanbakhsh, H., Sankaranarayanan, S.: Robust controller synthesis of switched systems using counterexample guided framework. In: Proceedings of the 13th International Conference on Embedded Software, EMSOFT 2016, pp. 8:1\u20138:10, New York. ACM (2016)","DOI":"10.1145\/2968478.2968485"},{"key":"19_CR30","doi-asserted-by":"crossref","unstructured":"Roy, P., Tabuada, P., Majumdar, R.: Pessoa 2.0: a controller synthesis tool for cyber-physical systems. In: Proceedings of the 14th International Conference on Hybrid Systems: Computation and Control, HSCC 2011, pp. 315\u2013316, New York. ACM (2011)","DOI":"10.1145\/1967701.1967748"},{"key":"19_CR31","doi-asserted-by":"crossref","unstructured":"Rungger, M, Zamani, M.: SCOTS: a tool for the synthesis of symbolic controllers. In: Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, HSCC 2016, pp. 99\u2013104, New York. ACM (2016)","DOI":"10.1145\/2883817.2883834"},{"key":"19_CR32","doi-asserted-by":"crossref","unstructured":"Sch\u00fcrmann, B., Althoff, M.: Optimal control of sets of solutions to formally guarantee constraints of disturbed linear systems. In: 2017 American Control Conference, ACC 2017, Seattle, WA, USA, 24\u201326 May 2017, pp. 2522\u20132529 (2017)","DOI":"10.23919\/ACC.2017.7963332"},{"key":"19_CR33","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-0224-5","volume-title":"Verification and Control of Hybrid Systems - A Symbolic Approach","author":"P Tabuada","year":"2009","unstructured":"Tabuada, P.: Verification and Control of Hybrid Systems - A Symbolic Approach. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-1-4419-0224-5"},{"issue":"12","key":"19_CR34","doi-asserted-by":"crossref","first-page":"1862","DOI":"10.1109\/TAC.2006.886494","volume":"51","author":"P Tabuada","year":"2006","unstructured":"Tabuada, P., Pappas, G.J.: Linear time logic control of discrete-time linear systems. IEEE Trans. Autom. Control 51(12), 1862\u20131877 (2006)","journal-title":"IEEE Trans. Autom. Control"},{"issue":"6","key":"19_CR35","doi-asserted-by":"crossref","first-page":"519","DOI":"10.1007\/s10009-010-0172-8","volume":"13","author":"A Taly","year":"2011","unstructured":"Taly, A., Gulwani, S., Tiwari, A.: Synthesizing switching logic using constraint solving. STTT 13(6), 519\u2013535 (2011)","journal-title":"STTT"},{"key":"19_CR36","unstructured":"Tran, H.D., Nguyen, L.V., Johnson, T.T.: Large-scale linear systems from order-reduction. In: ARCH@CPSWeek 2016, 3rd International Workshop on Applied Verification for Continuous and Hybrid Systems, Vienna, Austria, pp. 60\u201367 (2016)"},{"key":"19_CR37","doi-asserted-by":"crossref","unstructured":"Wong, K.W., Finucane, C., Kress-Gazit, H.: Provably-correct robot control with LTLMoP, OMPL and ROS. In: 2013 IEEE\/RSJ International Conference on Intelligent Robots and Systems, Tokyo, Japan, 3\u20137 November 2013, p. 2073 (2013)","DOI":"10.1109\/IROS.2013.6696636"},{"issue":"11","key":"19_CR38","doi-asserted-by":"crossref","first-page":"2817","DOI":"10.1109\/TAC.2012.2195811","volume":"57","author":"T Wongpiromsarn","year":"2012","unstructured":"Wongpiromsarn, T., Topcu, U., Murray, R.M.: Receding horizon temporal logic planning. IEEE Trans. Autom. Control 57(11), 2817\u20132830 (2012)","journal-title":"IEEE Trans. Autom. Control"},{"key":"19_CR39","doi-asserted-by":"crossref","unstructured":"Wongpiromsarn, T., Topcu, U., Ozay, N., Xu, H., Murray, R.M.: TuLiP: a software toolbox for receding horizon temporal logic planning. In: Proceedings of the 14th International Conference on Hybrid Systems: Computation and Control, HSCC 2011, pp. 313\u2013314, New York. ACM (2011)","DOI":"10.1145\/1967701.1967747"},{"issue":"6","key":"19_CR40","doi-asserted-by":"crossref","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.: Temporal logic control of discrete-time piecewise affine systems. IEEE Trans. Autom. Control 57(6), 1491\u20131504 (2012)","journal-title":"IEEE Trans. Autom. Control"},{"key":"19_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/978-3-642-39698-4_22","volume-title":"Theories of Programming and Formal Methods","author":"H Zhao","year":"2013","unstructured":"Zhao, H., Zhan, N., Kapur, D.: Synthesizing switching controllers for hybrid systems by generating invariants. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) Theories of Programming and Formal Methods. LNCS, vol. 8051, pp. 354\u2013373. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39698-4_22"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-96145-3_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,20]],"date-time":"2019-10-20T23:32:25Z","timestamp":1571614345000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-96145-3_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319961446","9783319961453"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-96145-3_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}