{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,14]],"date-time":"2025-10-14T14:47:34Z","timestamp":1760453254283},"reference-count":27,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2024,4,9]],"date-time":"2024-04-09T00:00:00Z","timestamp":1712620800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,4,9]],"date-time":"2024-04-09T00:00:00Z","timestamp":1712620800000},"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":["Acta Informatica"],"published-print":{"date-parts":[[2024,9]]},"DOI":"10.1007\/s00236-024-00458-8","type":"journal-article","created":{"date-parts":[[2024,4,9]],"date-time":"2024-04-09T07:02:14Z","timestamp":1712646134000},"page":"231-260","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Reachability analysis of linear systems"],"prefix":"10.1007","volume":"61","author":[{"given":"Shiping","family":"Chen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xinyu","family":"Ge","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,4,9]]},"reference":[{"key":"458_CR1","first-page":"215","volume-title":"Deciding Polynomial-Exponential Problems, ISSAC 2008","author":"M Achatz","year":"2008","unstructured":"Achatz, M., McCallum, S., Weispfenning, V.: Deciding Polynomial-Exponential Problems, ISSAC 2008, pp. 215\u2013222. ACM, New York (2008)"},{"issue":"1","key":"458_CR2","first-page":"3","volume":"138","author":"R Alur","year":"1995","unstructured":"Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Comput. Sci. 138(1), 3\u201334 (1995)","journal-title":"Comput. Sci."},{"issue":"2","key":"458_CR3","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"issue":"7","key":"458_CR4","first-page":"1692","volume":"37","author":"S Chen","year":"2017","unstructured":"Chen, S., Liu, Z.: Automated Proof of exponential polynomial inequality. J. Syst. Sci. Math. Sci. 37(7), 1692\u20131703 (2017)","journal-title":"J. Syst. Sci. Math. Sci."},{"issue":"5","key":"458_CR5","first-page":"804","volume":"39","author":"S Chen","year":"2019","unstructured":"Chen, S., Liu, Z.: Automated Proof of class of transcendental function inequalities. J. Syst. Sci. Math. Sci. 39(5), 804 (2019)","journal-title":"J. Syst. Sci. Math. Sci."},{"issue":"2020","key":"458_CR6","doi-asserted-by":"publisher","first-page":"318","DOI":"10.1016\/j.jsc.2019.10.002","volume":"101C","author":"S Chen","year":"2020","unstructured":"Chen, S., Liu, Z.: Automated proof of mixed trigonometric-polynomial inequalities. J. Symb. Comput. 101C(2020), 318\u2013329 (2020)","journal-title":"J. Symb. Comput."},{"issue":"2018","key":"458_CR7","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1016\/j.jsc.2017.07.007","volume":"85","author":"C Huang","year":"2018","unstructured":"Huang, C., Li, J., Xu, M., Li, Z.: Positive root isolation for poly-powers by exclusion and differentiation. J. Symb. Comput. 85(2018), 148\u2013169 (2018)","journal-title":"J. Symb. Comput."},{"key":"458_CR8","unstructured":"Chonev, V., Ouaknine, J., Worrell, J.: On the Skolem problem for continuous linear dynamical systems. In: Chatzigiannakis, I., Mitzenmacher, M., Rabani, Y., Sangiorgi, D. (eds.) 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), vol. 55, pp. 100-113. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2016)"},{"key":"458_CR9","doi-asserted-by":"crossref","unstructured":"Collins, G.E., Loos, R.: Polynomial real root isolation by differentiation. In Proceedings of the 1976 Symposium on Symbolic and Algebraic Computation SYMSAC76. ACM, pp. 15\u201325 (1976)","DOI":"10.1145\/800205.806319"},{"key":"458_CR10","doi-asserted-by":"publisher","first-page":"627","DOI":"10.1006\/jsco.1997.0157","volume":"24","author":"D Richardson","year":"1997","unstructured":"Richardson, D.: How to recognize zero. J. Symb. Comput. 24, 627\u2013645 (1997)","journal-title":"J. Symb. Comput."},{"key":"458_CR11","unstructured":"Gan, T.: Symbolic Numeric Approaches for Hybrid System Verification,Doctoral Dissertation, Peking University, Beijing (2016)"},{"key":"458_CR12","doi-asserted-by":"crossref","unstructured":"Gan, T., Chen, M., Dai, L., Xia, B., Zhan, N.J.: Decidability of the reachability for a family of linear vector fields. InATVA\u201915, vol. 9364 of LNCS, pp. 482\u2013499 (2015)","DOI":"10.1007\/978-3-319-24953-7_34"},{"key":"458_CR13","doi-asserted-by":"crossref","unstructured":"Han, J., Dai, L., Xia, B.: Constructing fewer open cells by gcd computation in CAD projection. In ISSAC 2014, pp. 240\u2013247. ACM (2014)","DOI":"10.1145\/2608628.2608676"},{"issue":"1","key":"458_CR14","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)","journal-title":"J. Comput. Syst. Sci."},{"key":"458_CR15","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1006\/jsco.2001.0472","volume":"32","author":"G Lafferriere","year":"2001","unstructured":"Lafferriere, G., Pappas, G.J., Yovine, S.: Symbolic reachability computation for for families of linear vector fields. J. Symb. Comput. 32, 231\u2013253 (2001)","journal-title":"J. Symb. Comput."},{"issue":"1","key":"458_CR16","first-page":"1","volume":"13","author":"G Lafferriere","year":"2000","unstructured":"Lafferriere, G., Pappas, G.J., Sastry, S.: O-minimal hybrid systems. MCSS 13(1), 1\u201321 (2000)","journal-title":"MCSS"},{"issue":"47","key":"458_CR17","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1016\/j.jsc.2011.08.004","volume":"2012","author":"S McCallum","year":"2012","unstructured":"McCallum, S., Weispfenning, V.: Deciding polynomial-transcendental problems. J. Symb Comput. 2012(47), 16\u201331 (2012)","journal-title":"J. Symb Comput."},{"issue":"12","key":"458_CR18","doi-asserted-by":"publisher","first-page":"1411","DOI":"10.1080\/00207720903480691","volume":"41","author":"M Xu","year":"2010","unstructured":"Xu, M., Chen, L., et al.: Reachability analysis of rational eigenvalue linear systems. Int. J. Syst. Sci. 41(12), 1411\u20131419 (2010). https:\/\/doi.org\/10.1080\/00207720903480691","journal-title":"Int. J. Syst. Sci."},{"issue":"2015","key":"458_CR19","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1016\/j.jsc.2014.09.015","volume":"68","author":"M Xu","year":"2015","unstructured":"Xu, M., Li, Z., Yang, L.: Quantifier elimination for a class of exponential polynomial formulas. J. Symb. Comput. 68(2015), 146\u2013168 (2015)","journal-title":"J. Symb. Comput."},{"key":"458_CR20","doi-asserted-by":"publisher","DOI":"10.1515\/9783110889055","volume-title":"Transcendental Numbers","author":"AB Shidlovskii","year":"1989","unstructured":"Shidlovskii, A.B.: Transcendental Numbers. Walter de Gruyter, Berlin, New York (1989)"},{"issue":"3","key":"458_CR21","doi-asserted-by":"publisher","first-page":"471","DOI":"10.1006\/jsco.1999.0327","volume":"29","author":"A Strzeboski","year":"2000","unstructured":"Strzeboski, A.: Solving systems of strict polynomial inequalities. J. Symb. Comput. 29(3), 471\u2013480 (2000)","journal-title":"J. Symb. Comput."},{"issue":"47","key":"458_CR22","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1016\/j.jsc.2011.11.004","volume":"2012","author":"A Strzeboski","year":"2012","unstructured":"Strzeboski, A.: Real root isolation for exp-log-arctan functions. J. Symb. Comput. 2012(47), 282\u2013314 (2012)","journal-title":"J. Symb. Comput."},{"key":"458_CR23","unstructured":"Chonev, V., Ouaknine, J., Worrell, J.: On the skolem problem for continuous linear dynamical systems (1994)"},{"key":"458_CR24","unstructured":"Wing, J.: How can we provide people with cyber-physical systems they can bet their lives on? Comput. Res. News 20(1), (2008)"},{"key":"458_CR25","unstructured":"Xu, M.: Some Symbolic Computation Issues in Program Verification and System Analysis. Doctoral Dissertation, East China Normal University, Shanghai (2010)"},{"key":"458_CR26","unstructured":"Lu, Y.: Practical automated reasoning on inequalities: generic programs for inequality proving and discovering. In Proceedings of the Third Asian Technology Conference in Mathematics. Tsukuba, Japan, pp. 24\u201335 (1998)"},{"key":"458_CR27","volume-title":"Introduction to Transcendental Numbers","author":"S Lang","year":"1996","unstructured":"Lang, S.: Introduction to Transcendental Numbers. Addison-Wesley, Boston (1996)"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-024-00458-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00236-024-00458-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-024-00458-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,8,14]],"date-time":"2024-08-14T10:03:17Z","timestamp":1723629797000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00236-024-00458-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,9]]},"references-count":27,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2024,9]]}},"alternative-id":["458"],"URL":"https:\/\/doi.org\/10.1007\/s00236-024-00458-8","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"type":"print","value":"0001-5903"},{"type":"electronic","value":"1432-0525"}],"subject":[],"published":{"date-parts":[[2024,4,9]]},"assertion":[{"value":"30 March 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"20 March 2024","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"9 April 2024","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}]}}