1932
0
  1. Home
  2. A-Z Publications
  3. Annual Review of Control, Robotics, and Autonomous Systems
  4. Volume 4, 2021
  5. Article

Annual Review of Control, Robotics, and Autonomous Systems

Volume 4, 2021

Set Propagation Techniques for Reachability Analysis

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.

Keyword(s): continuous and hybrid systems, reachability analysis, rigorous approximation, set representations
Loading

Article metrics loading...

/content/journals/10.1146/annurev-control-071420-081941
2021-05-03
2024-04-27
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
  2. 2. 
    Baier C, Katoen JP. 2008. Principles of Model Checking Cambridge, MA: MIT Press
  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
  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
  44. 44. 
    Kurzhanskiy AA, Varaiya P. 2006. Ellipsoidal toolbox Tech. Rep. UCB/EECS-2006-46 Dep. Electr. Eng. Comput. Sci., Univ. Calif Berkeley:
  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:.
  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
Set Propagation Techniques for Reachability Analysis
Annual Review of Control, Robotics, and Autonomous Systems 4, 369 (2021); https://doi.org/10.1146/annurev-control-071420-081941
/content/journals/10.1146/annurev-control-071420-081941
/content/journals/10.1146/annurev-control-071420-081941
Loading

Data & Media loading...

  • Article Type: Review Article

Most Cited Most Cited RSS feed

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