{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,20]],"date-time":"2025-09-20T19:30:48Z","timestamp":1758396648329,"version":"3.41.0"},"publisher-location":"Cham","reference-count":42,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319240206"},{"type":"electronic","value":"9783319240213"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-24021-3_32","type":"book-chapter","created":{"date-parts":[[2015,9,3]],"date-time":"2015-09-03T07:58:36Z","timestamp":1441267116000},"page":"440-456","source":"Crossref","is-referenced-by-count":7,"title":["Safety Verification of Hybrid Systems Using Certified Multiple Lyapunov-Like Functions"],"prefix":"10.1007","author":[{"given":"Zhikun","family":"She","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dan","family":"Song","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Meilun","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,11,12]]},"reference":[{"key":"32_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.-H., Nicollin, X., Oliviero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theoretical Computer Science 138, 3\u201334 (1995)","DOI":"10.1016\/0304-3975(94)00202-T"},{"key":"32_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., Dang, T., Ivanc\u0306i\u0107, F.: Counterexample-guided predicate abstraction of hybrid systems. Theoretical Computer Science 354, 250\u2013271 (2006)","DOI":"10.1016\/j.tcs.2005.11.026"},{"key":"32_CR3","doi-asserted-by":"crossref","unstructured":"Anai, H., Weispfenning, V.: Reach set computations using real quantifier elimination. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.) HSCC 2001. LNCS, vol. 2034, pp. 63\u201376. Springer, Heidelberg (2001)","DOI":"10.1007\/3-540-45351-2_9"},{"key":"32_CR4","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Fehnker, A., Han, Z., Krogh, B., Ouaknine, J., Stursberg, O., Theobald, M.: Abstraction and Counterexample-Guided Refinement in Model Checking of Hybrid Systems. International Journal Foundations of Computer Science 14, 583\u2013604 (2003)","DOI":"10.1142\/S012905410300190X"},{"key":"32_CR5","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Kurshan, R.P.: Computer-aided verification. IEEE Spectrum 33(6), 61\u201367 (1996)","DOI":"10.1109\/6.499951"},{"key":"32_CR6","doi-asserted-by":"crossref","unstructured":"Christoffer, S., George, J.P., Rafael, W.: Compositional safety analysis using barrier certificates. In: Proceedings of the 15th ACM International Conference on Hybrid Systems: Computation and Control, pp. 15\u201323 (2012)","DOI":"10.1145\/2185632.2185639"},{"key":"32_CR7","doi-asserted-by":"crossref","unstructured":"Chutinan, A., Krogh, B.H.: Computational techniques for hybrid system verification. IEEE Transactions on Automatic Control 48, 64\u201375 (2003)","DOI":"10.1109\/TAC.2002.806655"},{"key":"32_CR8","unstructured":"Fradkov, A.L., Yakubovich, V.A.: The S-procedure and a duality realations in nonconvex problems of quadratic programming. Vestnik Leningrad Univ. Math 5, 101\u2013109 (1979)"},{"key":"32_CR9","unstructured":"Grayson, D.R., Stillman, M.E.: Macaulay2, a software system for research in algebraic geometry. http:\/\/www.math.uiuc.edu\/Macaulay2"},{"key":"32_CR10","doi-asserted-by":"crossref","unstructured":"Le Guernic, C., Girard, A.: Reachability analysis of hybrid systems using support functions. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 540\u2013554. Springer, Heidelberg (2009)","DOI":"10.1007\/978-3-642-02658-4_40"},{"key":"32_CR11","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Tiwari, A.: Constraint-based approach for analysis of hybrid systems. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 190\u2013203. Springer, Heidelberg (2008)","DOI":"10.1007\/978-3-540-70545-1_18"},{"key":"32_CR12","unstructured":"H\u00e4rter, V., Jansson, C., Lange, M.: VSDP: a matlab toolbox for verified semidefinte-quadratic-linear programming. http:\/\/www.ti3.tuhh.de\/jansson\/vsdp\/"},{"key":"32_CR13","doi-asserted-by":"crossref","unstructured":"Huang, Z., Mitra, S.: Proofs from simulations and modular annotations. In: Proc. of the 17th International Conference on Hybrid Systems: Computation and Control, pp. 183\u2013192 (2014)","DOI":"10.1145\/2562059.2562126"},{"key":"32_CR14","doi-asserted-by":"crossref","unstructured":"Huang, Z., Fan, C., Mereacre, A., Mitra, S., Kwiatkowska, M.: Invariant verification of nonlinear hybrid automata networks of cardiac cells. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 373\u2013390. Springer, Heidelberg (2014)","DOI":"10.1007\/978-3-319-08867-9_25"},{"key":"32_CR15","unstructured":"Jones, W., Thron, W.: Continued fractions: analytic theory and applications. In: Encyclopedia of Mathematics and its Applications, vol. 11 (1980)"},{"key":"32_CR16","doi-asserted-by":"crossref","unstructured":"Kaltofen, E., Li, B., Yang, Z., Zhi, L.: Exact certification in global polynomial optimization via sums-of-squares of rational functions with rational coefficients. Journal of Symbolic Computation 47, 1\u201315 (2012)","DOI":"10.1016\/j.jsc.2011.08.002"},{"key":"32_CR17","unstructured":"Kurzhanski, A.B., Varaiya, P.: Ellipsoidal techniques for reachability analysis. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 203\u2013213. Springer, Heidelberg (2000)"},{"key":"32_CR18","doi-asserted-by":"crossref","unstructured":"Lafferriere, G., Pappas, G.J., Yovine, S.: Symbolic reachability computations for families of linear vectorfields. Journal of Symbolic Computation 32, 231\u2013253 (2001)","DOI":"10.1006\/jsco.2001.0472"},{"key":"32_CR19","doi-asserted-by":"crossref","unstructured":"Lin, W., Wu, M., Yang, Z., Zeng, Z.: Exact safety verification of hybrid systems using sums-of-squares representation. Science China Information Sciences 57(5), 1\u201313 (2014)","DOI":"10.1007\/s11432-013-4961-z"},{"key":"32_CR20","unstructured":"L\u00f6fberg, J.: Yalmip: a toolbox for modeling and optimization in MATLAB. In: Proceedings of the CACSD Conference (2004). http:\/\/control.ee.ethz.ch\/joloef\/yalmip.php"},{"key":"32_CR21","unstructured":"Parrilo, P.A.: Structured Semidefinite Programs and Semialgebraic Geometly Methods in Robustness and Optimization. Ph.D. thesis, California Institute of Technology, Pasadena (2000)"},{"key":"32_CR22","doi-asserted-by":"crossref","unstructured":"Peyrl, H., Parrilo, P.A.: Computing sum of squares decompositions with rational coefficients. Theoretical Computer Science 409, 269\u2013281 (2008)","DOI":"10.1016\/j.tcs.2008.09.025"},{"key":"32_CR23","doi-asserted-by":"crossref","unstructured":"Platzer, A., Clarke, E.M.: The image computation problem in hybrid systems model checking. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol. 4416, pp. 473\u2013486. Springer, Heidelberg (2007)","DOI":"10.1007\/978-3-540-71493-4_37"},{"key":"32_CR24","doi-asserted-by":"crossref","unstructured":"Prajna, S., Jadbabaie, A.: Safety verification of hybrid systems using barrier certificates. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 477\u2013492. Springer, Heidelberg (2004)","DOI":"10.1007\/978-3-540-24743-2_32"},{"key":"32_CR25","doi-asserted-by":"crossref","unstructured":"Prajna, S., Jadbabaie, A., Pappas, G.J.: A framework for worst-case and stochastic safety verification using barrier certificates. IEEE Transactions On Automatic Control 52, 1415\u20131428 (2007)","DOI":"10.1109\/TAC.2007.902736"},{"key":"32_CR26","unstructured":"Prajna, S., Papachristodoulou, A., Parrilo, P.A.: Introducing SOSTOOLS: a general purpose sum of squares programming solver. In: Proc. IEEE CDC (2002). http:\/\/www.cds.caltech.edu\/sostools and http:\/\/www.aut.ee.ethz.ch\/?parrilo\/sostools"},{"key":"32_CR27","doi-asserted-by":"crossref","unstructured":"Ratschan, S., She, Z.: Safety Verification of Hybrid Systems by Constraint Propagation-Based Abstraction Refinement. ACM Transactions on Embedded Computing Systems 6(1), 1\u201323 (2007). Article No. 8","DOI":"10.1145\/1210268.1210276"},{"key":"32_CR28","doi-asserted-by":"crossref","unstructured":"Ratschan, S., She, Z.: Providing a basin of attraction to a target region of polynomial systems by computation of Lyapunov-like functions. SIAM Journal on Control and Optimization 48, 4377\u20134394 (2010)","DOI":"10.1137\/090749955"},{"key":"32_CR29","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Chen, X., \u00c1brah\u00e1m, E.: Lyapunov function synthesis using Handelman representations. In: Proceedings of the 9th IFAC Symposium on Nonlinear Control Systems, pp. 576\u2013581 (2013)","DOI":"10.3182\/20130904-3-FR-2041.00198"},{"key":"32_CR30","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Constructing invariants for hybrid systems. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 539\u2013554. Springer, Heidelberg (2004)","DOI":"10.1007\/978-3-540-24743-2_36"},{"key":"32_CR31","doi-asserted-by":"crossref","unstructured":"Amin Ben Sassi, M.: Computation of polytopic invariants for polynomial dynamical systems using linear programming. Automatica 48, 3114\u20133121 (2012)","DOI":"10.1016\/j.automatica.2012.08.014"},{"key":"32_CR32","doi-asserted-by":"crossref","unstructured":"She, Z., Li, H., Xue, B., Zheng, Z., Xia, B.: Discovering polynomial Lyapunov functions for continuous dynamical systems. Journal of Symbolic Computation 58, 41\u201363 (2013)","DOI":"10.1016\/j.jsc.2013.06.003"},{"key":"32_CR33","doi-asserted-by":"crossref","unstructured":"She, Z., Xue, B.: Computing an invariance kernel with target by computing Lyapunov-like functions. IET Control Theory and Applications 7, 1932\u20131940 (2013)","DOI":"10.1049\/iet-cta.2013.0275"},{"key":"32_CR34","doi-asserted-by":"crossref","unstructured":"She, Z., Xue, B.: Discovering Multiple Lyapunov Functions for Switched Hybrid Systems. SIAM J. Control and Optimization 52(5), 3312\u20133340 (2014)","DOI":"10.1137\/130934313"},{"key":"32_CR35","doi-asserted-by":"crossref","unstructured":"Sturm, J.F.: Using SeDuMi 1.02, a MATLAB toolbox for optimization over symmetric cones. Optimization Methods and Software 11, 625\u2013653 (1999)","DOI":"10.1080\/10556789908805766"},{"key":"32_CR36","doi-asserted-by":"crossref","unstructured":"Tiwari, A., Khanna, G.: Series of abstractions for hybrid automata. In: Tomlin, C.J., Greenstreet, M.R. (eds.) HSCC 2002. LNCS, vol. 2289, pp. 465\u2013478. Springer, Heidelberg (2002)","DOI":"10.1007\/3-540-45873-5_36"},{"key":"32_CR37","doi-asserted-by":"crossref","unstructured":"Tiwari, A., Khanna, G.: Nonlinear systems: approximating reach sets. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 600\u2013614. Springer, Heidelberg (2004)","DOI":"10.1007\/978-3-540-24743-2_40"},{"key":"32_CR38","doi-asserted-by":"crossref","unstructured":"Tomlin, C.J., Mitchell, I., Bayen, A.M., Oishi, M.: Computational techniques for the verification of hybrid systems. Proc. of the IEEE 91, 986\u20131001 (2003)","DOI":"10.1109\/JPROC.2003.814621"},{"key":"32_CR39","doi-asserted-by":"crossref","unstructured":"VanAntwerp, J.G., Braatz, R.D.: A tutorial on linear and bilinear matrix inequalities. Journal of Process Control 10, 363\u2013385 (2000)","DOI":"10.1016\/S0959-1524(99)00056-6"},{"key":"32_CR40","doi-asserted-by":"crossref","unstructured":"Wu, M., Yang, Z.: Generating invariants of hybrid systems via sums-of-squares of polynomials with rational coefficients. In: Proc. International Workshop on Symbolic-Numeric Computation, pp. 104\u2013111 (2011)","DOI":"10.1145\/2331684.2331701"},{"key":"32_CR41","unstructured":"Yang, Z., Lin, W., Wu, M.: Exact Safety Verification of Hybrid Systems Based on Bilinear SOS Representation. ACM Trans. Embedded Comput. Syst 14(1), 1\u201319 (2015). Article No. 16"},{"key":"32_CR42","unstructured":"Zhou, K., Doyle, J.C., Glover, K.: Robust and Optimal Control. Prentice-Hall Inc., Upper Saddle River (1996)"}],"container-title":["Lecture Notes in Computer Science","Computer Algebra in Scientific Computing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-24021-3_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T11:37:34Z","timestamp":1748605054000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-24021-3_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319240206","9783319240213"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-24021-3_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}