{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T07:10:10Z","timestamp":1748761810344,"version":"3.41.0"},"reference-count":42,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2016,1,25]],"date-time":"2016-01-25T00:00:00Z","timestamp":1453680000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"name":"Danish National Research Foundation and the National Natural Science Foundation of China","award":["61361136002"],"award-info":[{"award-number":["61361136002"]}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61321064"],"award-info":[{"award-number":["61321064"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Shanghai Collaborative Innovation Center of Trustworthy Software for Internet of Things","award":["ZF1213"],"award-info":[{"award-number":["ZF1213"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Mobile Netw Appl"],"published-print":{"date-parts":[[2016,2]]},"DOI":"10.1007\/s11036-015-0671-7","type":"journal-article","created":{"date-parts":[[2016,1,25]],"date-time":"2016-01-25T05:25:28Z","timestamp":1453699528000},"page":"35-52","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["SMT-Based Symbolic Encoding and Formal Analysis of HML Models"],"prefix":"10.1007","volume":"21","author":[{"given":"Huixing","family":"Fang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Huibiao","family":"Zhu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jifeng","family":"He","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,1,25]]},"reference":[{"key":"671_CR1","doi-asserted-by":"crossref","unstructured":"Alur R, Courcoubetis C, Henzinger TA, Ho PH (1993) Hybrid Automata: An Algorithmic Approach to the Specification and Analysis of Hybrid Systems. In: Hybrid Systems, LNCS, vol 736. doi: 10.1007\/3-540-57318-6_30 . Springer, pp 209\u2013229","DOI":"10.1007\/3-540-57318-6_30"},{"key":"671_CR2","unstructured":"\u00c5str\u00f6m KJ, H\u00e4gglund T (2006) Advanced PID control. ISA-The Instrumentation, Systems, and Automation Society, Research Triangle Park, NC 27709"},{"key":"671_CR3","doi-asserted-by":"crossref","unstructured":"Baeten JCM, Weijland WP (1990) Process Algebra. Cambridge University Press","DOI":"10.1017\/CBO9780511624193"},{"key":"671_CR4","unstructured":"Barrett C, Stump A, Tinelli C (2010) The SMT-LIB Standard: Version 2.0. Tech. rep., Department of Computer Science, The University of Iowa, available at www.SMT-LIB.org"},{"key":"671_CR5","unstructured":"Berz M (1999) Modern Map Methods in Particle Beam Physics. ADV IMAG ELECT PHYS, vol 108. Elsevier"},{"issue":"4","key":"671_CR6","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1023\/A:1024467732637","volume":"4","author":"M Berz","year":"1998","unstructured":"Berz M, Makino K (1998) Verified Integration of ODEs and Flows Using Differential Algebraic Methods on High-Order Taylor Models. Reliab Comput 4(4):361\u2013369","journal-title":"Reliab Comput"},{"key":"671_CR7","first-page":"150","volume-title":"Proceedings of TACAS, LNCS, vol 6015","author":"R Bruttomesso","year":"2010","unstructured":"Bruttomesso R, Pek E, Sharygina N, Tsitovich A (2010) The OpenSMT Solver. In: Proceedings of TACAS, LNCS, vol 6015. Springer, Berlin, pp 150\u2013153"},{"issue":"11","key":"671_CR8","doi-asserted-by":"crossref","first-page":"3632","DOI":"10.1016\/j.cnsns.2010.01.005","volume":"15","author":"WD Chang","year":"2010","unstructured":"Chang WD, Shih SP (2010) PID Controller Design of Nonlinear Systems Using an Improved Particle Swarm Optimization Approach. Commun Nonlinear Sci 15(11):3632\u20133639","journal-title":"Commun Nonlinear Sci"},{"key":"671_CR9","doi-asserted-by":"crossref","unstructured":"Chen X, \u00c1brah\u00e1m E, Sankaranarayanan S (2013) Flow*: An Analyzer for Non-linear Hybrid Systems. In: Proceedings of CAV, LNCS, vol 8044. Springer, pp 258\u2013263","DOI":"10.1007\/978-3-642-39799-8_18"},{"key":"671_CR10","doi-asserted-by":"crossref","unstructured":"Chen X, Schupp S, Makhlouf I, \u00c1brah\u00e1m E, Frehse G, Kowalewski S (2015) A Benchmark Suite for Hybrid Systems Reachability Analysis. In: NASA Formal Methods, LNCS, vol 9058. Springer, pp 408\u2013414","DOI":"10.1007\/978-3-319-17524-9_29"},{"issue":"2","key":"671_CR11","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1016\/j.jlap.2004.02.001","volume":"62","author":"PJL Cuijpers","year":"2005","unstructured":"Cuijpers PJL, Reniers MA (2005) Hybrid Process Algebra. J Logic Algebr Progr 62(2):191\u2013245","journal-title":"J Logic Algebr Progr"},{"issue":"3","key":"671_CR12","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1007\/s10009-007-0062-x","volume":"10","author":"G Frehse","year":"2008","unstructured":"Frehse G (2008) PHAVer: Algorithmic Verification of Hybrid Systems Past HyTech. Int J Softw Tools Technol Transfer 10(3):263\u2013279","journal-title":"Int J Softw Tools Technol Transfer"},{"key":"671_CR13","doi-asserted-by":"crossref","unstructured":"Frehse G, Han Z, Krogh B (2004) Assume-Guarantee Reasoning for Hybrid I\/O-Automata by Over-Approximation of Continuous Interaction. In: Proceedings of CDC. IEEE, pp 479\u2013484","DOI":"10.1109\/CDC.2004.1428676"},{"key":"671_CR14","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 (2011) SpaceEx: Scalable Verification of Hybrid Systems. In: Proceedings of CAV, LNCS, vol 6806. Springer, pp 379\u2013395","DOI":"10.1007\/978-3-642-22110-1_30"},{"key":"671_CR15","doi-asserted-by":"crossref","unstructured":"Fritzson P, Engelson V (1998) Modelica\u2013A Unified Object-Oriented Language for System Modeling and Simulation. In: Proceedings of ECOOP, LNCS, vol 1445. Springer, pp 67\u201390","DOI":"10.1007\/BFb0054087"},{"key":"671_CR16","doi-asserted-by":"crossref","unstructured":"Gao S, Avigad J, Clarke EM (2012) Delta-Decidability Over the Reals. In: Proceedings of LICS. IEEE, pp 305\u2013314","DOI":"10.1109\/LICS.2012.41"},{"key":"671_CR17","doi-asserted-by":"crossref","unstructured":"Gao S, Kong S, Clarke EM (2013a) dReal: An SMT Solver for Nonlinear Theories Over the Reals. In: Proceedings of CADE. Springer, pp 208\u2013214","DOI":"10.1007\/978-3-642-38574-2_14"},{"key":"671_CR18","doi-asserted-by":"crossref","unstructured":"Gao S, Kong S, Clarke EM (2013b) Satisfiability Modulo ODEs. In: Proceedings of FMCAD. IEEE, pp 105\u2013112","DOI":"10.1109\/FMCAD.2013.6679398"},{"issue":"1","key":"671_CR19","doi-asserted-by":"crossref","first-page":"138","DOI":"10.1145\/1132973.1132980","volume":"32","author":"L Granvilliers","year":"2006","unstructured":"Granvilliers L, Benhamou F (2006) Algorithm 852: RealPaver: An Interval Solver Using Constraint Satisfaction Techniques. ACM T Math Software 32(1):138\u2013156","journal-title":"ACM T Math Software"},{"issue":"2","key":"671_CR20","first-page":"250","volume":"4","author":"CL Guernic","year":"2010","unstructured":"Guernic CL, Girard A (2010) Reachability Analysis of Linear Systems Using Support Functions. Nonlinear Analysis: Hybrid Systems 4(2):250\u2013262","journal-title":"Nonlinear Analysis: Hybrid Systems"},{"key":"671_CR21","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1007\/978-3-642-02547-1_2","volume-title":"Continuous-time markov decision processes. Stochastic Modelling and Applied Probability, vol 62","author":"X Guo","year":"2009","unstructured":"Guo X, Hernndez-Lerma O (2009) Continuous-time markov decision processes. Stochastic Modelling and Applied Probability, vol 62. Springer, Berlin, pp 9\u201318"},{"issue":"87","key":"671_CR22","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D Harel","year":"1987","unstructured":"Harel D (1987) Statecharts: A Visual Formalism for Complex Systems. Sci Comput Program 8(87):231\u2013274","journal-title":"Sci Comput Program"},{"key":"671_CR23","unstructured":"He J (1994) From CSP to Hybrid Systems. In: A Classical Mind, Essays in Honour of C.A.R. Hoare, Prentice Hall International, pp 171\u2013189"},{"key":"671_CR24","doi-asserted-by":"crossref","unstructured":"He J (2013) Hybrid Relation Calculus. In: Proceedings of ICECCS. IEEE, p 2","DOI":"10.1109\/ICECCS.2013.10"},{"key":"671_CR25","doi-asserted-by":"crossref","unstructured":"Henzinger TA (1996) The Theory of Hybrid Automata. In: Proceedings of LICS. IEEE, pp 278\u2013292","DOI":"10.1109\/LICS.1996.561342"},{"issue":"1\u20132","key":"671_CR26","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1007\/s100090050008","volume":"1","author":"TA Henzinger","year":"1997","unstructured":"Henzinger TA, Ho PH, Wong-Toi H (1997) HyTech : A Model Checker for Hybrid Systems. Int J Softw Tools Technol Transfer 1(1\u20132):110\u2013122","journal-title":"Int J Softw Tools Technol Transfer"},{"key":"671_CR27","doi-asserted-by":"crossref","first-page":"94","DOI":"10.1006\/jcss.1998.1581","volume":"57","author":"TA Henzinger","year":"1998","unstructured":"Henzinger TA, Kopke PW, Puri A, Varaiya P (1998) What\u2019s Decidable about Hybrid Automata? Journal of Computer and System Sciences 57:94\u2013124","journal-title":"Journal of Computer and System Sciences"},{"key":"671_CR28","doi-asserted-by":"crossref","unstructured":"Hoare CAR (1985) Communicating Sequential Processes. Prentice Hall","DOI":"10.1007\/978-3-642-82921-5_4"},{"key":"671_CR29","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4684-6802-1","volume-title":"Complexity Theory of Real Functions","author":"KI Ko","year":"1991","unstructured":"Ko KI (1991) Complexity Theory of Real Functions. Birkhauser Boston Inc., Cambridge"},{"key":"671_CR30","doi-asserted-by":"crossref","unstructured":"Kong S, Gao S, Chen W, Clarke E (2015) dReach: Delta-Reachability Analysis for Hybrid Systems. In: Proceedings of TACAS, Springer-Verlag, LNCS, vol 9035, pp 200\u2013205","DOI":"10.1007\/978-3-662-46681-0_15"},{"key":"671_CR31","doi-asserted-by":"crossref","unstructured":"Lynch N, Segala R, Vaandrager F, Weinberg H (1996) Hybrid I\/O Automata. In: Hybrid Systems III, LNCS, vol 1066. Springer, pp 496\u2013510","DOI":"10.1007\/BFb0020971"},{"key":"671_CR32","doi-asserted-by":"crossref","unstructured":"Lynch N, Segala R, Vaandrager F (2001) Hybrid I\/O Automata Revisited. In: Proceedings of HSCC, LNCS, vol 2034. Springer, pp 403\u2013417","DOI":"10.1007\/3-540-45351-2_33"},{"key":"671_CR33","doi-asserted-by":"crossref","first-page":"447","DOI":"10.1007\/BFb0032003","volume-title":"Real-Time: Theory in Practice, LNCS, vol 600","author":"O Maler","year":"1992","unstructured":"Maler O, Manna Z, Pnueli A (1992) From Timed to Hybrid Systems. In: Real-Time: Theory in Practice, LNCS, vol 600. Springer, Berlin, pp 447\u2013484"},{"key":"671_CR34","unstructured":"MathWorks (2015a) Simulink"},{"key":"671_CR35","unstructured":"MathWorks (2015b) Stateflow"},{"issue":"6","key":"671_CR36","doi-asserted-by":"crossref","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis R, Oliveras A, Tinelli C (2006) Solving SAT and SAT Modulo Theories: From an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T). J ACM 53(6):937\u2013977","journal-title":"J ACM"},{"issue":"8","key":"671_CR37","doi-asserted-by":"crossref","first-page":"871","DOI":"10.1016\/j.fss.2007.09.012","volume":"159","author":"PA Phan","year":"2008","unstructured":"Phan PA, Gale TJ (2008) Direct Adaptive Fuzzy Control with A Self-Structuring Algorithm. Fuzzy Set Syst 159(8):871\u2013899","journal-title":"Fuzzy Set Syst"},{"key":"671_CR38","doi-asserted-by":"crossref","unstructured":"Platzer A (2010) Logical Analysis of Hybrid Systems - Proving Theorems for Complex Dynamics. Springer","DOI":"10.1007\/978-3-642-14509-4"},{"issue":"5","key":"671_CR39","doi-asserted-by":"crossref","first-page":"541","DOI":"10.3166\/ejc.7.541-556","volume":"7","author":"M Von Mohrenschildt","year":"2001","unstructured":"Von Mohrenschildt M (2001) Symbolic Verification of Hybrid Systems: An Algebraic Approach. Eur J Control 7(5):541\u2013556","journal-title":"Eur J Control"},{"key":"671_CR40","doi-asserted-by":"crossref","unstructured":"Weihrauch K (2000) Computable Analysis: An Introduction. Springer","DOI":"10.1007\/978-3-642-56999-9"},{"issue":"2","key":"671_CR41","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1016\/S0954-1810(00)00007-8","volume":"14","author":"J Yi","year":"2000","unstructured":"Yi J, Yubazaki N (2000) Stabilization Fuzzy Control of Inverted Pendulum Systems. Artif Intell Eng 14(2):153\u2013163","journal-title":"Artif Intell Eng"},{"key":"671_CR42","unstructured":"Zhou C, Wang J, Ravn AP (1996) A Formal Description of Hybrid Systems. In: Hybrid Systems III, LNCS, vol 1066. Springer, pp 511\u2013530"}],"container-title":["Mobile Networks and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11036-015-0671-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11036-015-0671-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11036-015-0671-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T06:44:43Z","timestamp":1748760283000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11036-015-0671-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,1,25]]},"references-count":42,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2016,2]]}},"alternative-id":["671"],"URL":"https:\/\/doi.org\/10.1007\/s11036-015-0671-7","relation":{},"ISSN":["1383-469X","1572-8153"],"issn-type":[{"type":"print","value":"1383-469X"},{"type":"electronic","value":"1572-8153"}],"subject":[],"published":{"date-parts":[[2016,1,25]]}}}