{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:52:08Z","timestamp":1740099128556,"version":"3.37.3"},"publisher-location":"Cham","reference-count":42,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030001506"},{"type":"electronic","value":"9783030001513"}],"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:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-030-00151-3_14","type":"book-chapter","created":{"date-parts":[[2018,8,25]],"date-time":"2018-08-25T09:54:31Z","timestamp":1535190871000},"page":"235-251","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Duality-Based Nested Controller Synthesis from STL Specifications for Stochastic Linear Systems"],"prefix":"10.1007","author":[{"given":"Susmit","family":"Jha","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sunny","family":"Raj","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sumit Kumar","family":"Jha","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Natarajan","family":"Shankar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,8,26]]},"reference":[{"issue":"11","key":"14_CR1","doi-asserted-by":"publisher","first-page":"2724","DOI":"10.1016\/j.automatica.2008.03.027","volume":"44","author":"A Abate","year":"2008","unstructured":"Abate, A., Prandini, M., Lygeros, J., Sastry, S.: Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems. Automatica 44(11), 2724\u20132734 (2008)","journal-title":"Automatica"},{"key":"14_CR2","doi-asserted-by":"crossref","unstructured":"Akametalu, A.K., Fisac, J.F., Gillula, J.H., Kaynama, S., Zeilinger, M.N., Tomlin, C.J.: Reachability-based safe learning with Gaussian processes. In: 53rd IEEE Conference on Decision and Control, pp. 1424\u20131431. IEEE (2014)","DOI":"10.1109\/CDC.2014.7039601"},{"key":"14_CR3","unstructured":"Bellman, R., Bellman, R.E., Bellman, R.E.: Introduction to the Mathematical Theory of Control Processes, vol. 2. IMA (1971)"},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"Berkenkamp, F., Schoellig, A.P.: Safe and robust learning control with Gaussian processes. In: 2015 European Control Conference (ECC), pp. 2496\u20132501. IEEE (2015)","DOI":"10.1109\/ECC.2015.7330913"},{"issue":"11","key":"14_CR5","doi-asserted-by":"publisher","first-page":"1747","DOI":"10.1016\/S0005-1098(99)00113-2","volume":"35","author":"F Blanchini","year":"1999","unstructured":"Blanchini, F.: Set invariance in control. Automatica 35(11), 1747\u20131767 (1999)","journal-title":"Automatica"},{"key":"14_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-319-26287-1_2","volume-title":"Hardware and Software: Verification and Testing","author":"S Bogomolov","year":"2015","unstructured":"Bogomolov, S., Schilling, C., Bartocci, E., Batt, G., Kong, H., Grosu, R.: Abstraction-based parameter synthesis for multiaffine systems. In: Piterman, N. (ed.) HVC 2015. LNCS, vol. 9434, pp. 19\u201335. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-26287-1_2"},{"key":"14_CR7","doi-asserted-by":"publisher","DOI":"10.1137\/1.9781611970777","volume-title":"Linear Matrix Inequalities in System and Control Theory","author":"S Boyd","year":"1994","unstructured":"Boyd, S., El Ghaoui, L., Feron, E., Balakrishnan, V.: Linear Matrix Inequalities in System and Control Theory, vol. 15. SIAM, Philadelphia (1994)"},{"key":"14_CR8","doi-asserted-by":"crossref","DOI":"10.1201\/9781420008548","volume-title":"Stochastic Hybrid Systems","author":"CG Cassandras","year":"2006","unstructured":"Cassandras, C.G., Lygeros, J.: Stochastic Hybrid Systems, vol. 24. CRC Press, Boca Raton (2006)"},{"key":"14_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/978-3-319-19249-9_14","volume-title":"FM 2015: Formal Methods","author":"T Dang","year":"2015","unstructured":"Dang, T., Dreossi, T., Piazza, C.: Parameter synthesis through temporal logic specifications. In: Bj\u00f8rner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 213\u2013230. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-19249-9_14"},{"key":"14_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/978-3-642-15297-9_9","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"A Donz\u00e9","year":"2010","unstructured":"Donz\u00e9, A., Maler, O.: Robust satisfaction of temporal logic over real-valued signals. In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol. 6246, pp. 92\u2013106. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15297-9_9"},{"key":"14_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-540-88387-6_14","volume-title":"Automated Technology for Verification and Analysis","author":"A Eggers","year":"2008","unstructured":"Eggers, A., Fr\u00e4nzle, M., Herde, C.: SAT modulo ODE: a direct SAT approach to hybrid systems. In: Cha, S.S., Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol. 5311, pp. 171\u2013185. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-88387-6_14"},{"issue":"2","key":"14_CR12","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1016\/j.automatica.2008.08.008","journal-title":"Automatica"},{"issue":"42","key":"14_CR13","doi-asserted-by":"publisher","first-page":"4262","DOI":"10.1016\/j.tcs.2009.06.021","volume":"410","author":"GE Fainekos","year":"2009","unstructured":"Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic specifications for continuous-time signals. Theor. Comput. Sci. 410(42), 4262\u20134291 (2009)","journal-title":"Theor. Comput. Sci."},{"key":"14_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_19","volume-title":"Computer Aided Verification","author":"C Fan","year":"2018","unstructured":"Fan, C., Mathur, U., Mitra, S., Viswanathan, M.: Controller synthesis made real: reach-avoid specifications and linear dynamics. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_19"},{"key":"14_CR15","doi-asserted-by":"crossref","DOI":"10.2307\/j.ctvcm4hws","volume-title":"Nonlinear Dynamical Systems and Control: A Lyapunov-Based Approach","author":"WM Haddad","year":"2011","unstructured":"Haddad, W.M., Chellaboina, V.: Nonlinear Dynamical Systems and Control: A Lyapunov-Based Approach. Princeton University Press, Princeton (2011)"},{"key":"14_CR16","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: 2015 54th IEEE Conference on Decision and Control (CDC), pp. 7434\u20137439, December 2015","DOI":"10.1109\/CDC.2015.7403394"},{"key":"14_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/978-3-319-40648-0_10","volume-title":"NASA Formal Methods","author":"S Jha","year":"2016","unstructured":"Jha, S., Raman, V.: Automated synthesis of safe autonomous vehicle control under perception uncertainty. In: Rayadurgam, S., Tkachuk, O. (eds.) NFM 2016. LNCS, vol. 9690, pp. 117\u2013132. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40648-0_10"},{"key":"14_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-319-44878-7_5","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"S Jha","year":"2016","unstructured":"Jha, S., Raman, V.: On optimal control of stochastic linear hybrid systems. In: Fr\u00e4nzle, M., Markey, N. (eds.) FORMATS 2016. LNCS, vol. 9884, pp. 69\u201384. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-44878-7_5"},{"issue":"1","key":"14_CR19","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/s10817-017-9413-9","volume":"60","author":"S Jha","year":"2018","unstructured":"Jha, S., Raman, V., Sadigh, D., Seshia, S.A.: Safe autonomy under perception uncertainty using chance-constrained temporal logic. J. Autom. Reason. 60(1), 43\u201362 (2018). https:\/\/doi.org\/10.1007\/s10817-017-9413-9","journal-title":"J. Autom. Reason."},{"issue":"5","key":"14_CR20","doi-asserted-by":"publisher","first-page":"1129","DOI":"10.1080\/0020718508961188","volume":"41","author":"J Kautsky","year":"1985","unstructured":"Kautsky, J., Nichols, N.K., Van Dooren, P.: Robust pole assignment in linear state feedback. Int. J. Control 41(5), 1129\u20131155 (1985)","journal-title":"Int. J. Control"},{"issue":"1","key":"14_CR21","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1109\/TAC.2007.914952","journal-title":"IEEE Trans. Autom. Control"},{"key":"14_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-662-46681-0_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Kong","year":"2015","unstructured":"Kong, S., Gao, S., Chen, W., Clarke, E.: dReach: $$\\delta $$-reachability analysis for hybrid systems. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 200\u2013205. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_15"},{"key":"14_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/11730637_29","volume-title":"Hybrid Systems: Computation and Control","author":"X Koutsoukos","year":"2006","unstructured":"Koutsoukos, X., Riley, D.: Computational methods for reachability analysis of stochastic hybrid systems. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC 2006. LNCS, vol. 3927, pp. 377\u2013391. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11730637_29"},{"key":"14_CR24","doi-asserted-by":"crossref","unstructured":"Liu, J., Prabhakar, P.: Switching control of dynamical systems from metric temporal logic specifications. In: IEEE International Conference on Robotics and Automation (2014)","DOI":"10.1109\/ICRA.2014.6907643"},{"key":"14_CR25","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1016\/j.enbuild.2014.03.057","volume":"77","author":"M Maasoumy","year":"2014","unstructured":"Maasoumy, M., Razmara, M., Shahbakhti, M., Vincentelli, A.S.: Handling model uncertainty in model predictive control for energy efficient buildings. Energy Build. 77, 377\u2013392 (2014). https:\/\/doi.org\/10.1016\/j.enbuild.2014.03.057 . http:\/\/www.sciencedirect.com\/science\/article\/pii\/S0378778814002771","journal-title":"Energy Build."},{"key":"14_CR26","doi-asserted-by":"crossref","unstructured":"Maasoumy, M., Sanandaji, B.M., Sangiovanni-Vincentelli, A., Poolla, K.: Model predictive control of regulation services from commercial buildings to the smart grid. In: 2014 American Control Conference (ACC), pp. 2226\u20132233. IEEE (2014)","DOI":"10.1109\/ACC.2014.6859332"},{"key":"14_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/11603009_2","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"O Maler","year":"2005","unstructured":"Maler, O., Nickovic, D., Pnueli, A.: Real time temporal logic: past, present, future. In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol. 3829, pp. 2\u201316. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11603009_2"},{"key":"14_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1007\/3-540-46430-1_27","volume-title":"Hybrid Systems: Computation and Control","author":"I Mitchell","year":"2000","unstructured":"Mitchell, I., Tomlin, C.J.: Level set methods for computation in hybrid systems. In: Lynch, N., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 310\u2013323. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-46430-1_27"},{"issue":"7","key":"14_CR29","doi-asserted-by":"publisher","first-page":"947","DOI":"10.1109\/TAC.2005.851439","volume":"50","author":"IM Mitchell","year":"2005","unstructured":"Mitchell, I.M., Bayen, A.M., Tomlin, C.J.: A time-dependent hamilton-jacobi formulation of reachable sets for continuous dynamic games. IEEE Trans. Autom. Control 50(7), 947\u2013957 (2005)","journal-title":"IEEE Trans. Autom. Control"},{"key":"14_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-85778-5_1","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"J Ouaknine","year":"2008","unstructured":"Ouaknine, J., Worrell, J.: Some recent results in metric temporal logic. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol. 5215, pp. 1\u201313. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-85778-5_1"},{"issue":"3","key":"14_CR31","first-page":"3","volume":"14","author":"L Pontryagin","year":"1959","unstructured":"Pontryagin, L.: Optimal control processes. Usp. Mat. Nauk 14(3), 3\u201320 (1959)","journal-title":"Usp. Mat. Nauk"},{"key":"14_CR32","doi-asserted-by":"crossref","unstructured":"Prabhakar, P., Garc\u00eda Soto, M.: Formal synthesis of stabilizing controllers for switched systems. In: Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control, HSCC 2017, pp. 111\u2013120. ACM, New York (2017). http:\/\/doi.acm.org\/10.1145\/3049797.3049822","DOI":"10.1145\/3049797.3049822"},{"issue":"8","key":"14_CR33","doi-asserted-by":"publisher","first-page":"1415","DOI":"10.1109\/TAC.2007.902736","volume":"52","author":"S Prajna","year":"2007","unstructured":"Prajna, S., Jadbabaie, A., Pappas, G.J.: A framework for worst-case and stochastic safety verification using barrier certificates. IEEE Trans. Autom. Control 52(8), 1415\u20131428 (2007)","journal-title":"IEEE Trans. Autom. Control"},{"key":"14_CR34","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1201\/9781420008548.ch5","volume":"24","author":"M Prandini","year":"2006","unstructured":"Prandini, M., Hu, J.: Stochastic reachability: theory and numerical approximation. Stochast. Hybrid Syst. Autom. Control Eng. Ser. 24, 107\u2013138 (2006)","journal-title":"Stochast. Hybrid Syst. Autom. Control Eng. Ser."},{"key":"14_CR35","doi-asserted-by":"publisher","unstructured":"Raman, V., Donz, A., Maasoumy, M., Murray, R.M., Sangiovanni-Vincentelli, A., Seshia, S.A.: Model predictive control with signal temporal logic specifications. In: 53rd IEEE Conference on Decision and Control, pp. 81\u201387, December 2014. https:\/\/doi.org\/10.1109\/CDC.2014.7039363","DOI":"10.1109\/CDC.2014.7039363"},{"key":"14_CR36","unstructured":"Sadigh, D., Kapoor, A.: Safe control under uncertainty with probabilistic signal temporal logic. In: Robotics: Science and Systems XII (2016). http:\/\/www.roboticsproceedings.org\/rss12\/p17.html"},{"key":"14_CR37","doi-asserted-by":"crossref","unstructured":"Schrmann, B., Althoff, M.: Optimal control of sets of solutions to formally guarantee constraints of disturbed linear systems. In: 2017 American Control Conference (ACC), pp. 2522\u20132529, May 2017","DOI":"10.23919\/ACC.2017.7963332"},{"issue":"4","key":"14_CR38","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1109\/37.710880","volume":"18","author":"D Seto","year":"1998","unstructured":"Seto, D., Krogh, B.H., Sha, L., Chutinan, A.: Dynamic control system upgrade using the simplex architecture. IEEE Control Syst. 18(4), 72\u201380 (1998)","journal-title":"IEEE Control Syst."},{"key":"14_CR39","doi-asserted-by":"crossref","unstructured":"Summers, S., Kamgarpour, M., Lygeros, J., Tomlin, C.: A stochastic reach-avoid problem with random obstacles. In: Proceedings of the 14th International Conference on Hybrid Systems: Computation and Control, pp. 251\u2013260. ACM (2011)","DOI":"10.1145\/1967701.1967738"},{"issue":"12","key":"14_CR40","doi-asserted-by":"publisher","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":"11","key":"14_CR41","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1109\/TAC.2012.2195811","journal-title":"IEEE Trans. Autom. Control"},{"issue":"6","key":"14_CR42","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.: Temporal logic control of discrete-time piecewise affine systems. IEEE Trans. Autom. Control 57(6), 1491\u20131504 (2012)","journal-title":"IEEE Trans. Autom. Control"}],"container-title":["Lecture Notes in Computer Science","Formal Modeling and Analysis of Timed Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-00151-3_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,22]],"date-time":"2019-10-22T19:51:26Z","timestamp":1571773886000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-00151-3_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783030001506","9783030001513"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-00151-3_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}