{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,12]],"date-time":"2026-05-12T11:54:49Z","timestamp":1778586889676,"version":"3.51.4"},"reference-count":22,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2017,4,12]],"date-time":"2017-04-12T00:00:00Z","timestamp":1491955200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,4,12]],"date-time":"2017-04-12T00:00:00Z","timestamp":1491955200000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/100000143","name":"Division of Computing and Communication Foundations","doi-asserted-by":"publisher","award":["1527398"],"award-info":[{"award-number":["1527398"]}],"id":[{"id":"10.13039\/100000143","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000144","name":"Division of Computer and Network Systems","doi-asserted-by":"publisher","award":["1464311"],"award-info":[{"award-number":["1464311"]}],"id":[{"id":"10.13039\/100000144","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100006602","name":"Air Force Research Laboratory","doi-asserted-by":"publisher","award":["FA8750-15-1-0105"],"award-info":[{"award-number":["FA8750-15-1-0105"]}],"id":[{"id":"10.13039\/100006602","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"publisher","award":["FA9550-15-1-0258"],"award-info":[{"award-number":["FA9550-15-1-0258"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"publisher","award":["FA9550-16-1-0246"],"award-info":[{"award-number":["FA9550-16-1-0246"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Discrete Event Dyn Syst"],"published-print":{"date-parts":[[2017,6]]},"DOI":"10.1007\/s10626-017-0244-y","type":"journal-article","created":{"date-parts":[[2017,4,12]],"date-time":"2017-04-12T05:45:26Z","timestamp":1491975926000},"page":"443-461","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Order-reduction abstractions for safety verification of high-dimensional linear systems"],"prefix":"10.1007","volume":"27","author":[{"given":"Hoang-Dung","family":"Tran","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luan Viet","family":"Nguyen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Weiming","family":"Xiang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Taylor T.","family":"Johnson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,4,12]]},"reference":[{"key":"244_CR1","doi-asserted-by":"crossref","unstructured":"Abbas H, Mittelmann H, Fainekos G (2014) Formal property verification in a conformance testing framework. In: Twelfth ACM\/IEEE international conference on formal methods and models for codesign (memocode), 2014. IEEE, pp 155\u2013164","DOI":"10.1109\/MEMCOD.2014.6961854"},{"key":"244_CR2","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1090\/conm\/280\/04630","volume":"280","author":"AC Antoulas","year":"2001","unstructured":"Antoulas A C, Sorensen D C, Gugercin S (2001) A survey of model reduction methods for large-scale systems. Contemp Math 280:193\u2013219","journal-title":"Contemp Math"},{"key":"244_CR3","volume-title":"18th international conference on hybrid systems: computation and control","author":"S Bak","year":"2015","unstructured":"Bak S, Bogomolov S, Johnson TT (2015) HyST: a source transformation and translation tool for hybrid automaton models. In: 18th international conference on hybrid systems: computation and control. ACM, Seattle, Washington"},{"key":"244_CR4","doi-asserted-by":"crossref","unstructured":"Chahlaoui Y, Van Dooren P (2005) Benchmark examples for model reduction of linear time-invariant dynamical systems. Dimension Reduction of Large-Scale Systems, pp 379\u2013392. Springer","DOI":"10.1007\/3-540-27909-1_24"},{"key":"244_CR5","doi-asserted-by":"crossref","unstructured":"De Moura L, Bj\u00f8rner N (2008) Z3: an efficient smt solver. In: International conference on tools and algorithms for the construction and analysis of systems. Springer, pp 337\u2013340","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"244_CR6","unstructured":"Duggirala PS, Mitra S, Viswanathan M (2013) Verification of annotated models from executions. In: Proceedings of the eleventh acm international conference on embedded software. Emsoft \u201913. ISBN 978-1-4799-1443-2. IEEE Press, Piscataway, NJ, USA"},{"key":"244_CR7","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: Computer aided verification. Springer, pp 379\u2013395","DOI":"10.1007\/978-3-642-22110-1_30"},{"issue":"8","key":"244_CR8","doi-asserted-by":"publisher","first-page":"1307","DOI":"10.1016\/j.automatica.2007.01.019","volume":"43","author":"A Girard","year":"2007","unstructured":"Girard A, Pappas GJ (2007) Approximate bisimulation relations for constrained linear systems. Automatica 43(8):1307\u20131317","journal-title":"Automatica"},{"issue":"2","key":"244_CR9","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/s10626-007-0029-9","volume":"18","author":"A Girard","year":"2008","unstructured":"Girard A, Julius AA, Pappas GJ (2008) Approximate simulation relations for hybrid systems. Discrete Event Dynamic Systems 18(2):163\u2013179","journal-title":"Discrete Event Dynamic Systems"},{"key":"244_CR10","doi-asserted-by":"crossref","unstructured":"Girard A, Pappas GJ, et al (2006) Approximate bisimulation for a class of stochastic hybrid systems. In: American control conference, 2006, vol 6. IEEE","DOI":"10.1109\/ACC.2006.1657467"},{"key":"244_CR11","unstructured":"Han Z (2005) Formal verification of hybrid systems using model order reduction and decomposition. PhD diss PhD thesis, Dept. of ECE, Carnegie Mellon University"},{"key":"244_CR12","unstructured":"Han Z, Krogh B (2004) Reachability analysis of hybrid control systems using reduced-order models American control conference, 2004. Proceedings of the 2004, vol 2. IEEE, pp 1183\u20131189"},{"key":"244_CR13","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1016\/j.tcs.2014.03.018","volume":"599","author":"MdA Islam","year":"2015","unstructured":"Islam MdA, Murthy A, Bartocci E, Cherry EM, Fenton FH, Glimm J, Smolka SA, Grosu R (2015) Model-order reduction of ion channel dynamics using approximate bisimulation. Theor Comput Sci 599:34\u201346. doi: 10.1016\/j.tcs.2014.03.018 . Advances in Computational Methods in Systems Biology","journal-title":"Theor Comput Sci"},{"key":"244_CR14","unstructured":"Julius AA (2006) Approximate abstraction of stochastic hybrid automata Hybrid systems: computation and control. Springer, pp 318\u2013332"},{"issue":"1","key":"244_CR15","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1109\/TAC.1981.1102568","volume":"26","author":"B Moore","year":"1981","unstructured":"Moore B (1981) Principal component analysis in linear systems: controllability, observability, and model reduction. IEEE Trans Autom Control 26(1):17\u201332","journal-title":"IEEE Trans Autom Control"},{"key":"244_CR16","doi-asserted-by":"crossref","unstructured":"Nesterov Y, Nemirovskii A, Ye Y (1994) Interior-point polynomial algorithms in convex programming, vol 13. SIAM","DOI":"10.1137\/1.9781611970791"},{"key":"244_CR17","unstructured":"Obinata G, Anderson BDO (2012) Model reduction for control system design. Springer"},{"issue":"12","key":"244_CR18","doi-asserted-by":"publisher","first-page":"2035","DOI":"10.1016\/j.automatica.2003.07.003","volume":"39","author":"GJ Pappas","year":"2003","unstructured":"Pappas G J (2003) Bisimilar linear systems. Automatica 39(12):2035\u20132047","journal-title":"Automatica"},{"issue":"1","key":"244_CR19","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/j.sysconle.2003.09.013","volume":"52","author":"P Tabuada","year":"2004","unstructured":"Tabuada P, Pappas G J (2004) Bisimilar control affine systems. Syst Control Lett 52(1):49\u201358","journal-title":"Syst Control Lett"},{"key":"244_CR20","unstructured":"Tanner HG, Pappas GJ (2003) Abstractions of constrained linear systems. In: American control conference, 2003. Proceedings of the 2003, vol 4. IEEE, pp 3381\u20133386"},{"issue":"12","key":"244_CR21","doi-asserted-by":"publisher","first-page":"2160","DOI":"10.1109\/TAC.2004.838497","volume":"49","author":"A van der Schaft","year":"2004","unstructured":"van der Schaft A (2004) Equivalence of dynamical systems by bisimulation. IEEE Trans Autom Control 49(12):2160\u20132172","journal-title":"IEEE Trans Autom Control"},{"key":"244_CR22","unstructured":"Vandenberghe L, Boyd S (1994) Positive definite programming. Mathematical Programming: State of the Art"}],"container-title":["Discrete Event Dynamic Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10626-017-0244-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10626-017-0244-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10626-017-0244-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:58:55Z","timestamp":1750197535000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10626-017-0244-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,4,12]]},"references-count":22,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2017,6]]}},"alternative-id":["244"],"URL":"https:\/\/doi.org\/10.1007\/s10626-017-0244-y","relation":{},"ISSN":["0924-6703","1573-7594"],"issn-type":[{"value":"0924-6703","type":"print"},{"value":"1573-7594","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,4,12]]},"assertion":[{"value":"31 August 2016","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"10 March 2017","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"12 April 2017","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}