{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,11]],"date-time":"2026-05-11T11:27:45Z","timestamp":1778498865142,"version":"3.51.4"},"reference-count":43,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2017,2,1]],"date-time":"2017-02-01T00:00:00Z","timestamp":1485907200000},"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":["J Syst Sci Complex"],"published-print":{"date-parts":[[2017,2]]},"DOI":"10.1007\/s11424-017-6226-1","type":"journal-article","created":{"date-parts":[[2017,2,13]],"date-time":"2017-02-13T04:29:29Z","timestamp":1486960169000},"page":"234-252","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Generating semi-algebraic invariants for non-autonomous polynomial hybrid systems"],"prefix":"10.1007","volume":"30","author":[{"given":"Qiuye","family":"Wang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yangjia","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bican","family":"Xia","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Naijun","family":"Zhan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,2,14]]},"reference":[{"key":"6226_CR1","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1007\/3-540-57318-6_30","volume":"736","author":"R Alur","year":"1992","unstructured":"Alur R, Courcoubetis C, Henzinger T, et al., Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems, Proceedings of Hybrid Systems, LNCS, Springer Berlin. Heldelberg, 1992, 736: 209\u2013229.","journal-title":"Proceedings of Hybrid Systems, LNCS, Springer Berlin. Heldelberg"},{"key":"6226_CR2","first-page":"20","volume":"1790","author":"E Asarin","year":"2000","unstructured":"Asarin E, Bournez O, Dang T, et al., Approximate reachability analysis of piecewise-linear dynamical systems, Proceedings of Hybrid Systems: Computation and Control, LNCS, Springer Berlin. Heldelberg, 2000, 1790: 20\u201331.","journal-title":"Proceedings of Hybrid Systems: Computation and Control, LNCS, Springer Berlin. Heldelberg"},{"issue":"3","key":"6226_CR3","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1006\/jsco.2001.0472","volume":"32","author":"G Lafferriere","year":"2001","unstructured":"Lafferriere G, Pappas G, and Yovine S, Symbolic reachability computation for families of linear vector fields. Journal of Symbolic Computation, 2001, 32(3): 231\u2013253.","journal-title":"Journal of Symbolic Computation"},{"issue":"1","key":"6226_CR4","doi-asserted-by":"crossref","first-page":"152","DOI":"10.1145\/1132357.1132363","volume":"5","author":"R Alur","year":"2006","unstructured":"Alur R, Dang T, and Ivancic F, Predicate abstraction for reachability analysis of hybrid systems. ACM Trasactions on Embedded Computing Systems, 2006, 5(1): 152\u2013199.","journal-title":"ACM Trasactions on Embedded Computing Systems"},{"key":"6226_CR5","doi-asserted-by":"crossref","first-page":"482","DOI":"10.1007\/978-3-319-24953-7_34","volume":"9364","author":"T Gan","year":"2015","unstructured":"Gan T, Chen M, Dai L, et al., Decidability of the reachability for a family of linear vector fields, Proceedings of International Symposium on Automated Technology for Verification and Analysis, LNCS, Springer Berlin. Heldelberg, 2015, 9364: 482\u2013499.","journal-title":"Proceedings of International Symposium on Automated Technology for Verification and Analysis, LNCS, Springer Berlin. Heldelberg"},{"key":"6226_CR6","volume-title":"Proceedings of European Control Conference, Aalborg","author":"T Gan","year":"2016","unstructured":"Gan T, Chen M, Li Y, et al., Computing reachable sets of linear vector fields revisited, Proceedings of European Control Conference, Aalborg, 2016."},{"key":"6226_CR7","first-page":"477","volume":"2993","author":"S Prajna","year":"2004","unstructured":"Prajna S and Jadbabaie A, Safety verification of hybrid systems using barrier certificates, Proceedings of Hybrid Systems: Computation and Control, LNCS, Springer Berlin. Heldelberg, 2004, 2993: 477\u2013492.","journal-title":"Heldelberg"},{"key":"6226_CR8","first-page":"539","volume":"2993","author":"S Sankaranarayanan","year":"2004","unstructured":"Sankaranarayanan S, Sipma H, and Manna Z, Constructing invariants for hybrid systems, Proceedings of Hybrid Systems: Computation and Control, LNCS, Springer Berlin. Heldelberg, 2004, 2993: 539\u2013554.","journal-title":"Heldelberg"},{"key":"6226_CR9","first-page":"190","volume":"5123","author":"S Gulwani","year":"2008","unstructured":"Gulwani S and Tiwari A, Constraint-based approach for analysis of hybrid systems, Proceedings of International Conference on Computer Aided Verification, LNCS, Springer Berlin. Heldelberg, 2008, 5123: 190\u2013203.","journal-title":"Heldelberg"},{"key":"6226_CR10","first-page":"176","volume":"5123","author":"A Platzer","year":"2008","unstructured":"Platzer A and Clarke E, Computing differential invariants of hybrid systems as fixedpoints, Proceedings of International Conference on Computer Aided Verification, LNCS, Springer Berlin. Heldelberg, 2008, 5123: 176\u2013189.","journal-title":"Heldelberg"},{"key":"6226_CR11","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1145\/2038642.2038659","volume-title":"Proceedings of ACM International Conference on Embedded Software","author":"J Liu","year":"2011","unstructured":"Liu J, Zhan N, and Zhao H, Computing semi-algebraic invariants for polynomial dynamical systems. Proceedings of ACM International Conference on Embedded Software, 2011, 97\u2013106."},{"issue":"1","key":"6226_CR12","first-page":"62","volume":"80","author":"L Dai","year":"2016","unstructured":"Dai L, Gan T, Xia B, et al., Barrier certificate revisited, Journal of Symbolic Computation, 2016, 80(1): 62\u201386.","journal-title":"Journal of Symbolic Computation"},{"issue":"7","key":"6226_CR13","doi-asserted-by":"crossref","first-page":"1011","DOI":"10.1109\/5.871306","volume":"88","author":"E Asarin","year":"2000","unstructured":"Asarin E, Bournez O, Dang T, et al., Effective synthesis of switching controllers for linear systems, Proceedings of the IEEE, 2000, 88(7): 1011\u20131025.","journal-title":"Proceedings of the IEEE"},{"issue":"7","key":"6226_CR14","doi-asserted-by":"crossref","first-page":"949","DOI":"10.1109\/5.871303","volume":"88","author":"C Tomlin","year":"2000","unstructured":"Tomlin C, Lygeros J, and Sastry S, A game theoretic approach to controller design for hybrid systems, Proceedings of the IEEE, 2000, 88(7): 949\u2013970.","journal-title":"Proceedings of the IEEE"},{"key":"6226_CR15","first-page":"383","volume":"4","author":"A Taly","year":"2009","unstructured":"Taly A and Tiwari A, Deductive verification of continuous dynamical systems, LProceedings of IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. IPIcs, 2009, 4: 383\u2013394.","journal-title":"LProceedings of IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. IPIcs"},{"key":"6226_CR16","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1145\/1993886.1993935","volume-title":"Proceedings of International Symposium on Symbolic and Algebraic Computation","author":"T Sturm","year":"2011","unstructured":"Sturm T and Tiwari A, Verification and synthesis using real quantifier elimination. Proceedings of International Symposium on Symbolic and Algebraic Computation, 2011, 329\u2013336."},{"key":"6226_CR17","first-page":"471","volume":"7436","author":"H Zhao","year":"2012","unstructured":"Zhao H, Zhan N, Kapur D, et al., A \u201chybrid\u201d approach for synthesizing optimal controllers of hybrid systems: A case study of the oil pump industrial example, Proceedings of International Symposium on Formal Methods, LNCS, Springer Berlin. Heldelberg, 2012, 7436: 471\u2013485.","journal-title":"Proceedings of International Symposium on Formal Methods, LNCS, Springer Berlin. Heldelberg"},{"key":"6226_CR18","first-page":"354","volume":"8051","author":"H Zhao","year":"2013","unstructured":"Zhao H, Zhan N, and Kapur D, Synthesizing switching controllers for hybrid systems by generating invariants, Proceedings of Theories of Programming and Formal Methods, LNCS, Springer Berlin. Heidelberg, 2013, 8051: 354\u2013373.","journal-title":"Heidelberg"},{"key":"6226_CR19","doi-asserted-by":"crossref","first-page":"58","DOI":"10.1007\/978-3-540-45099-3_4","volume":"1824","author":"S Bensalem","year":"2000","unstructured":"Bensalem S, Bozga M, Fernandez J C, et al., A transformational approach for generating nonlinear invariants, Proceedings of 7th International Symposium on Static Analysis, LNCS, 2000, 1824: 58\u201374.","journal-title":"Proceedings of 7th International Symposium on Static Analysis, LNCS"},{"key":"6226_CR20","doi-asserted-by":"crossref","first-page":"420","DOI":"10.1007\/978-3-540-45069-6_39","volume":"2725","author":"M Colon","year":"2003","unstructured":"Colon M, Sankaranarayanan S, and Sipma H, Linear invariant generation using non-linear constraint solving, Proceedings of International Conference on Computer Aided Verification, LNCS, Springer Berlin. Heidelberg, 2003, 2725: 420\u2013432.","journal-title":"Proceedings of International Conference on Computer Aided Verification, LNCS, Springer Berlin. Heidelberg"},{"key":"6226_CR21","first-page":"318","volume-title":"Proceedings of Symoisium on Principles of Programming Languages","author":"S Sankaranarayanan","year":"2004","unstructured":"Sankaranarayanan S, Sipma H, and Manna Z, Non-linear loop invariant generation using gr\u00f6bner bases, Proceedings of Symoisium on Principles of Programming Languages, 2004, 318\u2013329."},{"key":"6226_CR22","volume-title":"Proceedings of Conferences on Applications of Computer Algebra. Beaumout","author":"D Kapur","year":"2004","unstructured":"Kapur D, Automatically generating loop invariants using quantifier elimination, Proceedings of Conferences on Applications of Computer Algebra. Beaumout, 2004."},{"key":"6226_CR23","first-page":"1","volume":"6461","author":"L Liu","year":"2010","unstructured":"Liu L, L\u00fc J, Quan Z, et al., A calculus for hybrid CSP, Proceedings of Asian Symposium on Programming Languages and Systems, LNCS, Springer Berlin. Heidelberg, 2010, 6461: 1\u201315.","journal-title":"Proceedings of Asian Symposium on Programming Languages and Systems, LNCS, Springer Berlin. Heidelberg"},{"key":"6226_CR24","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-14509-4","volume-title":"Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics","author":"A Platzer","year":"2010","unstructured":"Platzer A, Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics, Springer Berlin, Heidelberg, 2010."},{"key":"6226_CR25","first-page":"143","volume-title":"Chicago","author":"S Sankaranarayanan","year":"2011","unstructured":"Sankaranarayanan S, Automatic abstraction of non-linear systems using change of bases transformations, Proceedings of International Conference on Hybrid Systems: Computation and Control. Chicago, 2011, 143\u2013152."},{"key":"6226_CR26","doi-asserted-by":"crossref","first-page":"28","DOI":"10.1007\/978-3-642-32347-8_3","volume":"7406","author":"A Platzer","year":"2012","unstructured":"Platzer A, A differential operator approach to equational differential invariants, Proceedings of International Conference on Interactive Theorem Proving, LNCS, Springer Berlin. Heidelberg, 2012, 7406: 28\u201348.","journal-title":"Proceedings of International Conference on Interactive Theorem Proving, LNCS, Springer Berlin. Heidelberg"},{"key":"6226_CR27","first-page":"541","volume-title":"Proceedings of Logic in Computer Science","author":"A Platzer","year":"2012","unstructured":"Platzer A, The complete proof theory of hybrid systems. Proceedings of Logic in Computer Science, 2012, 541\u2013550."},{"key":"6226_CR28","first-page":"3699","volume":"4","author":"M Jirstrand","year":"1998","unstructured":"Jirstrand M, Invariant sets for a class of hybrid systems. Proceedings of IEEE Conference on Decision and Control, 1998, 4: 3699\u20133704.","journal-title":"Proceedings of IEEE Conference on Decision and Control"},{"key":"6226_CR29","first-page":"590","volume":"3414","author":"E Rodr\u00edguez-Carbonell","year":"2005","unstructured":"Rodr\u00edguez-Carbonell E and Tiwari A, Generating polynomial invariants for hybrid systems, Proceedings of Hybrid Systems: Computation and Control, LNCS, Springer Berlin. Heidelberg, 2005, 3414: 590\u2013605.","journal-title":"Proceedings of Hybrid Systems: Computation and Control, LNCS, Springer Berlin. Heidelberg"},{"key":"6226_CR30","first-page":"221","volume-title":"Proceedings of Hybrid Systems: Computation and Control","author":"S Sankaranarayanan","year":"2010","unstructured":"Sankaranarayanan S, Automatic invariant generation for hybrid systems using ideal fixed points. Proceedings of Hybrid Systems: Computation and Control, 2010, 221\u2013230."},{"key":"6226_CR31","first-page":"477","volume":"2993","author":"S Prajna","year":"2004","unstructured":"Prajna S and Jadbabaie A, Safety verification of hybrid systems using barrier certificates, Proceedings of Hybrid Systems: Computation and Control, LNCS, Springer Berlin. Heidelberg, 2004, 2993: 477\u2013492.","journal-title":"Heidelberg"},{"issue":"8","key":"6226_CR32","doi-asserted-by":"crossref","first-page":"1415","DOI":"10.1109\/TAC.2007.902736","volume":"52","author":"S Prajna","year":"2007","unstructured":"Prajna S, Jadbabaie A, and Pappas G, A framework for worst-case and stochastic safety verification using barrier certificates, IEEE Transactions on Automatic Control, 2007, 52(8): 1415\u20131428.","journal-title":"IEEE Transactions on Automatic Control"},{"key":"6226_CR33","first-page":"242","volume":"8044","author":"H Kong","year":"2013","unstructured":"Kong H, He F, Song X, et al., Exponential-condition-based barrier certificate generation for safety verification of hybrid systems, Proceedings of International Conference on Computer Aided Verification, LNCS, Springer Berlin. Heidelberg, 2013, 8044: 242\u2013257.","journal-title":"Proceedings of International Conference on Computer Aided Verification, LNCS, Springer Berlin. Heidelberg"},{"key":"6226_CR34","first-page":"15","volume-title":"Proceedings of Hybrid Systems: Computation and Control","author":"C Sloth","year":"2012","unstructured":"Sloth C, Pappas G, and Wisniewski R, Compositional safety analysis using barrier certificates. Proceedings of Hybrid Systems: Computation and Control, 2012, 15\u201324."},{"key":"6226_CR35","doi-asserted-by":"crossref","first-page":"181","DOI":"10.7146\/math.scand.a-12421","volume":"71","author":"G Moreno-Socias","year":"1992","unstructured":"Moreno-Socias G, Length of polynomial ascending chains and primitive recursiveness. Mathematica Scandinavica, 1992, 71: 181\u2013205.","journal-title":"Mathematica Scandinavica"},{"key":"6226_CR36","first-page":"269","volume-title":"Proceedings of Logic in Computer Science","author":"D Figueira","year":"2011","unstructured":"Figueira D, Figueira S, Schmitz S, et al., Ackermannian and primitive-recursive bounds with Dickson\u2019s lemma, Proceedings of Logic in Computer Science, 2011, 269\u2013278."},{"key":"6226_CR37","volume-title":"Invariant clusters for hybrid systems","author":"H Kong","year":"2016","unstructured":"Kong H, Bogomolov S, Schilling C, et al., Invariant clusters for hybrid systems, CoRR, abs\/1605. 01450, 2016."},{"key":"6226_CR38","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-2181-2","volume-title":"Ideals, Varieties, and Algorithms","author":"D Cox","year":"1992","unstructured":"Cox D, Little J, and O\u2019shea D, Ideals, Varieties, and Algorithms, Springer, 1992."},{"key":"6226_CR39","first-page":"562","volume-title":"Courier Corporation","author":"M Tenenbaum","year":"1963","unstructured":"Tenenbaum M and Pollard H, Ordinary Differential Equations: An Elementary Textbook for Students of Mathematics, Engineering, and the Sciences. Courier Corporation, 1963, 562\u2013563."},{"issue":"3","key":"6226_CR40","doi-asserted-by":"crossref","first-page":"102","DOI":"10.1145\/1358190.1358197","volume":"41","author":"B Xia","year":"2007","unstructured":"Xia B, DISCOVERER: A tool for solving semi-algebraic systems, ACM Communications in Computer Algebra, 2007, 41(3): 102\u2013103.","journal-title":"ACM Communications in Computer Algebra"},{"issue":"4","key":"6226_CR41","first-page":"45","volume":"6","author":"Y Li","year":"2016","unstructured":"Li Y, Lu H, Zhan N, et al., Termination analysis of polynomial programs with equality conditions, Computer Science, 2016, 6(4): 45\u201314.","journal-title":"Computer Science"},{"issue":"3\u20134","key":"6226_CR42","doi-asserted-by":"crossref","first-page":"475","DOI":"10.1016\/j.jsc.2005.09.007","volume":"41","author":"B Buchberger","year":"2006","unstructured":"Buchberger B, An algorithm for finding the basis elements of the residue class ring of a zero dimensional polynomial ideal, Journal of Symbolic Computation, 2006, 41(3\u20134): 475\u2013511.","journal-title":"Journal of Symbolic Computation"},{"key":"6226_CR43","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1145\/2038642.2038659","volume-title":"ACM International Conference on Embedded Software","author":"J Liu","year":"2011","unstructured":"Liu J, Zhan N, and Zhao H, Computing semi-algebraic invariants for polynomial dynamical systems. ACM International Conference on Embedded Software, 2011, 97\u2013106."}],"container-title":["Journal of Systems Science and Complexity"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11424-017-6226-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11424-017-6226-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11424-017-6226-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,24]],"date-time":"2022-07-24T01:26:56Z","timestamp":1658626016000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11424-017-6226-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,2]]},"references-count":43,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2017,2]]}},"alternative-id":["6226"],"URL":"https:\/\/doi.org\/10.1007\/s11424-017-6226-1","relation":{},"ISSN":["1009-6124","1559-7067"],"issn-type":[{"value":"1009-6124","type":"print"},{"value":"1559-7067","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,2]]}}}