{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,23]],"date-time":"2025-08-23T00:40:10Z","timestamp":1755909610144,"version":"3.44.0"},"publisher-location":"New York, NY, USA","reference-count":48,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,5,14]],"date-time":"2024-05-14T00:00:00Z","timestamp":1715644800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"ANR","award":["ANR-20-CE48-0014"],"award-info":[{"award-number":["ANR-20-CE48-0014"]}]},{"name":"AID-CIEDS","award":["project 2021 - FARO"],"award-info":[{"award-number":["project 2021 - FARO"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,5,14]]},"DOI":"10.1145\/3641513.3650125","type":"proceedings-article","created":{"date-parts":[[2024,5,2]],"date-time":"2024-05-02T18:05:48Z","timestamp":1714673148000},"page":"1-11","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Inner and outer approximate quantifier elimination for general reachability problems"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3198-1863","authenticated-orcid":false,"given":"Eric","family":"Goubault","sequence":"first","affiliation":[{"name":"LIX, CNRS, Ecole Polytechnique, Institut Polytechnique de Paris, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5624-3755","authenticated-orcid":false,"given":"Sylvie","family":"Putot","sequence":"additional","affiliation":[{"name":"LIX, CNRS, Ecole Polytechnique, Institut Polytechnique de Paris, France"}]}],"member":"320","published-online":{"date-parts":[[2024,5,14]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Proceedings of the 4th IEEE Mediterranean Symposium on Control and Automation (02","author":"Abdallah Chaouki","year":"1970","unstructured":"Chaouki Abdallah, Peter Dorato, and Wei Yang. 1970. Applications Of Quantifier Elimination Theory To Control System Design. Proceedings of the 4th IEEE Mediterranean Symposium on Control and Automation (02 1970)."},{"volume-title":"Reachability Analysis of Nonlinear Systems Using Conservative Polynomialization and Non-convex Sets","author":"Althoff M.","key":"e_1_3_2_1_2_1","unstructured":"M. Althoff. 2013. Reachability Analysis of Nonlinear Systems Using Conservative Polynomialization and Non-convex Sets. In HSCC. ACM publishers, 173\u2013182."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1967701.1967717"},{"volume-title":"Proceedings of CDC. 4042\u20134048","author":"Althoff M.","key":"e_1_3_2_1_4_1","unstructured":"M. Althoff, O. Stursberg, and M. Buss. 2008. Reachability analysis of nonlinear systems with uncertain parameters using conservative linearization. In Proceedings of CDC. 4042\u20134048."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"crossref","unstructured":"S. Bansal M. Chen S.\u00a0L. Herbert and C.\u00a0J. Tomlin. 2017. Hamilton-Jacobi reachability: A brief overview and recent advances. In CDC.","DOI":"10.1109\/CDC.2017.8263977"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/968708.968710"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"crossref","unstructured":"X. Chen E. \u00c1brah\u00e1m and S. Sankaranarayanan. 2012. Taylor Model Flowpipe Construction for Non-linear Hybrid Systems. In RTSS.","DOI":"10.1109\/RTSS.2012.70"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/2682923.2682940"},{"key":"e_1_3_2_1_9_1","unstructured":"X. Chen S. Sankaranarayanan and E. Abraham. 2014. Under-approximate Flowpipes for Non-linear Continuous Systems. In FMCAD."},{"volume-title":"Automata Theory and Formal Languages, H.\u00a0Brakhage (Ed.)","author":"Collins E.","key":"e_1_3_2_1_10_1","unstructured":"George\u00a0E. Collins. 1975. Quantifier elimination for real closed fields by cylindrical algebraic decompostion. In Automata Theory and Formal Languages, H.\u00a0Brakhage (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 134\u2013183."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/261320.261324"},{"volume-title":"RV(LNCS, Vol.\u00a08174)","author":"Donz\u00e9 Alexandre","key":"e_1_3_2_1_12_1","unstructured":"Alexandre Donz\u00e9. 2013. On Signal Temporal Logic. In RV(LNCS, Vol.\u00a08174). Springer."},{"key":"e_1_3_2_1_13_1","volume-title":"Robustness of temporal logic specifications for continuous-time signals. Theor. Comput. Sci. 410, 42","author":"Fainekos E.","year":"2009","unstructured":"Georgios\u00a0E. Fainekos and George\u00a0J. Pappas. 2009. Robustness of temporal logic specifications for continuous-time signals. Theor. Comput. Sci. 410, 42 (2009)."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"crossref","unstructured":"Sicun Gao Soonho Kong and Edmund Clarke. 2013. dReal: An SMT Solver for Nonlinear Theories of the Reals (Tool Paper). In CADE (Conference on Automated Deduction).","DOI":"10.1007\/978-3-642-38574-2_14"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"crossref","unstructured":"Isabel Garcia-Contreras V.\u00a0K.\u00a0Hari Govind Sharon Shoham and Arie Gurfinkel. 2023. Fast Approximations of\u00a0Quantifier Elimination. In Computer Aided Verification Constantin Enea and Akash Lal (Eds.). Springer Nature Switzerland Cham 64\u201386.","DOI":"10.1007\/978-3-031-37703-7_4"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"crossref","unstructured":"Yeting Ge and Leonardo de Moura. 2009. Complete instantiation for quantified formulas in satisfiability modulo theories. In Computer Aided Verification. 306\u2013320.","DOI":"10.1007\/978-3-642-02658-4_25"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"crossref","unstructured":"A. Girard C.\u00a0Le Guernic and O. Maler. 2006. Efficient Computation of Reachable Sets of Linear Time-Invariant Systems with Inputs. In HSCC.","DOI":"10.1007\/11730637_21"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2017.8264291"},{"key":"e_1_3_2_1_19_1","first-page":"130","article-title":"Modal Intervals Revisited","volume":"16","author":"Goldsztejn Alexandre","year":"2012","unstructured":"Alexandre Goldsztejn. 2012. Modal Intervals Revisited, Part 1: A Generalized Interval Natural Extension. Reliable Computing 16 (2012), 130\u2013183.","journal-title":"Part 1: A Generalized Interval Natural Extension. Reliable Computing"},{"key":"e_1_3_2_1_20_1","first-page":"184","article-title":"Modal Intervals Revisited","volume":"16","author":"Goldsztejn Alexandre","year":"2012","unstructured":"Alexandre Goldsztejn. 2012. Modal Intervals Revisited, Part 2: A Generalized Interval Mean Value Extension. Reliable Computing 16 (2012), 184\u2013209.","journal-title":"Part 2: A Generalized Interval Mean Value Extension. Reliable Computing"},{"key":"e_1_3_2_1_21_1","unstructured":"A. Goldsztejn D. Daney M. Rueher and P. Taillibert. 2005. Modal intervals revisited: a mean-value extension to generalized intervals. In QCP\u201905."},{"key":"e_1_3_2_1_22_1","unstructured":"A. Goldsztejn and L. Jaulin. 2010. Inner Approximation of the Range of Vector-Valued Functions. Reliable Computing 14 (2010)."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3302504.3311794"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/LCSYS.2020.2997261"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ifacol.2021.08.504"},{"key":"e_1_3_2_1_26_1","volume-title":"Guaranteed approximations of arbitrarily quantified reachability problems. arXiv:2309.07662","author":"Goubault Eric","year":"2023","unstructured":"Eric Goubault and Sylvie Putot. 2023. Guaranteed approximations of arbitrarily quantified reachability problems. arXiv:2309.07662 (2023)."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"crossref","unstructured":"C.\u00a0Le Guernic and A. Girard. 2009. Reachability Analysis of Hybrid Systems Using Support Functions. In CAV.","DOI":"10.1007\/978-3-642-02658-4_40"},{"key":"e_1_3_2_1_28_1","unstructured":"Wolfram\u00a0Research Inc.[n. d.]. Mathematica Version 13.1. https:\/\/www.wolfram.com\/mathematica Champaign IL 2022."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1006\/jsco.1997.0119"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/CDC42340.2020.9304022"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"crossref","unstructured":"A.\u00a0B. Kurzhanski and P. Varaiya. 2000. Ellipsoidal Techniques for Reachability Analysis. In HSCC.","DOI":"10.1007\/3-540-46430-1_19"},{"volume-title":"Planning Algorithms","author":"Lavalle M.","key":"e_1_3_2_1_32_1","unstructured":"Steven\u00a0M. Lavalle. 2006. Planning Algorithms. Cambridge University Press."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"crossref","unstructured":"M. Li P.N. Mosaad M. Fr\u00e4nzle Z. She and B. Xue. 2018. Safe over- and under- approximation of reachable sets for autonomous dynamical systems. In FORMATS. 252\u2013\u2013270.","DOI":"10.1007\/978-3-030-00151-3_15"},{"key":"e_1_3_2_1_34_1","unstructured":"K. Makino and M. Berz. 2003. Taylor models and other validated functional inclusion methods. Int. J. Pure Appl. Math (2003)."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2011.2105730"},{"key":"e_1_3_2_1_36_1","volume-title":"Bracketing the solutions of an ordinary differential equation with uncertain initial conditions. Appl. Math. Comput. 318","author":"M\u00e9zo Thomas\u00a0Le","year":"2018","unstructured":"Thomas\u00a0Le M\u00e9zo, Luc Jaulin, and Beno\u00eet Zerr. 2018. Bracketing the solutions of an ordinary differential equation with uncertain initial conditions. Appl. Math. Comput. 318 (2018)."},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2005.851439"},{"volume-title":"Hybrid Systems: Computation and Control","author":"Mitchell M.","key":"e_1_3_2_1_38_1","unstructured":"Ian\u00a0M. Mitchell. 2007. Comparing Forward and Backward Reachability as Tools for Safety Analysis. In Hybrid Systems: Computation and Control, Alberto Bemporad, Antonio Bicchi, and Giorgio Buttazzo (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 428\u2013443."},{"key":"e_1_3_2_1_39_1","series-title":"SIAM J. Numer. Anal 45","volume-title":"On Taylor model based integration of ODEs","author":"Neher M.","year":"2007","unstructured":"M. Neher, K.\u00a0R. Jackson, and N.\u00a0S. Nedialkov. 2007. On Taylor model based integration of ODEs. SIAM J. Numer. Anal 45 (2007)."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"crossref","unstructured":"Luan\u00a0Viet Nguyen James Kapinski Xiaoqing Jin Jyotirmoy\u00a0V. Deshmukh and Taylor\u00a0T. Johnson. 2017. Hyperproperties of Real-Valued Signals. In MEMOCODE \u201917.","DOI":"10.1145\/3127041.3127058"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"crossref","unstructured":"M.\u00a0A.\u00a0Ben Sassi R. Testylier T. Dang and A. Girard. 2012. Reachability Analysis of Polynomial Systems Using Linear Programming Relaxations(LNCS Vol.\u00a07561).","DOI":"10.1007\/978-3-642-33386-6_12"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/0196-8858(83)90014-3"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2016.7798471"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993886.1993935"},{"key":"e_1_3_2_1_45_1","unstructured":"A. Tarski. 1948. A decision method for elementary algebra and geometry. Technical Report. Rand Corporation."},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/s002000050055"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2310.19083"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"crossref","unstructured":"B. Xue Z. She and A. Easwaran. 2016. Under-Approximating Backward Reachable Sets by Polytopes. In CAV.","DOI":"10.1007\/978-3-319-41528-4_25"}],"event":{"name":"HSCC '24: Computation and Control","sponsor":["SIGCHI ACM Special Interest Group on Computer-Human Interaction"],"location":"Hong Kong SAR China","acronym":"HSCC '24"},"container-title":["Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3641513.3650125","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3641513.3650125","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,23]],"date-time":"2025-08-23T00:12:30Z","timestamp":1755907950000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3641513.3650125"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,5,14]]},"references-count":48,"alternative-id":["10.1145\/3641513.3650125","10.1145\/3641513"],"URL":"https:\/\/doi.org\/10.1145\/3641513.3650125","relation":{},"subject":[],"published":{"date-parts":[[2024,5,14]]},"assertion":[{"value":"2024-05-14","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}