1932

Abstract

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–Jacobi (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.

Loading

Article metrics loading...

/content/journals/10.1146/annurev-control-060117-104941
2018-05-28
2024-04-27
Loading full text...

Full text loading...

/deliver/fulltext/control/1/1/annurev-control-060117-104941.html?itemId=/content/journals/10.1146/annurev-control-060117-104941&mimeType=html&fmt=ahah

Literature Cited

  1. 1.  Kong S, Gao S, Chen W, Clarke E 2015. dReach: δ-reachability analysis for hybrid systems. Tools and Algorithms for the Construction and Analysis of Systems: TACAS 2015 C Baier, C Tinelli 200–5 Berlin: Springer
    [Google Scholar]
  2. 2.  Duggirala PS, Mitra S, Viswanathan M, Potok M 2015. C2E2: a verification tool for Stateflow models. Tools and Algorithms for the Construction and Analysis of Systems: TACAS 2015 C Baier, C Tinelli 68–82 Berlin: Springer
    [Google Scholar]
  3. 3.  Greenstreet MR, Mitchell I 1998. Integrating projections. Hybrid Systems: Computation and Control: HSCC 1998 TA Henzinger, SS Sastry 159–74 Berlin: Springer
    [Google Scholar]
  4. 4.  Frehse G, Le Guernic C, Donzé A, Cotton S, Ray R et al. 2011. SpaceEx: scalable verification of hybrid systems. Computer Aided Verification: CAV 2011 G Gopalakrishnan, S Qadeer 379–95 Berlin: Springer
    [Google Scholar]
  5. 5.  Kurzhanski A, Varaiya P 2000. Ellipsoidal techniques for reachability analysis: internal approximation. Syst. Control Lett. 41:201–11
    [Google Scholar]
  6. 6.  Kurzhanski A, Varaiya P 2002. On ellipsoidal techniques for reachability analysis. Part II: internal approximations box-valued constraints. Optim. Methods Softw. 17:207–37
    [Google Scholar]
  7. 7.  Maidens JN, Kaynama S, Mitchell IM, Oishi MMK, Dumont GA 2013. Lagrangian methods for approximating the viability kernel in high-dimensional systems. Automatica 49:2017–29
    [Google Scholar]
  8. 8.  Chen X, Ábrahám E, Sankaranarayanan S 2013. Flow*: an analyzer for non-linear hybrid systems. Computer Aided Verification: CAV 2013 N Sharygina, H Veith 258–63 Berlin: Springer
    [Google Scholar]
  9. 9.  Althoff M 2015. An introduction to CORA 2015. ARCH14-15: 1st and 2nd International Workshop on Applied veRification for Continuous and Hybrid Systems G Frehse, M Althoff 120–51 Manchester, UK: EasyChair
    [Google Scholar]
  10. 10.  Majumdar A, Vasudevan R, Tobenkin MM, Tedrake R 2014. Convex optimization of nonlinear feedback controllers via occupation measures. Int. J. Robot. Res. 33:1209–30
    [Google Scholar]
  11. 11.  Dreossi T, Dang T, Piazza C 2016. Parallelotope bundles for polynomial reachability. HCCC '16: Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control297–306 New York: ACM
    [Google Scholar]
  12. 12.  Nilsson P, Ozay N 2016. Synthesis of separable controlled invariant sets for modular local control design. 2016 American Control Conference (ACC)5656–63 New York: IEEE
    [Google Scholar]
  13. 13.  Althoff M, Krogh BH 2014. Reachability analysis of nonlinear differential-algebraic systems. IEEE Trans. Autom. Control 59:371–83
    [Google Scholar]
  14. 14.  Barron EN 1990. Differential games with maximum cost. Nonlinear Anal 14:971–89
    [Google Scholar]
  15. 15.  Mitchell IM, Bayen AM, Tomlin CJ 2005. A time-dependent Hamilton-Jacobi formulation of reachable sets for continuous dynamic games. IEEE Trans. Autom. Control 50:947–57
    [Google Scholar]
  16. 16.  Margellos K, Lygeros J 2011. Hamilton-Jacobi formulation for reach-avoid differential games. Trans. Autom. Control 56:1849–61
    [Google Scholar]
  17. 17.  Bokanowski O, Zidani H 2011. Minimal time problems with moving targets and obstacles. IFAC Proc. Vol. 44:2589–93
    [Google Scholar]
  18. 18.  Darbon J, Osher S 2016. Algorithms for overcoming the curse of dimensionality for certain Hamilton-Jacobi equations arising in control theory and elsewhere. Res. Math. Sci. 3:19
    [Google Scholar]
  19. 19.  Hafner MR, Del Vecchio D 2009. Computation of safety control for uncertain piecewise continuous systems on a partial order. Proceedings of the 48th IEEE Conference on Decision and Control (CDC) Held Jointly with 2009 28th Chinese Control Conference1671–77 New York: IEEE
    [Google Scholar]
  20. 20.  Coogan S, Arcak M 2015. Efficient finite abstraction of mixed monotone systems. HSCC '15: Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control58–67 New York: ACM
    [Google Scholar]
  21. 21.  Mitchell I 2011. Scalable calculation of reach sets and tubes for nonlinear systems with terminal integrators: a mixed implicit explicit formulation. HSCC '11: Proceedings of the 14th International Conference on Hybrid Systems: Computation and Control103–12 New York: ACM
    [Google Scholar]
  22. 22.  Fisac JF, Chen M, Tomlin CJ, Sastry SS 2015. Reach-avoid problems with time-varying dynamics, targets and constraints. HSCC '15: Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control11–20 New York: ACM
    [Google Scholar]
  23. 23.  Mitchell IM, Tomlin CJ 2003. Overapproximating reachable sets by Hamilton-Jacobi projections. J. Sci. Comput. 19:323–46
    [Google Scholar]
  24. 24.  Chen M, Herbert S, Tomlin CJ 2016. Fast reachable set approximations via state decoupling disturbances. 2016 IEEE 55th Conference on Decision and Control (CDC)191–96 New York: IEEE
    [Google Scholar]
  25. 25.  Kaynama S, Oishi M 2009. Schur-based decomposition for reachability analysis of linear time-invariant systems. Proceedings of the 48th IEEE Conference on Decision and Control (CDC) Held Jointly with 2009 28th Chinese Control Conference69–74 New York: IEEE
    [Google Scholar]
  26. 26.  Kaynama S, Oishi M 2013. A modified Riccati transformation for decentralized computation of the viability kernel under LTI dynamics. IEEE Trans. Autom. Control 58:2878–92
    [Google Scholar]
  27. 27.  Varaiya PP 1967. On the existence of solutions to a differential game. SIAM J. Control 5:153–62
    [Google Scholar]
  28. 28.  Evans LC, Souganidis PE 1984. Differential games and representation formulas for solutions of Hamilton-Jacobi-Isaacs equations. Ind. Univ. Math. J. 33:773–97
    [Google Scholar]
  29. 29.  Tomlin C, Lygeros J, Sastry SS 2000. A game theoretic approach to controller design for hybrid systems. Proc. IEEE 88:949–70
    [Google Scholar]
  30. 30.  Bokanowski O, Forcadel N, Zidani H 2010. Reachability and minimal times for state constrained nonlinear problems without any controllability assumption. SIAM J. Control Optim. 48:4292–316
    [Google Scholar]
  31. 31.  Ding J, Sprinkle J, Sastry SS, Tomlin CJ 2008. Reachability calculations for automated aerial refueling. 2008 47th IEEE Conference on Decision and Control3706–12 New York: IEEE
    [Google Scholar]
  32. 32.  Chen M, Hu Q, Mackin C, Fisac J, Tomlin CJ 2015. Safe platooning of unmanned aerial vehicles via reachability. 2015 54th IEEE Conference on Decision and Control (CDC)4695–701 New York: IEEE
    [Google Scholar]
  33. 33.  Bayen AM, Mitchell IM, Oishi M, Tomlin CJ 2007. Aircraft autolander safety analysis through optimal control-based reach set computation. AIAA J. Guid. Control Dyn. 30:68–77
    [Google Scholar]
  34. 34.  Huang H, Ding J, Zhang W, Tomlin C 2011. A differential game approach to planning in adversarial scenarios: a case study on capture-the-flag. 2011 IEEE International Conference on Robotics and Automation1451–56 New York: IEEE
    [Google Scholar]
  35. 35. Joint Plan. Dev. Office. 2013. Unmanned aircraft systems (UAS) comprehensive plan – a report on the nation's UAS path forward Tech. Rep., Fed. Aviat. Admin Washington, DC:
  36. 36. Amazon. 2017. Amazon Prime Air http://www.amazon.com/b?node=8037720011
  37. 37. BBC. 2015. Google plans drone delivery service for 2017. BBC News Nov. 2. http://www.bbc.co.uk/news/technology-34704868
  38. 38. 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
  39. 39.  Prevot T, Rios J, Kopardekar P, Robinson JE III, Johnson M, Jung J 2016. UAS Traffic Management (UTM) concept of operations to safely enable low altitude flight operations. 16th AIAA Aviation Technology, Integration, and Operations Conference chap. 2016-3292 Reston, VA: AIAA
    [Google Scholar]
  40. 40.  Mitchell IM 2008. The flexible, extensible and efficient toolbox of level set methods. J. Sci. Comput. 35:300–29
    [Google Scholar]
  41. 41.  Osher S, Fedkiw R 2003. Hamilton-Jacobi equations. Level Set Methods and Dynamic Implicit Surfaces47–54 New York: Springer
    [Google Scholar]
  42. 42.  Sethian JA 1996. A fast marching level set method for monotonically advancing fronts. PNAS 93:1591–95
    [Google Scholar]
  43. 43.  Coddington EA, Levinson N 1955. Existence and uniqueness of solutions. Theory of Ordinary Differential Equations1–42 New York: McGraw-Hill
    [Google Scholar]
  44. 44.  Mitchell IM 2007. Comparing forward and backward reachability as tools for safety analysis. Hybrid Systems: Computation and Control: HSCC 2007 A Bemporad, A Bicchi, G Buttazzo 428–43 Berlin: Springer
    [Google Scholar]
  45. 45.  Crandall MG, Lions PL 1983. Viscosity solutions of Hamilton-Jacobi equations. Trans. Am. Math. Soc. 277:1–42
    [Google Scholar]
  46. 46.  Crandall MG, Evans LC, Lions PL 1984. Some properties of viscosity solutions of Hamilton-Jacobi equations. Trans. Am. Math. Soc. 282:487–502
    [Google Scholar]
  47. 47.  Callier FM, Desoer CA 1991. The system representation R = [A,B,C,D], part II. Linear System Theory103–39 New York: Springer
    [Google Scholar]
  48. 48.  Sastry SS 1999. Linearization by state feedback. Nonlinear Systems: Analysis, Stability, and Control384–448 New York: Springer
    [Google Scholar]
  49. 49.  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
    [Crossref]
  50. 50.  Gillula JH, Hoffmann GM, Haomiao Huang, Vitus MP, Tomlin CJ 2011. Applications of hybrid reachability analysis to robotic aerial vehicles. Int. J. Robot. Res. 30:335–54
    [Google Scholar]
  51. 51.  Kaynama S, Oishi M 2011. Complexity reduction through a Schur-based decomposition for reachability analysis of linear time-invariant systems. Int. J. Control 84:165–79
    [Google Scholar]
  52. 52.  Tice BP 1991. Unmanned aerial vehicles – the force multiplier of the 1990s. Airpower J 5:41–55
    [Google Scholar]
  53. 53.  Haulman DL 2003. U.S. unmanned aerial vehicles in combat, 1991–2003. Tech. Rep., Air Force Hist. Res. Agency, Maxwell Air Force Base, Montgomery, AL
  54. 54.  Chen M, Hu Q, Fisac JF, Akametalu K, Mackin C, Tomlin CJ 2017. Reachability-based safety and goal satisfaction of unmanned aerial platoons on air highways. AIAA J. Guid. Control Dyn. 40:1360–73
    [Google Scholar]
  55. 55.  Chen M, Fisac JF, Sastry SS, Tomlin CJ 2015. Safe sequential path planning of multi-vehicle systems via double-obstacle Hamilton-Jacobi-Isaacs variational inequality. 2015 European Control Conference (ECC)3304–9 New York: IEEE
    [Google Scholar]
  56. 56.  Bansal S, Chen M, Fisac JF, Tomlin CJ 2017. Safe sequential path planning under disturbances and imperfect information. 2017 American Control Conference (ACC)5550–55 New York: IEEE
    [Google Scholar]
  57. 57.  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
  58. 58.  Chen M, Shih JC, Tomlin CJ 2016. Multi-vehicle collision avoidance via Hamilton-Jacobi reachability and mixed integer programming. 2016 IEEE 55th Conference on Decision and Control (CDC)1695–700 New York: IEEE
    [Google Scholar]
  59. 59.  Chen M, Zhou Z, Tomlin CJ 2017. Multiplayer reach-avoid games via pairwise outcomes. IEEE Trans. Autom. Control 62:1451–57
    [Google Scholar]
  60. 60.  Pierson A, Wang Z, Schwager M 2017. Intercepting rogue robots: an algorithm for capturing multiple evaders with multiple pursuers. IEEE Robot. Autom. Lett. 2:530–37
    [Google Scholar]
/content/journals/10.1146/annurev-control-060117-104941
Loading
/content/journals/10.1146/annurev-control-060117-104941
Loading

Data & Media loading...

  • Article Type: Review Article
This is a required field
Please enter a valid email address
Approval was a Success
Invalid data
An Error Occurred
Approval was partially successful, following selected items could not be processed due to error