{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,18]],"date-time":"2026-03-18T02:47:10Z","timestamp":1773802030764,"version":"3.50.1"},"reference-count":38,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2016,9,22]],"date-time":"2016-09-22T00:00:00Z","timestamp":1474502400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"crossref","award":["No. 11371003"],"award-info":[{"award-number":["No. 11371003"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"crossref","award":["No. 11461006"],"award-info":[{"award-number":["No. 11461006"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]},{"name":"Natural Science Foundation of Guangxi","award":["2012GXNSFGA060003"],"award-info":[{"award-number":["2012GXNSFGA060003"]}]},{"name":"Scientific Research Project from Guangxi Education Department","award":["201012MS274"],"award-info":[{"award-number":["201012MS274"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Cluster Comput"],"published-print":{"date-parts":[[2016,12]]},"DOI":"10.1007\/s10586-016-0652-z","type":"journal-article","created":{"date-parts":[[2016,9,21]],"date-time":"2016-09-21T23:36:34Z","timestamp":1474500994000},"page":"2189-2199","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Safety verification of finite real-time nonlinear hybrid systems using enhanced group preserving scheme"],"prefix":"10.1007","volume":"19","author":[{"given":"Hui","family":"Zhang","sequence":"first","affiliation":[]},{"given":"Jinzhao","family":"Wu","sequence":"additional","affiliation":[]},{"given":"Jianguang","family":"Lu","sequence":"additional","affiliation":[]},{"given":"Juan","family":"Tang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,9,22]]},"reference":[{"issue":"6","key":"652_CR1","doi-asserted-by":"publisher","first-page":"624","DOI":"10.3166\/ejc.16.624-641","volume":"16","author":"A Abate","year":"2010","unstructured":"Abate, A., Katoen, J.P., Lygeros, J., Prandini, M.: Approximate model checking of stochastic hybrid systems. Eur. J. Control 16(6), 624\u2013641 (2010). doi: 10.3166\/ejc.16.624-641","journal-title":"Eur. J. Control"},{"key":"652_CR2","volume-title":"Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems","author":"R Alur","year":"1993","unstructured":"Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.H.: Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems. Springer, New York (1993)"},{"issue":"3","key":"652_CR3","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1109\/32.489079","volume":"22","author":"R Alur","year":"1996","unstructured":"Alur, R., Henzinger, T.A., Ho, P.H.: Automatic symbolic verification of embedded systems. IEEE Trans. Softw. Eng. 22(3), 181\u2013201 (1996). doi: 10.1109\/32.489079","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"2","key":"652_CR4","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1016\/j.tcs.2005.11.026","volume":"354","author":"R Alur","year":"2006","unstructured":"Alur, R., Dang, T., Ivan\u010di\u0107, F.: Counterexample-guided predicate abstraction of hybrid systems. Theor. Comput. Sci. 354(2), 250\u2013271 (2006). doi: 10.1016\/j.tcs.2005.11.026","journal-title":"Theor. Comput. Sci."},{"issue":"7","key":"652_CR5","doi-asserted-by":"publisher","first-page":"1011","DOI":"10.1109\/5.871306","volume":"88","author":"E Asarin","year":"2000","unstructured":"Asarin, E., Bournez, O., Dang, T., Maler, O., Pnueli, A.: Effective synthesis of switching controllers for linear systems. Proc. IEEE 88(7), 1011\u20131025 (2000). doi: 10.1109\/5.871306","journal-title":"Proc. IEEE"},{"key":"652_CR6","doi-asserted-by":"crossref","DOI":"10.1137\/1.9781611971392","volume-title":"Computer Methods for Ordinary Differential Equations and Differential-algebraic Equations","author":"UM Ascher","year":"1998","unstructured":"Ascher, U.M., Petzold, L.R.: Computer Methods for Ordinary Differential Equations and Differential-algebraic Equations, vol. 61. SIAM, Philadelphia (1998)"},{"key":"652_CR7","volume-title":"Numerical Solution of Initial-Value Problems in Differential-Algebraic Equations","author":"KE Brenan","year":"1996","unstructured":"Brenan, K.E., Campbell, S.L., Petzold, L.R.: Numerical Solution of Initial-Value Problems in Differential-Algebraic Equations, vol. 14. SIAM, Philadelphia (1996)"},{"issue":"4","key":"652_CR8","doi-asserted-by":"publisher","first-page":"471","DOI":"10.1007\/s10626-009-0082-7","volume":"19","author":"A Casagrande","year":"2009","unstructured":"Casagrande, A., Piazza, C., Policriti, A.: Discrete semantics for hybrid automata. Discret. Event Dynamic Syst.Theory Appl. 19(4), 471\u2013493 (2009). doi: 10.1007\/s10626-009-0082-7","journal-title":"Discret. Event Dynamic Syst.Theory Appl."},{"key":"652_CR9","doi-asserted-by":"crossref","unstructured":"Chen, X., \u00c1brahm, E., Sankaranarayanan, S.: Flow*: An Analyzer for Non-linear Hybrid Systems. Computer Aided Verification. Computer Aided Verification, pp. 258\u2013263. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-39799-8_18"},{"key":"652_CR10","unstructured":"Chutinan, A.: Hybrid system verification using discrete model approximations. Ph.D. thesis, Carnegie Mellon University (1999)"},{"key":"652_CR11","doi-asserted-by":"crossref","first-page":"192","DOI":"10.1007\/3-540-36577-X_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems, Proceedings, Tools and Algorithms for the Construction and Analysis of Systems, Proceedings","author":"E Clarke","year":"2003","unstructured":"Clarke, E., Fehnker, A., Han, Z., Krogh, B., Stursberg, O., Theobald, M.: Verification of hybrid systems based on counterexample-guided abstraction refinement. In: Garavel, H., Hatcliff, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, Proceedings, Tools and Algorithms for the Construction and Analysis of Systems, Proceedings, vol. 2619, pp. 192\u2013207. Springer, Berlin (2003)"},{"issue":"4","key":"652_CR12","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1007\/s10586-009-0099-6","volume":"12","author":"V Curcin","year":"2009","unstructured":"Curcin, V., Ghanem, M.M., Guo, Y.: Analysing scientific workflows with computational tree logic. Cluster Comput. 12(4), 399\u2013419 (2009). doi: 10.1007\/s10586-009-0099-6","journal-title":"Cluster Comput."},{"issue":"7","key":"652_CR13","doi-asserted-by":"publisher","first-page":"985","DOI":"10.1109\/5.871305","volume":"88","author":"JM Davoren","year":"2000","unstructured":"Davoren, J.M., Nerode, A.: Logics for hybrid systems. Proc. IEEE 88(7), 985\u20131010 (2000). doi: 10.1109\/5.871305","journal-title":"Proc. IEEE"},{"key":"652_CR14","unstructured":"Dreossi, T., Piazza, C.: Non standard hybrid automata semantics. Ph.D. thesis, University degli Studi di Udine (2012)"},{"key":"652_CR15","first-page":"209","volume":"1","author":"M Franzle","year":"2007","unstructured":"Franzle, M., Herde, C., Teige, T., Ratschan, S., Schubert, T.: Efficient solving of large non-linear arithmetic constraint systems with complex boolean structure. J. Satisf. Boolean Model. Comput. 1, 209\u2013236 (2007)","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"652_CR16","doi-asserted-by":"crossref","first-page":"258","DOI":"10.1007\/978-3-540-31954-2_17","volume-title":"Hybrid Systems: Computation and Control","author":"G Frehse","year":"2005","unstructured":"Frehse, G.: Phaver: algorithmic verification of hybrid systems past hytech. In: Morari, M., Thiele, L. (eds.) Hybrid Systems: Computation and Control, vol. 3414, pp. 258\u2013273. Springer, Berlin (2005)"},{"key":"652_CR17","doi-asserted-by":"crossref","unstructured":"Frehse, G., Le Guernic, C., Donz\u00e9, A., Cotton, S., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., Maler, O.: Spaceex: scalable verification of hybrid systems. In: Computer Aided Verification, pp. 379\u2013395. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-22110-1_30"},{"key":"652_CR18","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1007\/978-3-540-31954-2_19","volume-title":"Hybrid Systems: Computation and Control","author":"A Girard","year":"2005","unstructured":"Girard, A.: Reachability of uncertain linear systems using zonotopes. In: Morari, M., Thiele, L. (eds.) Hybrid Systems: Computation and Control, vol. 3414, pp. 291\u2013305. Springer, Berlin (2005)"},{"key":"652_CR19","doi-asserted-by":"crossref","first-page":"186","DOI":"10.1007\/11599555_20","volume-title":"Embedded Software and Systems, Proceedings","author":"Z Gu","year":"2005","unstructured":"Gu, Z.: Solving real-time scheduling problems with model-checking. In: Yang, L.T., Zhou, X., Zhao, W., Wu, Z., Zhu, Y., Lin, M. (eds.) Embedded Software and Systems, Proceedings, vol. 3820, pp. 186\u2013197. Springer, Berlin (2005)"},{"issue":"1","key":"652_CR20","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1007\/s10586-015-0518-9","volume":"19","author":"KH Han","year":"2016","unstructured":"Han, K.H., Bae, W.S.: Proposing and verifying a security protocol for hash function-based iot communication system. Cluster Comput. 19(1), 497\u2013504 (2016). doi: 10.1007\/s10586-015-0518-9","journal-title":"Cluster Comput."},{"key":"652_CR21","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/978-3-642-59615-5_13","volume-title":"Verification of Digital and Hybrid System","author":"TA Henzinger","year":"2000","unstructured":"Henzinger, T.A.: The theory of hybrid automata. In: Inan, M.K., Kurshan, R.P. (eds.) Verification of Digital and Hybrid System, vol. 170, pp. 265\u2013292. Springer, Berlin (2000)"},{"issue":"4","key":"652_CR22","doi-asserted-by":"publisher","first-page":"540","DOI":"10.1109\/9.664156","volume":"43","author":"TA Henzinger","year":"1998","unstructured":"Henzinger, T.A., Ho, P.H., Wong-Toi, H.: Algorithmic analysis of nonlinear hybrid systems. IEEE Trans. Autom. Control 43(4), 540\u2013554 (1998). doi: 10.1109\/9.664156","journal-title":"IEEE Trans. Autom. Control"},{"issue":"1","key":"652_CR23","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1006\/jcss.1998.1581","volume":"57","author":"TA Henzinger","year":"1998","unstructured":"Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What\u2019s decidable about hybrid automata? J. Comput. Syst. Sci. 57(1), 94\u2013124 (1998). doi: 10.1006\/jcss.1998.1581","journal-title":"J. Comput. Syst. Sci."},{"issue":"2","key":"652_CR24","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/s0020-7462(98)00029-8","volume":"34","author":"HK Hong","year":"1999","unstructured":"Hong, H.K., Liu, C.S.: Internal symmetry in bilinear elastoplasticity. Int. J. Non-Linear Mech. 34(2), 279\u2013288 (1999). doi: 10.1016\/s0020-7462(98)00029-8","journal-title":"Int. J. Non-Linear Mech."},{"issue":"4","key":"652_CR25","doi-asserted-by":"publisher","first-page":"679","DOI":"10.1016\/s0020-7462(00)00033-0","volume":"36","author":"HK Hong","year":"2001","unstructured":"Hong, H.K., Liu, C.S.: Lorentz group on minkowski spacetime for construction of the two basic principles of plasticity. Int. J. Non-Linear Mech. 36(4), 679\u2013686 (2001). doi: 10.1016\/s0020-7462(00)00033-0","journal-title":"Int. J. Non-Linear Mech."},{"issue":"11","key":"652_CR26","doi-asserted-by":"publisher","first-page":"19","DOI":"10.7498\/aps.65.110501.11-1958\/O4","volume":"65","author":"L Jian-Guang","year":"2016","unstructured":"Jian-Guang, L., Juan, T., Xiao-Lin, Q., Yong, F.: Modified group preserving methods and applications in chaotic systems. Acta Phys. Sin. 65(11), 19\u201327 (2016). doi: 10.7498\/aps.65.110501.11-1958\/O4","journal-title":"Acta Phys. Sin."},{"key":"652_CR27","volume-title":"Nonlinear Systems","author":"HK Khalil","year":"2002","unstructured":"Khalil, H.K.: Nonlinear Systems, 3rd edn. Prentice-Hall, Upper Saddle River, NJ (2002)","edition":"3"},{"issue":"1","key":"652_CR28","doi-asserted-by":"publisher","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). doi: 10.1109\/tac.2006.887900","journal-title":"IEEE Trans. Autom. Control"},{"key":"652_CR29","doi-asserted-by":"crossref","unstructured":"Le Guernic, C., Girard, A.: Reachability analysis of hybrid systems using support functions. In: Computer Aided Verification, pp. 540\u2013554. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-02658-4_40"},{"issue":"2","key":"652_CR30","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/s10586-013-0310-7","volume":"17","author":"JL Lerida","year":"2014","unstructured":"Lerida, J.L., Agraz, A., Solsona, F., Angels\u00a0Colomer, M.: Psyscal: a parallel tool for calibration of ecosystem models. Cluster Comput. 17(2), 271\u2013279 (2014). doi: 10.1007\/s10586-013-0310-7","journal-title":"Cluster Comput."},{"issue":"3","key":"652_CR31","doi-asserted-by":"publisher","first-page":"642","DOI":"10.1109\/tpds.2013.50","volume":"25","author":"T Li","year":"2014","unstructured":"Li, T., Tan, F., Wang, Q., Bu, L., Cao, J.N., Liu, X.: From offline toward real time: a hybrid systems model checking and cps codesign approach for medical device plug-and-play collaborations. IEEE Trans. Parallel Distrib. Syst. 25(3), 642\u2013652 (2014). doi: 10.1109\/tpds.2013.50","journal-title":"IEEE Trans. Parallel Distrib. Syst."},{"issue":"7","key":"652_CR32","doi-asserted-by":"publisher","first-page":"1047","DOI":"10.1016\/s0020-7462(00)00069-x","volume":"36","author":"CS Liu","year":"2001","unstructured":"Liu, C.S.: Cone of non-linear dynamical system and group preserving schemes. Int. J. Non-Linear Mech. 36(7), 1047\u20131068 (2001). doi: 10.1016\/s0020-7462(00)00069-x","journal-title":"Int. J. Non-Linear Mech."},{"issue":"2","key":"652_CR33","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/s10817-008-9103-8","volume":"41","author":"A Platzer","year":"2008","unstructured":"Platzer, A.: Differential dynamic logic for hybrid systems. J. Autom. Reason. 41(2), 143\u2013189 (2008). doi: 10.1007\/s10817-008-9103-8","journal-title":"J. Autom. Reason."},{"issue":"8","key":"652_CR34","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). doi: 10.1109\/tac.2007.902736","journal-title":"IEEE Trans. Autom. Control"},{"key":"652_CR35","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/3-540-45352-0_5","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems, Proceedings","author":"J Sproston","year":"2000","unstructured":"Sproston, J.: Decidable model checking of probabilistic hybrid automata. In: Joseph, M. (ed.) Formal Techniques in Real-Time and Fault-Tolerant Systems, Proceedings, vol. 1926, pp. 31\u201345. Springer, Berlin (2000)"},{"key":"652_CR36","unstructured":"Stoer, J., Bulirsch, R.: Introduction to Numerical Analysis, vol.\u00a012. Springer Science and Business Media (2013)"},{"issue":"9","key":"652_CR37","doi-asserted-by":"publisher","first-page":"1213","DOI":"10.1016\/s0893-6080(99)00068-4","volume":"12","author":"A Tonnelier","year":"1999","unstructured":"Tonnelier, A., Meignen, S., Bosch, H., Demongeot, J.: Synchronization and desynchronization of neural oscillators. Neural Netw. 12(9), 1213\u20131228 (1999). doi: 10.1016\/s0893-6080(99)00068-4","journal-title":"Neural Netw."},{"issue":"2","key":"652_CR38","doi-asserted-by":"publisher","first-page":"593","DOI":"10.1007\/s10586-013-0304-5","volume":"17","author":"Z Zong","year":"2014","unstructured":"Zong, Z., Fares, R., Romoser, B., Wood, J.: Faststor: improving the performance of a large scale hybrid storage system via caching and prefetching. Cluster Comput. 17(2), 593\u2013604 (2014). doi: 10.1007\/s10586-013-0304-5","journal-title":"Cluster Comput."}],"container-title":["Cluster Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10586-016-0652-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10586-016-0652-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10586-016-0652-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,13]],"date-time":"2019-09-13T17:36:19Z","timestamp":1568396179000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10586-016-0652-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,9,22]]},"references-count":38,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2016,12]]}},"alternative-id":["652"],"URL":"https:\/\/doi.org\/10.1007\/s10586-016-0652-z","relation":{},"ISSN":["1386-7857","1573-7543"],"issn-type":[{"value":"1386-7857","type":"print"},{"value":"1573-7543","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,9,22]]}}}