{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,21]],"date-time":"2026-07-21T20:31:18Z","timestamp":1784665878716,"version":"3.55.0"},"reference-count":60,"publisher":"Annual Reviews","issue":"1","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Annu. Rev. Control Robot. Auton. Syst."],"published-print":{"date-parts":[[2018,5,28]]},"abstract":"<jats:p> Autonomous systems are becoming pervasive in everyday life, and many of these systems are complex and safety-critical. Formal verification is important for providing performance and safety guarantees for these systems. In particular, Hamilton\u2013Jacobi (HJ) reachability is a formal verification tool for nonlinear and hybrid systems; however, it is computationally intractable for analyzing complex systems, and computational burden is in general a difficult challenge in formal verification. In this review, we begin by briefly presenting background on reachability analysis with an emphasis on the HJ formulation. We then present recent work showing how high-dimensional reachability verification can be made more tractable by focusing on two areas of development: system decomposition for general nonlinear systems, and traffic protocols for unmanned airspace management. By tackling the curse of dimensionality, tractable verification of practical systems is becoming a reality, paving the way for more pervasive and safer automation. <\/jats:p>","DOI":"10.1146\/annurev-control-060117-104941","type":"journal-article","created":{"date-parts":[[2018,5,30]],"date-time":"2018-05-30T00:50:56Z","timestamp":1527641456000},"page":"333-358","source":"Crossref","is-referenced-by-count":105,"title":["Hamilton\u2013Jacobi Reachability: Some Recent Theoretical Advances and Applications in Unmanned Airspace Management"],"prefix":"10.1146","volume":"1","author":[{"given":"Mo","family":"Chen","sequence":"first","affiliation":[{"name":"Department of Electrical Engineering and Computer Sciences, University of California, Berkeley, California 94720, USA;,"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Claire J.","family":"Tomlin","sequence":"additional","affiliation":[{"name":"Department of Electrical Engineering and Computer Sciences, University of California, Berkeley, California 94720, USA;,"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"22","reference":[{"key":"B1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_15"},{"key":"B2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_5"},{"key":"B3","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-64358-3_38"},{"key":"B4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_30"},{"key":"B5","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6911(00)00059-1"},{"key":"B6","doi-asserted-by":"publisher","DOI":"10.1080\/1055678021000012435"},{"key":"B7","doi-asserted-by":"publisher","DOI":"10.1016\/j.automatica.2013.03.020"},{"key":"B8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_18"},{"key":"B9","first-page":"120","volume-title":"ARCH14-15: 1st and 2nd International Workshop on Applied veRification for Continuous and Hybrid Systems","author":"Althoff M","year":"2015"},{"key":"B10","doi-asserted-by":"publisher","DOI":"10.1177\/0278364914528059"},{"key":"B11","doi-asserted-by":"publisher","DOI":"10.1145\/2883817.2883838"},{"key":"B12","doi-asserted-by":"publisher","DOI":"10.1109\/ACC.2016.7526557"},{"key":"B13","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2013.2285751"},{"key":"B14","doi-asserted-by":"publisher","DOI":"10.1016\/0362-546X(90)90113-U"},{"key":"B15","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2005.851439"},{"key":"B16","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2011.2105730"},{"key":"B17","doi-asserted-by":"publisher","DOI":"10.3182\/20110828-6-IT-1002.02261"},{"key":"B18","doi-asserted-by":"publisher","DOI":"10.1186\/s40687-016-0068-7"},{"key":"B19","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2009.5400532"},{"key":"B20","doi-asserted-by":"publisher","DOI":"10.1145\/2728606.2728607"},{"key":"B21","doi-asserted-by":"publisher","DOI":"10.1145\/1967701.1967718"},{"key":"B22","doi-asserted-by":"publisher","DOI":"10.1145\/2728606.2728612"},{"key":"B23","doi-asserted-by":"publisher","DOI":"10.1023\/A:1025364227563"},{"key":"B24","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2016.7798268"},{"key":"B25","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2009.5400336"},{"key":"B26","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2013.2272152"},{"key":"B27","doi-asserted-by":"publisher","DOI":"10.1137\/0305009"},{"key":"B28","doi-asserted-by":"publisher","DOI":"10.1512\/iumj.1984.33.33040"},{"key":"B29","doi-asserted-by":"publisher","DOI":"10.1109\/5.871303"},{"key":"B30","doi-asserted-by":"publisher","DOI":"10.1137\/090762075"},{"key":"B31","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2008.4738998"},{"key":"B32","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2015.7402951"},{"key":"B33","doi-asserted-by":"publisher","DOI":"10.2514\/1.21562"},{"key":"B34","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA.2011.5980264"},{"key":"B35","unstructured":"35.\u2002 Joint Plan. Dev. Office.  2013.  Unmanned aircraft systems (UAS) comprehensive plan \u2013 a report on the nation's UAS path forward.  Tech. Rep., Fed. Aviat. Admin.  Washington, DC"},{"key":"B36","unstructured":"36.\u2002 Amazon.  2017.  Amazon Prime Air.  http:\/\/www.amazon.com\/b?node=8037720011"},{"key":"B37","unstructured":"37.\u2002 BBC.  2015.  Google plans drone delivery service for 2017.  BBC News,  Nov. 2. http:\/\/www.bbc.co.uk\/news\/technology-34704868"},{"key":"B38","unstructured":"38.\u2002 AUVSI News.  2016.  UAS aid in South Carolina tornado investigation.  AUVSI News,  Jan. 29. http:\/\/www.auvsi.org\/blogs\/auvsi-news\/2016\/01\/29\/tornado"},{"key":"B39","doi-asserted-by":"publisher","DOI":"10.2514\/6.2016-3292"},{"key":"B40","doi-asserted-by":"publisher","DOI":"10.1007\/s10915-007-9174-4"},{"key":"B41","doi-asserted-by":"publisher","DOI":"10.1007\/0-387-22746-6_5"},{"key":"B42","doi-asserted-by":"publisher","DOI":"10.1073\/pnas.93.4.1591"},{"key":"B43","first-page":"1","volume-title":"Theory of Ordinary Differential Equations","author":"Coddington EA","year":"1955"},{"key":"B44","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71493-4_34"},{"key":"B45","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-1983-0690039-8"},{"key":"B46","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-1984-0732102-X"},{"key":"B47","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0957-7_6"},{"key":"B48","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3108-8_9"},{"key":"B49","doi-asserted-by":"crossref","unstructured":"49.\u2002  Chen  M,  Herbert  SL,  Vashishtha  MS,  Bansal  S,  Tomlin  CJ.  2018.  Decomposition of reachable sets and tubes for a class of nonlinear systems.  IEEE Trans. Autom. Control.  In press. https:\/\/doi.org\/10.1109\/TAC.2018.2797194","DOI":"10.1109\/TAC.2018.2797194"},{"key":"B50","doi-asserted-by":"publisher","DOI":"10.1177\/0278364910387173"},{"key":"B51","doi-asserted-by":"publisher","DOI":"10.1080\/00207179.2010.543703"},{"key":"B52","first-page":"41","volume":"5","author":"Tice BP","year":"1991","journal-title":"Airpower J"},{"key":"B53","unstructured":"53.\u2002  Haulman  DL.  2003.  U.S. unmanned aerial vehicles in combat, 1991\u20132003.  Tech. Rep., Air Force Hist. Res. Agency, Maxwell Air Force Base, Montgomery, AL"},{"key":"B54","doi-asserted-by":"publisher","DOI":"10.2514\/1.G000774"},{"key":"B55","doi-asserted-by":"publisher","DOI":"10.1109\/ECC.2015.7331044"},{"key":"B56","doi-asserted-by":"publisher","DOI":"10.23919\/ACC.2017.7963818"},{"key":"B57","doi-asserted-by":"crossref","unstructured":"57.\u2002  Chen  M,  Bansal  S,  Fisac  JF,  Tomlin  CJ.  2018.  Robust sequential path planning under disturbances and adversarial intruder.  IEEE Trans. Control Syst. Technol.  In press","DOI":"10.23919\/ACC.2017.7963818"},{"key":"B58","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2016.7798509"},{"key":"B59","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2016.2577619"},{"key":"B60","doi-asserted-by":"publisher","DOI":"10.1109\/LRA.2016.2645516"}],"container-title":["Annual Review of Control, Robotics, and Autonomous Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.annualreviews.org\/doi\/pdf\/10.1146\/annurev-control-060117-104941","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,8]],"date-time":"2021-10-08T10:46:16Z","timestamp":1633689976000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.annualreviews.org\/doi\/10.1146\/annurev-control-060117-104941"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,5,28]]},"references-count":60,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2018,5,28]]}},"alternative-id":["10.1146\/annurev-control-060117-104941"],"URL":"https:\/\/doi.org\/10.1146\/annurev-control-060117-104941","relation":{},"ISSN":["2573-5144","2573-5144"],"issn-type":[{"value":"2573-5144","type":"print"},{"value":"2573-5144","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,5,28]]}}}