{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,2]],"date-time":"2025-10-02T00:42:58Z","timestamp":1759365778322,"version":"build-2065373602"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032057914","type":"print"},{"value":"9783032057921","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,10,2]],"date-time":"2025-10-02T00:00:00Z","timestamp":1759363200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,10,2]],"date-time":"2025-10-02T00:00:00Z","timestamp":1759363200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-05792-1_18","type":"book-chapter","created":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T10:31:55Z","timestamp":1759314715000},"page":"333-352","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Symbolic Reduction for\u00a0Formal Synthesis of\u00a0Global Lyapunov Functions"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8762-2299","authenticated-orcid":false,"given":"Jun","family":"Liu","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3764-4542","authenticated-orcid":false,"given":"Maxwell","family":"Fitzsimmons","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,10,2]]},"reference":[{"key":"18_CR1","doi-asserted-by":"crossref","unstructured":"Abate, A., et al.: Automated formal synthesis of digital controllers for state-space physical plants. In: Proceedings of International Conference on Computer Aided Verification, pp. 462\u2013482. Springer (2017)","DOI":"10.1007\/978-3-319-63387-9_23"},{"key":"18_CR2","unstructured":"Ahmadi, A.A., Parrilo, P.A.: Stability of polynomial differential equations: complexity and converse Lyapunov questions. arXiv preprint arXiv:1308.6833 (2013)"},{"key":"18_CR3","doi-asserted-by":"crossref","unstructured":"Ahmed, D., Peruffo, A., Abate, A.: Automated and sound synthesis of Lyapunov functions with SMT solvers. In: Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 97\u2013114 (2020)","DOI":"10.1007\/978-3-030-45190-5_6"},{"key":"18_CR4","unstructured":"Arnold, V.: Problems of present day mathematics, xvii (dynamical systems and differential equations). In: Proc. Symp. Pure Math. vol.\u00a028 (1976)"},{"key":"18_CR5","doi-asserted-by":"crossref","unstructured":"Barrett, C., Tinelli, C.: Satisfiability modulo theories. Handbook of model checking, pp. 305\u2013343 (2018)","DOI":"10.1007\/978-3-319-10575-8_11"},{"key":"18_CR6","unstructured":"Chang, Y.C., Roohi, N., Gao, S.: Neural lyapunov control. Adv. Neural Inf. Proc. Syst. 32 (2019)"},{"key":"18_CR7","doi-asserted-by":"crossref","unstructured":"Cox, D.A., Little, J., O\u2019Shea, D.: Ideals, varieties, and algorithms: An Introduction to Computational Algebraic Geometry and Commutative Algebra. Springer, 4 edn. (2015)","DOI":"10.1007\/978-3-319-16721-3"},{"key":"18_CR8","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: International conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 337\u2013340. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"18_CR9","doi-asserted-by":"crossref","unstructured":"Edwards, A., Peruffo, A., Abate, A.: Fossil 2.0: formal certificate synthesis for the verification and control of dynamical models. In: Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control, pp. 1\u201310 (2024)","DOI":"10.1145\/3641513.3651398"},{"key":"18_CR10","doi-asserted-by":"crossref","unstructured":"Gerbet, D., R\u00f6benack, K.: Proving asymptotic stability with LaSalle\u2019s invariance principle: on the automatic computation of invariant sets using quantifier elimination. In: 2020 7th International Conference on Control, Decision and Information Technologies (CoDIT). vol.\u00a01, pp. 306\u2013311. IEEE (2020)","DOI":"10.1109\/CoDIT49905.2020.9263958"},{"key":"18_CR11","doi-asserted-by":"crossref","unstructured":"Giesl, P.: Construction of global lyapunov functions using radial basis functions. Springer (2007)","DOI":"10.1007\/978-3-540-69909-5"},{"issue":"8","key":"18_CR12","doi-asserted-by":"publisher","first-page":"2291","DOI":"10.3934\/dcdsb.2015.20.2291","volume":"20","author":"P Giesl","year":"2015","unstructured":"Giesl, P., Hafstein, S.: Review on computational methods for lyapunov functions. Discrete and Continuous Dynamical Systems-B 20(8), 2291\u20132331 (2015)","journal-title":"Discrete and Continuous Dynamical Systems-B"},{"key":"18_CR13","unstructured":"Huangfu, Q., Galabova, I., Feldmeier, M., Hall, J.A.J.: HiGHS - high performance software for linear optimization. https:\/\/highs.dev\/ (2023)"},{"key":"18_CR14","doi-asserted-by":"crossref","unstructured":"Kapinski, J., Deshmukh, J.V., Sankaranarayanan, S., Arechiga, N.: Simulation-guided lyapunov analysis for hybrid dynamical systems. In: Proceedings of the 17th International Conference On Hybrid Systems: Computation And Control, pp. 133\u2013142 (2014)","DOI":"10.1145\/2562059.2562139"},{"key":"18_CR15","unstructured":"Khalil, H.K.: Nonlinear Systems. Prentice-Hall (2002)"},{"key":"18_CR16","unstructured":"La\u00a0Salle, J., Lefschetz, S.: Stability by Liapunov\u2019s direct method with applications. Academic Press (1961)"},{"issue":"4","key":"18_CR17","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/s11786-012-0133-6","volume":"6","author":"J Liu","year":"2012","unstructured":"Liu, J., Zhan, N., Zhao, H.: Automatically discovering relaxed lyapunov functions for polynomial dynamical systems. Math. Comput. Sci. 6(4), 395\u2013408 (2012)","journal-title":"Math. Comput. Sci."},{"key":"18_CR18","unstructured":"Liu, J., Fitzsimmons, M.: Symbolic reduction for formal synthesis of global Lyapunov functions. arXiv preprint (2025)"},{"key":"18_CR19","doi-asserted-by":"crossref","unstructured":"Liu, J., Meng, Y., Fitzsimmons, M., Zhou, R.: LyZNet: a lightweight python tool for learning and verifying neural Lyapunov functions and regions of attraction. In: Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control, pp.\u00a01\u20138 (2024)","DOI":"10.1145\/3641513.3650134"},{"key":"18_CR20","doi-asserted-by":"publisher","DOI":"10.1016\/j.automatica.2025.112193","volume":"175","author":"J Liu","year":"2025","unstructured":"Liu, J., Meng, Y., Fitzsimmons, M., Zhou, R.: Physics-informed neural network lyapunov functions: pde characterization, learning, and verification. Automatica 175, 112193 (2025)","journal-title":"Automatica"},{"issue":"3","key":"18_CR21","doi-asserted-by":"publisher","first-page":"531","DOI":"10.1080\/00207179208934253","volume":"55","author":"AM Lyapunov","year":"1992","unstructured":"Lyapunov, A.M.: The general problem of the stability of motion. Int. J. Control 55(3), 531\u2013534 (1992)","journal-title":"Int. J. Control"},{"key":"18_CR22","unstructured":"Papachristodoulou, A., et al.: SOSTOOLS: sum of squares optimization toolbox for MATLAB (2013)"},{"key":"18_CR23","doi-asserted-by":"crossref","unstructured":"Papachristodoulou, A., Prajna, S.: On the construction of Lyapunov functions using the sum of squares decomposition. In: Proceedings of the 41st IEEE Conference on Decision and Control, 2002. vol.\u00a03, pp. 3482\u20133487. IEEE (2002)","DOI":"10.1109\/CDC.2002.1184414"},{"key":"18_CR24","doi-asserted-by":"crossref","unstructured":"Ravanbakhsh, H., Sankaranarayanan, S.: Counter-example guided synthesis of control Lyapunov functions for switched systems. In: 2015 54th IEEE conference on decision and control (CDC), pp. 4232\u20134239. IEEE (2015)","DOI":"10.1109\/CDC.2015.7402879"},{"key":"18_CR25","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/s10514-018-9791-9","volume":"43","author":"H Ravanbakhsh","year":"2019","unstructured":"Ravanbakhsh, H., Sankaranarayanan, S.: Learning control lyapunov functions from counterexamples and demonstrations. Auton. Robot. 43, 275\u2013307 (2019)","journal-title":"Auton. Robot."},{"issue":"23","key":"18_CR26","doi-asserted-by":"publisher","first-page":"576","DOI":"10.3182\/20130904-3-FR-2041.00198","volume":"46","author":"S Sankaranarayanan","year":"2013","unstructured":"Sankaranarayanan, S., et al.: Lyapunov function synthesis using handelman representations. IFAC Proc. Vol. 46(23), 576\u2013581 (2013)","journal-title":"IFAC Proc. Vol."},{"key":"18_CR27","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/j.jsc.2013.06.003","volume":"58","author":"Z She","year":"2013","unstructured":"She, Z., Li, H., Xue, B., Zheng, Z., Xia, B.: Discovering polynomial lyapunov functions for continuous dynamical systems. J. Symb. Comput. 58, 41\u201363 (2013)","journal-title":"J. Symb. Comput."},{"issue":"4","key":"18_CR28","doi-asserted-by":"publisher","first-page":"588","DOI":"10.1016\/j.nahs.2009.04.010","volume":"3","author":"Z She","year":"2009","unstructured":"She, Z., Xia, B., Xiao, R., Zheng, Z.: A semi-algebraic approach for asymptotic stability analysis. Nonlinear Anal. Hybrid Syst 3(4), 588\u2013596 (2009)","journal-title":"Nonlinear Anal. Hybrid Syst"},{"key":"18_CR29","doi-asserted-by":"crossref","unstructured":"Sturm, J.F.: Using SeDuMi 1.02, a MATLAB toolbox for optimization over symmetric cones. Optim. Meth. Softw. 11(1-4), 625\u2013653 (1999)","DOI":"10.1080\/10556789908805766"},{"issue":"10","key":"18_CR30","doi-asserted-by":"publisher","first-page":"2669","DOI":"10.1016\/j.automatica.2008.03.010","volume":"44","author":"U Topcu","year":"2008","unstructured":"Topcu, U., Packard, A., Seiler, P.: Local stability analysis using simulations and sum-of-squares programming. Automatica 44(10), 2669\u20132675 (2008)","journal-title":"Automatica"},{"key":"18_CR31","doi-asserted-by":"crossref","unstructured":"Virtanen, P., et\u00a0al.: SciPy 1.0: fundamental algorithms for scientific computing in Python. Nature Meth. 17(3), 261\u2013272 (2020)","DOI":"10.1038\/s41592-019-0686-2"},{"key":"18_CR32","first-page":"29113","volume":"35","author":"R Zhou","year":"2022","unstructured":"Zhou, R., Quartz, T., Sterck, H., Liu, J.: Neural lyapunov control of unknown nonlinear systems with stability guarantees. Adv. Neural. Inf. Process. Syst. 35, 29113\u201329125 (2022)","journal-title":"Adv. Neural. Inf. Process. Syst."},{"key":"18_CR33","unstructured":"Zubov, V.I.: Methods of AM Lyapunov and their application, vol.\u00a04439. US Atomic Energy Commission (1961)"}],"container-title":["Lecture Notes in Computer Science","Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-05792-1_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T10:32:05Z","timestamp":1759314725000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-05792-1_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,2]]},"ISBN":["9783032057914","9783032057921"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-05792-1_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,2]]},"assertion":[{"value":"2 October 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"QEST+FORMATS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Aarhus","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Denmark","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 August 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 August 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"qest2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.qest-formats.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}