1932

Abstract

Reachability analysis consists in computing the set of states that are reachable by a dynamical system from all initial states and for all admissible inputs and parameters. It is a fundamental problem motivated by many applications in formal verification, controller synthesis, and estimation, to name only a few. This article focuses on a class of methods for computing a guaranteed overapproximation of the reachable set of continuous and hybrid systems, relying predominantly on set propagation; starting from the set of initial states, these techniques iteratively propagate a sequence of sets according to the system dynamics. After a review of set representation and computation, the article presents the state of the art of set propagation techniques for reachability analysis of linear, nonlinear, and hybrid systems. It ends with a discussion of successful applications of reachability analysis to real-world problems.

Loading

Article metrics loading...

/content/journals/10.1146/annurev-control-071420-081941
2021-05-03
2024-06-23
Loading full text...

Full text loading...

/deliver/fulltext/control/4/1/annurev-control-071420-081941.html?itemId=/content/journals/10.1146/annurev-control-071420-081941&mimeType=html&fmt=ahah

Literature Cited

  1. 1. 
    Clarke EMJr., Grumberg O, Kroening D, Peled D, Veith H 2018. Model Checking Cambridge, MA: MIT Press
    [Google Scholar]
  2. 2. 
    Baier C, Katoen JP. 2008. Principles of Model Checking Cambridge, MA: MIT Press
    [Google Scholar]
  3. 3. 
    Bertsekas DP, Rhodes IB. 1971. On the minimax reachability of target sets and target tubes. Automatica 7:233–47
    [Google Scholar]
  4. 4. 
    Alur R, Courcoubetis C, Halbwachs N, Henzinger TA, Ho PH et al. 1995. The algorithmic analysis of hybrid systems. Theor. Comput. Sci. 138:3–34
    [Google Scholar]
  5. 5. 
    Silva BI, Richeson K, Krogh B, Chutinan A 2000. Modeling and verifying hybrid dynamic systems using CheckMate. ADPM 2000 Conference Proceedings: The 4th International Conference on Automation of Mixed Processes: Hybrid Dynamic Systems323–28 Aachen, Ger: Shaker
    [Google Scholar]
  6. 6. 
    Asarin E, Dang T, Maler O 2002. The d/dt tool for verification of hybrid systems. Computer Aided Verification: 14th International Conference, CAV 2002 E Brinksma, KG Larsen 365–70 Berlin: Springer
    [Google Scholar]
  7. 7. 
    Fijalkow N, Ouaknine J, Pouly A, Sousa-Pinto J, Worrell J 2019. On the decidability of reachability in linear time-invariant systems. Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control77–86 New York: ACM
    [Google Scholar]
  8. 8. 
    Henzinger TA, Kopke PW, Puri A, Varaiya P 1998. What's decidable about hybrid automata. ? J. Comput. Syst. Sci. 57:94–124
    [Google Scholar]
  9. 9. 
    Brihaye T, Doyen L, Geeraerts G, Ouaknine J, Raskin JF, Worrell J 2011. On reachability for hybrid automata over bounded time. Automata, Languages and Programming: 14th International Conference, CAV 2002 L Aceto, M Henzinger, J Sgall 416–27 Berlin: Springer
    [Google Scholar]
  10. 10. 
    Chen X, Sankaranarayanan S, Abrahám E 2014. Under-approximate flowpipes for non-linear continuous systems. Proceedings of the 14th Conference on Formal Methods in Computer-Aided Design59–66 Berlin: Springer
    [Google Scholar]
  11. 11. 
    Blanchini F. 1999. Set invariance in control. Automatica 35:1747–67
    [Google Scholar]
  12. 12. 
    Rungger M, Tabuada P. 2017. Computing robust controlled invariant sets of linear systems. IEEE Trans. Autom. Control 62:3665–70
    [Google Scholar]
  13. 13. 
    El-Guindy A, Han D, Althoff M 2017. Estimating the region of attraction via forward reachable sets. 2017 American Control Conference1263–70 Piscataway, NJ: IEEE
    [Google Scholar]
  14. 14. 
    Bravo JM, Alamo T, Camacho EF 2006. Robust MPC of constrained discrete-time nonlinear systems based on approximated reachable sets. Automatica 42:1745–51
    [Google Scholar]
  15. 15. 
    Schürmann B, Kochdumper N, Althoff M 2018. Reachset model predictive control for disturbed nonlinear systems. 2018 IEEE Conference on Decision and Control3463–70 Piscataway, NJ: IEEE
    [Google Scholar]
  16. 16. 
    Gruber F, Althoff M. 2019. Scalable robust model predictive control for linear sampled-data systems. 2019 IEEE 58th Conference on Decision and Control438–44 Piscataway, NJ: IEEE
    [Google Scholar]
  17. 17. 
    Combastel C. 2005. A state bounding observer for uncertain non-linear continuous-time systems based on zonotopes. Proceedings of the 44th IEEE Conference on Decision and Control7228–34 Piscataway, NJ: IEEE
    [Google Scholar]
  18. 18. 
    Scott JK, Raimondo DM, Marseglia GR, Braatz RD 2016. Constrained zonotopes: a new tool for set-based estimation and fault detection. Automatica 69:126–36
    [Google Scholar]
  19. 19. 
    Su J, Chen W. 2019. Model-based fault diagnosis system verification using reachability analysis. IEEE Trans. Syst. Man Cybernet. Syst. 49:742–51
    [Google Scholar]
  20. 20. 
    Althoff M, Magdici S. 2016. Set-based prediction of traffic participants on arbitrary road networks. IEEE Trans. Intell. Veh. 1:187–202
    [Google Scholar]
  21. 21. 
    Pereira A, Althoff M. 2018. Overapproximative human arm occupancy prediction for collision avoidance. IEEE Trans. Autom. Sci. Eng. 15:818–31
    [Google Scholar]
  22. 22. 
    Zamani M, Pola G, Mazo M, Tabuada P 2012. Symbolic models for nonlinear control systems without stability assumptions. IEEE Trans. Autom. Control 57:1804–9
    [Google Scholar]
  23. 23. 
    Schürmann B, Althoff M. 2017. Guaranteeing constraints of disturbed nonlinear systems using set-based optimal control in generator space. 20th IFAC World Congress D Dochain, D Henrion, D Peaucelle 11515–22 IFAC-PapersOnLine 50(1) Amsterdam: Elsevier
    [Google Scholar]
  24. 24. 
    Roehm H, Oehlerking J, Woehrle M, Althoff M 2016. Reachset conformance testing of hybrid automata. Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control277–86 New York: ACM
    [Google Scholar]
  25. 25. 
    Roehm H, Oehlerking J, Woehrle M, Althoff M 2019. Model conformance for cyber-physical systems: a survey. ACM Trans. Cyber-Phys. Syst. 3:30
    [Google Scholar]
  26. 26. 
    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]
  27. 27. 
    Chen M, Tomlin CJ. 2018. Hamilton–Jacobi reachability: some recent theoretical advances and applications in unmanned airspace management. Annu. Rev. Control Robot. Auton. Syst. 1:333–58
    [Google Scholar]
  28. 28. 
    Prajna S, Jadbabaie A. 2004. Safety verification of hybrid systems using barrier certificates. Hybrid Systems: Computation and Control: 7th International Workshop, HSCC 2004 R Alur, GJ Pappas 477–92 Berlin: Springer
    [Google Scholar]
  29. 29. 
    Kong H, Bartocci E, Henzinger TA 2018. Reachable set over-approximation for nonlinear systems using piecewise barrier tubes. Computer Aided Verification: 30th International Conference, CAV 2018 H Chockler, G Weissenbacher 449–67 Cham, Switz: Springer
    [Google Scholar]
  30. 30. 
    Girard A, Pappas GJ. 2006. Verification using simulation. Hybrid Systems: Computation and Control: 9th International Workshop, HSCC 2006 JP Hespanha, A Tiwari 272–86 Berlin: Springer
    [Google Scholar]
  31. 31. 
    Donzé A, Maler O. 2007. Systematic simulation using sensitivity analysis. Hybrid Systems: Computation and Control: 10th International Workshop, HSCC 2007 A Bemporad, A Bicchi, G Buttazzo 174–89 Berlin: Springer
    [Google Scholar]
  32. 32. 
    Ramdani N, Meslem N, Candau Y 2008. Reachability analysis of uncertain nonlinear systems using guaranteed set integration. 17th IFAC World Congress8972–77 IFAC Proc. Vol. 41(2) Amsterdam: Elsevier
    [Google Scholar]
  33. 33. 
    Duggirala PS, Mitra S, Viswanathan M 2013. Verification of annotated models from executions. 2013 International Conference on Embedded Software Piscataway, NJ: IEEE https://doi.org/10.1109/EMSOFT.2013.6658604
    [Crossref] [Google Scholar]
  34. 34. 
    Fan C, Kapinski J, Jin X, Mitra S 2016. Locally optimal reach set over-approximation for nonlinear systems. 2016 International Conference on Embedded Software Piscataway, NJ: IEEE https://doi.org/10.1145/2968478.2968482
    [Crossref] [Google Scholar]
  35. 35. 
    Ratschan S, She Z. 2007. Safety verification of hybrid systems by constraint propagation based abstraction refinement. ACM Trans. Embedded Comput. Syst. 6:8–es
    [Google Scholar]
  36. 36. 
    Gao S, Kong S, Clarke E 2013. Satisfiability modulo ODEs. 2013 Formal Methods in Computer-Aided Design105–12 Piscataway, NJ: IEEE
    [Google Scholar]
  37. 37. 
    Frehse G, Althoff M 2019. ARCH19: 6th International Workshop on Applied Verification of Continuous and Hybrid Systems Manchester, UK: EasyChair
    [Google Scholar]
  38. 38. 
    Althoff M, Krogh BH. 2011. Zonotope bundles for the efficient computation of reachable sets. 2011 50th IEEE Conference on Decision and Control and European Control Conference6814–21 Piscataway, NJ: IEEE
    [Google Scholar]
  39. 39. 
    Reißig G. 2007. Convexity of reachable setsof nonlinear ordinary differential equations. Autom. Remote Control 68:1527–43
    [Google Scholar]
  40. 40. 
    Chen X, Sankaranarayanan S, Ábrahám E 2012. Taylor model flowpipe construction for non-linear hybrid systems. 2012 IEEE 33rd Real-Time Systems Symposium183–92 Piscataway, NJ: IEEE
    [Google Scholar]
  41. 41. 
    Althoff M. 2013. Reachability analysis of nonlinear systems using conservative polynomialization and non-convex sets. Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control173–82 New York: ACM
    [Google Scholar]
  42. 42. 
    Kochdumper N, Althoff M. 2020. Constrained polynomial zonotopes. arXiv:2005.08849 [math.CO]
  43. 43. 
    Jaulin L, Kieffer M, Didrit O 2006. Applied Interval Analysis London: Springer
    [Google Scholar]
  44. 44. 
    Kurzhanskiy AA, Varaiya P. 2006. Ellipsoidal toolbox Tech. Rep. UCB/EECS-2006-46 Dep. Electr. Eng. Comput. Sci., Univ. Calif Berkeley:
    [Google Scholar]
  45. 45. 
    Bogomolov S, Forets M, Frehse G, Viry F, Podelski A, Schilling C 2018. Reach set approximation through decomposition with low-dimensional sets and high-dimensional matrices. Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control41–50 New York: ACM
    [Google Scholar]
  46. 46. 
    Avis D, Bremner D, Seidel R 1997. How good are convex hull algorithms. ? Comput. Geom. 7:265–301
    [Google Scholar]
  47. 47. 
    Fukuda K, Liebling TM, Lütolf C 2001. Extended convex hull. Comput. Geom. 20:13–23
    [Google Scholar]
  48. 48. 
    Bremner DD. 1997. On the complexity of vertex and facet enumeration for convex polytopes PhD Thesis, McGill Univ Montreal, Can:.
    [Google Scholar]
  49. 49. 
    Althoff M, Frehse G. 2016. Combining zonotopes and support functions for efficient reachability analysis of linear systems. 2016 IEEE 55th Conference on Decision and Control7439–46 Piscataway, NJ: IEEE
    [Google Scholar]
  50. 50. 
    Kochdumper N, Althoff M. 2019. Sparse polynomial zonotopes: a novel set representation for reachability analysis. arXiv:1901.01780 [cs.SY]
  51. 51. 
    Tran HD, Cai F, Diego ML, Musau P, Johnson TT, Koutsoukos X 2019. Safety verification of cyber-physical systems with reinforcement learning control. ACM Trans. Embedded Comput. Syst. 18:105
    [Google Scholar]
  52. 52. 
    Bak S, Duggirala PS. 2017. Simulation-equivalent reachability of large linear systems with inputs. Computer Aided Verification: 29th International Conference, CAV 2017 R Majumdar, V Kunčak 401–20 Berlin: Springer
    [Google Scholar]
  53. 53. 
    McMullen E. 1970. The maximum numbers of faces of a convex polytope. Mathematika 17:179–84
    [Google Scholar]
  54. 54. 
    Neidinger RD. 2004. Directions for computing truncated multivariate Taylor series. Math. Comput. 74:321–40
    [Google Scholar]
  55. 55. 
    Makino K, Berz M. 2003. Taylor models and other validated functional inclusion methods. Int. J. Pure Appl. Math. 4:379–456
    [Google Scholar]
  56. 56. 
    Duggirala PS, Viswanathan M. 2016. Parsimonious, simulation based verification of linear systems. Computer Aided Verification: 28th International Conference, CAV 2016 S Chaudhuri, A Farzan 477–94 Cham, Switz: Springer
    [Google Scholar]
  57. 57. 
    Botchkarev O, Tripakis S. 2000. Verification of hybrid systems with linear differential inclusions using ellipsoidal approximations. Hybrid Systems: Computation and Control: Third International Workshop, HSCC 2000 N Lynch, BH Krogh 73–88 Berlin: Springer
    [Google Scholar]
  58. 58. 
    Kurzhanski AB, Varaiya P. 2000. Ellipsoidal techniques for reachability analysis. Hybrid Systems: Computation and Control: Third International Workshop, HSCC 2000 N Lynch, BH Krogh 202–14 Berlin: Springer
    [Google Scholar]
  59. 59. 
    Chutinan A, Krogh BH. 2003. Computational techniques for hybrid system verification. IEEE Trans. Autom. Control 48:64–75
    [Google Scholar]
  60. 60. 
    Asarin E, Bournez O, Dang T, Maler O 2000. Approximate reachability analysis of piecewise-linear dynamical systems. Hybrid Systems: Computation and Control: Third International Workshop, HSCC 2000 N Lynch, BH Krogh 20–31 Berlin: Springer
    [Google Scholar]
  61. 61. 
    Girard A. 2005. Reachability of uncertain linear systems using zonotopes. Hybrid Systems: Computation and Control: 8th International Workshop, HSCC 2005 M Morari, L Thiele 291–305 Berlin: Springer
    [Google Scholar]
  62. 62. 
    Althoff M, Stursberg O, Buss M 2010. Computing reachable sets of hybrid systems using a combination of zonotopes and polytopes. Nonlinear Anal. Hybrid Syst. 4:233–49
    [Google Scholar]
  63. 63. 
    Le Guernic C, Girard A 2010. Reachability analysis of linear systems using support functions. Nonlinear Anal. Hybrid Syst. 4:250–62
    [Google Scholar]
  64. 64. 
    Frehse G, Le Guernic C, Donzé A, Cotton S, Ray R et al. 2011. SpaceEx: scalable verification of hybrid systems. Computer Aided Verification: 23rd International Conference, CAV 2011 G Gopalakrishnan, S Qadeer 379–95 Berlin: Springer
    [Google Scholar]
  65. 65. 
    Althoff M, Le Guernic C, Krogh BH 2011. Reachable set computation for uncertain time-varying linear systems. Hybrid Systems: Computation and Control: 8th International Workshop, HSCC 200593–102 Berlin: Springer
    [Google Scholar]
  66. 66. 
    Kühn W. 1998. Rigorously computed orbits of dynamical systems without the wrapping effect. Computing 61:47–67
    [Google Scholar]
  67. 67. 
    Girard A, Le Guernic C, Maler O 2006. Efficient computation of reachable sets of linear time-invariant systems with inputs. Hybrid Systems: Computation and Control: 9th International Workshop, HSCC 2006 JP Hespanha, A Tiwari 257–71 Berlin: Springer
    [Google Scholar]
  68. 68. 
    Han Z, Krogh B. 2004. Reachability analysis of hybrid control systems using reduced-order models. 2004 American Control Conference1183–89 Piscataway, NJ: IEEE
    [Google Scholar]
  69. 69. 
    Han Z, Krogh BH. 2006. Reachability analysis of large-scale affine systems using low-dimensional polytopes. Hybrid Systems: Computation and Control: 9th International Workshop, HSCC 2006 JP Hespanha, A Tiwari 287–301 Berlin: Springer
    [Google Scholar]
  70. 70. 
    Tran HD, Nguyen LV, Xiang W, Johnson TT 2017. Order-reduction abstractions for safety verification of high-dimensional linear systems. Discrete Event Dyn. Syst. 27:443–61
    [Google Scholar]
  71. 71. 
    Bak S, Tran HD, Johnson TT 2019. Numerical verification of affine systems with up to a billion dimensions. Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control23–32 New York: ACM
    [Google Scholar]
  72. 72. 
    Althoff M. 2020. Reachability analysis of large linear systems with uncertain inputs in the Krylov subspace. IEEE Trans. Autom. Control 65:477–92
    [Google Scholar]
  73. 73. 
    Asarin E, Dang T. 2004. Abstraction by projection and application to multi-affine systems. Hybrid Systems: Computation and Control: 7th International Workshop, HSCC 2004 R Alur, GJ Pappas 32–47 Berlin: Springer
    [Google Scholar]
  74. 74. 
    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]
  75. 75. 
    Mitchell IM, Tomlin C. 2003. Overapproximating reachable sets by Hamilton-Jacobi projections. J. Sci. Comput. 19:323–46
    [Google Scholar]
  76. 76. 
    Greenstreet MR, Mitchell I. 1999. Reachability analysis using polygonal projections. Hybrid Systems: Computation and Control: Second International Workshop, HSCC99 FW Vaandrager, JH van Schuppen 103–16 Berlin: Springer
    [Google Scholar]
  77. 77. 
    Chen X, Sankaranarayanan S. 2016. Decomposed reachability analysis for nonlinear systems. 2016 IEEE Real-Time Systems Symposium13–24 Piscataway, NJ: IEEE
    [Google Scholar]
  78. 78. 
    Berz M, Hoffstätter G. 1998. Computation and application of Taylor polynomials with interval remainder bounds. Reliable Comput 4:83–97
    [Google Scholar]
  79. 79. 
    Makino K, Berz M. 1996. Remainder differential algebras and their applications. Computational Differentiation: Techniques, Applications, and Tools M Berz, C Bischof, G Corliss, A Griewank 63–74 Philadelphia: Soc. Ind. Appl. Math.
    [Google Scholar]
  80. 80. 
    Eckmann JP, Malaspinas A, Kamphorst SO 1991. A software tool for analysis in function spaces. Computer Aided Proofs in Analysis KR Meyer, DS Schmidt 147–67 New York: Springer
    [Google Scholar]
  81. 81. 
    Sankaranarayanan S. 2011. Automatic abstraction of non-linear systems using change of bases transformations. Proceedings of the 14th International Conference on Hybrid Systems: Computation and Control143–52 New York: ACM
    [Google Scholar]
  82. 82. 
    Sankaranarayanan S. 2016. Change-of-bases abstractions for non-linear hybrid systems. Nonlinear Anal. Hybrid Syst. 19:107–33
    [Google Scholar]
  83. 83. 
    Henzinger TA, Ho PH, Wong-Toi H 1998. Algorithmic analysis of nonlinear hybrid systems. IEEE Trans. Autom. Control 43:540–54
    [Google Scholar]
  84. 84. 
    Asarin E, Dang T, Girard A 2003. Reachability analysis of nonlinear systems using conservative approximation. Hybrid Systems: Computation and Control: 6th International Workshop, HSCC 2003 O Maler, A Pnueli 20–35 Berlin: Springer
    [Google Scholar]
  85. 85. 
    Asarin E, Dang T, Girard A 2007. Hybridization methods for the analysis of nonlinear systems. Acta Inf 43:451–76
    [Google Scholar]
  86. 86. 
    Lee HSL, Althoff M, Hoelldampf S, Olbrich M, Barke E 2015. Automated generation of hybrid system models for reachability analysis of nonlinear analog circuits. The 20th Asia and South Pacific Design Automation Conference725–30 Piscataway, NJ: IEEE
    [Google Scholar]
  87. 87. 
    Althoff M, Stursberg O, Buss M 2008. Reachability analysis of nonlinear systems with uncertain parameters using conservative linearization. 2008 47th IEEE Conference on Decision and Control4042–48 Piscataway, NJ: IEEE
    [Google Scholar]
  88. 88. 
    Dang T, Maler O, Testylier R 2010. Accurate hybridization of nonlinear systems. Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control11–19 New York: ACM
    [Google Scholar]
  89. 89. 
    Waldron S. 1998. The error in linear interpolation at the vertices of a simplex. SIAM J. Numer. Anal. 35:1191–200
    [Google Scholar]
  90. 90. 
    Han Z, Krogh BH. 2006. Reachability analysis of nonlinear systems using trajectory piecewise linearized models. 2006 American Control Conference1505–10 Piscataway, NJ: IEEE
    [Google Scholar]
  91. 91. 
    Dang T. 2006. Approximate reachability computation for polynomial systems. Hybrid Systems: Computation and Control: 9th International Workshop, HSCC 2006 JP Hespanha, A Tiwari 138–52 Berlin: Springer
    [Google Scholar]
  92. 92. 
    Dang T, Maler O. 1998. Reachability analysis via face lifting. Hybrid Systems: Computation and Control: First International Workshop, HSCC'98 TA Henzinger, S Sastry 96–109 Berlin: Springer
    [Google Scholar]
  93. 93. 
    Dang T, Salinas D. 2009. Image computation for polynomial dynamical systems using the Bernstein expansion. Computer Aided Verification: 21st International Conference, CAV 2009 A Bouajjani, O Maler 219–32 Berlin: Springer
    [Google Scholar]
  94. 94. 
    Angeli D, Sontag ED. 2003. Monotone control systems. IEEE Trans. Autom. Control 48:1684–98
    [Google Scholar]
  95. 95. 
    Ramdani N, Meslem N, Candau Y 2010. Computing reachable sets for uncertain nonlinear monotone systems. Nonlinear Anal. Hybrid Syst. 4:263–78
    [Google Scholar]
  96. 96. 
    Ramdani N, Meslem N, Candau Y 2008. Reachability of uncertain nonlinear systems using a nonlinear hybridization. Hybrid Systems: Computation and Control: 11th International Workshop, HSCC 2008 M Egerstedt, B Mishra 415–28 Berlin: Springer
    [Google Scholar]
  97. 97. 
    Coogan S, Arcak M. 2015. Efficient finite abstraction of mixed monotone systems. Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control58–67 New York: ACM
    [Google Scholar]
  98. 98. 
    Scott JK, Barton PI. 2013. Bounds on the reachable sets of nonlinear control systems. Automatica 49:93–100
    [Google Scholar]
  99. 99. 
    Cross EA, Mitchell IM. 2008. Level set methods for computing reachable sets of systems with differential algebraic equation dynamics. 2008 American Control Conference2260–65 Piscataway, NJ: IEEE
    [Google Scholar]
  100. 100. 
    Mitchell IM, Susuki Y. 2008. Level set methods for computing reachable sets of hybrid systems with differential algebraic equation dynamics. Hybrid Systems: Computation and Control: 11th International Workshop, HSCC 2008 M Egerstedt, B Mishra 630–33 Berlin: Springer
    [Google Scholar]
  101. 101. 
    Dang T, Donze A, Maler O 2004. Verification of analog and mixed-signal circuits using hybrid systems techniques. Formal Methods for Computer Aided Design: 5th International Conference, FMCAD 2004 AJ Hu, AK Martin 21–36 Berlin: Springer
    [Google Scholar]
  102. 102. 
    Althoff M, Krogh BH. 2014. Reachability analysis of nonlinear differential-algebraic systems. IEEE Trans. Autom. Control 59:371–83
    [Google Scholar]
  103. 103. 
    Alur R, Courcoubetis C, Henzinger TA, Ho PH 1993. Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. Hybrid Systems RL Grossman, A Nerode, AP Ravn, H Rischel 209–29 Berlin: Springer
    [Google Scholar]
  104. 104. 
    Bemporad A, Morari M. 1999. Control of systems integrating logic, dynamics, and constraints. Automatica 35:407–27
    [Google Scholar]
  105. 105. 
    Goebel R, Sanfelice RG, Teel AR 2009. Hybrid dynamical systems. IEEE Control Syst. Mag. 29:228–93
    [Google Scholar]
  106. 106. 
    Henzinger T. 1996. The theory of hybrid automata. 11th Annual IEEE Symposium on Logic in Computer Science278–92 Piscataway, NJ: IEEE
    [Google Scholar]
  107. 107. 
    Minopoli S, Frehse G. 2016. From simulation models to hybrid automata using urgency and relaxation. Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control287–96 New York: ACM
    [Google Scholar]
  108. 108. 
    Halbwachs N, Proy YE, Raymond P 1994. Verification of linear hybrid systems by means of convex approximations. Static Analysis: First International Static Analysis Symposium, SAS'94 Le B Charlier 223–37 Berlin: Springer
    [Google Scholar]
  109. 109. 
    Becchi A, Zaffanella E. 2019. Revisiting polyhedral analysis for hybrid systems. Static Analysis: 26th International Symposium, SAS 2019 BY Chang 183–202 Cham, Switz: Springer
    [Google Scholar]
  110. 110. 
    Fränzle M. 1999. Analysis of hybrid systems: an ounce of realism can save an infinity of states. Computer Science Logic: 13th International Workshop, CSL99 J Flum, M Rodriguez-Artalejo 126–39 Berlin: Springer
    [Google Scholar]
  111. 111. 
    Cousot P, Cousot R. 1977. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages238–52 New York: ACM
    [Google Scholar]
  112. 112. 
    Frehse G. 2008. PHAVer: algorithmic verification of hybrid systems past HyTech. Int. J. Softw. Tools Technol. Transf. 10:263–79
    [Google Scholar]
  113. 113. 
    Donzé A, Frehse G. 2013. Modular, hierarchical models of control systems in SpaceEx. 2013 European Control Conference4244–51 Piscataway, NJ: IEEE
    [Google Scholar]
  114. 114. 
    Le Guernic C, Girard A 2009. Reachability analysis of hybrid systems using support functions. Computer Aided Verification: 21st International Conference, CAV 2009 A Bouajjani, O Maler 540–54 Berlin: Springer
    [Google Scholar]
  115. 115. 
    Frehse G, Kateja R, Le Guernic C 2013. Flowpipe approximation and clustering in space-time. Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control203–12 New York: ACM
    [Google Scholar]
  116. 116. 
    Cattaruzza D, Abate A, Schrammel P, Kroening D 2015. Unbounded-time analysis of guarded LTI systems with inputs by abstract acceleration. International Static Analysis Symposium: 22nd International Symposium, SAS 2015 S Blazy, T Jensen 312–31 Berlin: Springer
    [Google Scholar]
  117. 117. 
    Althoff D, Althoff M, Scherer S 2015. Online safety verification of trajectories for unmanned flight with offline computed robust invariant sets. 2015 IEEE/RSJ International Conference on Intelligent Robots and Systems3470–77 Piscataway, NJ: IEEE
    [Google Scholar]
  118. 118. 
    Hobbs K, Heidlauf P, Collins A, Bak S 2018. Space debris collision detection using reachability. ARCH18: 5th International Workshop on Applied Verification of Continuous and Hybrid Systems G Frehse 218–28 Manchester, UK: EasyChair
    [Google Scholar]
  119. 119. 
    Gupta S, Krogh BH, Rutenbar RA 2004. Towards formal verification of analog designs. IEEE/ACM International Conference on Computer Aided Design, 2004210–17 Piscataway, NJ: IEEE
    [Google Scholar]
  120. 120. 
    Frehse G, Krogh BH, Rutenbar RA 2006. Verifying analog oscillator circuits using forward/backward abstraction refinement. Proceedings of the Design Automation and Test in Europe Conference257–62 Piscataway, NJ: IEEE
    [Google Scholar]
  121. 121. 
    Althoff M, Rajhans A, Krogh BH, Yaldiz S, Li X, Pileggi L 2013. Formal verification of phase-locked loops using reachability analysis and continuization. Commun. ACM 56:97–104
    [Google Scholar]
  122. 122. 
    Stursberg O, Fehnker A, Han Z, Krogh BH 2004. Verification of a cruise control system using counterexample-guided search. Control Eng. Pract. 12:1269–78
    [Google Scholar]
  123. 123. 
    Althoff M, Althoff D, Wollherr D, Buss M 2010. Safety verification of autonomous vehicles for coordinated evasive maneuvers. 2010 IEEE Intelligent Vehicles Symposium1078–83 Piscataway, NJ: IEEE
    [Google Scholar]
  124. 124. 
    Heß D, Althoff M, Sattel T 2014. Formal verification of maneuver automata for parameterized motion primitives. 2014 IEEE/RSJ International Conference on Intelligent Robots and Systems1474–81 Piscataway, NJ: IEEE
    [Google Scholar]
  125. 125. 
    Althoff M, Dolan JM. 2014. Online verification of automated road vehicles using reachability analysis. IEEE Trans. Robot. 30:903–18
    [Google Scholar]
  126. 126. 
    Söntges S, Althoff M. 2018. Computing the drivable area of autonomous road vehicles in dynamic road scenes. IEEE Trans. Intell. Transp. Syst. 19:1855–66
    [Google Scholar]
  127. 127. 
    Chen YC, Domínguez-García AD. 2012. A method to study the effect of renewable resource variability on power system dynamics. IEEE Trans. Power Syst. 27:1978–89
    [Google Scholar]
  128. 128. 
    Villegas Pico HN, Aliprantis DC 2014. Voltage ride-through capability verification of wind turbines with fully-rated converters using reachability analysis. IEEE Trans. Energy Convers. 29:392–405
    [Google Scholar]
  129. 129. 
    Althoff M. 2014. Formal and compositional analysis of power systems using reachable sets. IEEE Trans. Power Syst. 29:2270–80
    [Google Scholar]
  130. 130. 
    El-Guindy A, Han D, Althoff M 2016. Formal analysis of drum-boiler units to maximize the load-following capabilities of power plants. IEEE Trans. Power Syst. 31:4691–702
    [Google Scholar]
  131. 131. 
    Li Y, Zhang P, Luh PB 2018. Formal analysis of networked microgrids dynamics. IEEE Trans. Power Syst. 33:3418–27
    [Google Scholar]
  132. 132. 
    Lengagne S, Ramdani N, Fraisse P 2011. Planning and fast replanning safe motions for humanoid robots. IEEE Trans. Robot. 27:1095–106
    [Google Scholar]
  133. 133. 
    Liu SB, Roehm H, Heinzemann C, Lütkebohle I, Oehlerking J, Althoff M 2017. Provably safe motion of mobile robots in human environments. 2017 IEEE/RSJ International Conference on Intelligent Robots and Systems1351–57 Piscataway, NJ: IEEE
    [Google Scholar]
  134. 134. 
    Althoff M, Giusti A, Liu SB, Pereira A 2019. Effortless creation of safe robots from modules through self-programming and self-verification. Sci. Robot. 4:eaaw1924
    [Google Scholar]
  135. 135. 
    Batt G, Belta C, Weiss R 2007. Model checking genetic regulatory networks with parameter uncertainty. Hybrid Systems: Computation and Control: 10th International Workshop, HSCC 2007 A Bemporad, A Bicchi, G Buttazzo 61–75 Berlin: Springer
    [Google Scholar]
  136. 136. 
    Dang T, Le Guernic C, Maler O 2009. Computing reachable states for nonlinear biological models. Computational Methods in Systems Biology: 7th International Conference, CMSB 2009 P Degano, R Gorrieri 126–41 Berlin: Springer
    [Google Scholar]
  137. 137. 
    Kaynama S, Maidens JN, Oishi M, Mitchell IM, Dumont GA 2012. Computing the viability kernel using maximal reachable sets. Proceedings of the 15th ACM International Conference on Hybrid Systems: Computation and Control55–64 New York: ACM
    [Google Scholar]
  138. 138. 
    Dang T, Dreossi T, Fanchon E, Maler O, Piazza C, Rocca A 2019. Set-based analysis for biological modeling. Automated Reasoning for Systems Biology and Medicine P Liò, P Zuliani 157–89 Cham, Switz: Springer
    [Google Scholar]
/content/journals/10.1146/annurev-control-071420-081941
Loading
/content/journals/10.1146/annurev-control-071420-081941
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