SpringerLink
Log in

Reachable Set Estimation and Safety Verification of Nonlinear Systems via Iterative Sums of Squares Programming

  • Published:
Journal of Systems Science and Complexity Aims and scope Submit manuscript

Abstract

In this paper, the problems of forward reachable set estimation and safety verification of uncertain nonlinear systems with polynomial dynamics are addressed. First, an iterative sums of squares (SOS) programming approach is developed for reachable set estimation. It characterizes the over-approximations of the forward reachable sets by sub-level sets of time-varying Lyapunov-like functions that satisfy an invariance condition, and formulates the problem of searching for the Lyapunov-like functions as a bilinear SOS program, which can be solved via an iterative algorithm. To make the over-approximation tight, the proposed approach seeks to minimize the volume of the over-approximation set with a desired shape. Then, the reachable set estimation approach is extended for safety verification, via explicitly encoding the safety constraint such that the Lyapunov-like functions guarantee both reaching and avoidance. The efficiency of the presented method is illustrated by some numerical examples.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
EUR 32.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or Ebook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (France)

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Alur R, Formal verification of hybrid systems, Proceedings of the International Conference on Embedded Software (EMSOFT), IEEE, 2011, 273–278.

    Google Scholar 

  2. Mitchell I and Tomlin C J, Level set methods for computation in hybrid systems, Proceedings of the International Workshop on Hybrid Systems: Computation and Control, Springer, 2000, 310–323.

    Chapter  Google Scholar 

  3. Asarin E, Bournez O, Dang T, et al., Approximate reachability analysis of piecewise-linear dynamical systems, Proceedings of the International Workshop on Hybrid Systems: Computation and Control, Springer, 2000, 20–31.

    Chapter  Google Scholar 

  4. Kurzhanskiy A A and Varaiya P, Ellipsoidal techniques for reachability analysis of discrete-time linear systems, IEEE Transactions on Automatic Control, 2007, 52(1): 26–38.

    Article  MathSciNet  Google Scholar 

  5. Girard A, Reachability of uncertain linear systems using zonotopes, Proceedings of the 8th International Workshop on Hybrid Systems: Computation and Control, 2005, 291–305.

    Chapter  Google Scholar 

  6. Stursberg O and Krogh B H, Efficient representation and computation of reachable sets for hybrid systems, Proceedings of the 6th International Workshop on Hybrid Systems: Computation and Control, Springer, 2003, 482–497.

    Chapter  Google Scholar 

  7. Makino K and Berz M, Taylor models and other validated functional inclusion methods, International Journal of Pure and Applied Mathematics, 2003, 6: 239–316.

    MathSciNet  MATH  Google Scholar 

  8. Chen X, Abraham E, and Sankaranarayanan S, Taylor model flowpipe construction for non-linear hybrid systems, Proceedings of the IEEE 33rd Real-Time Systems Symposium, IEEE, 2012, 183–192.

    Google Scholar 

  9. Althoff M, Reachability analysis of nonlinear systems using conservative polynomialization and non-convex sets, Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control, 2013, 173–182.

    MATH  Google Scholar 

  10. Alur R, Courcoubetis C, Halbwachs N, et al., The algorithmic analysis of hybrid systems, Theoretical Computer Science, 1995, 138(1): 3–34.

    Article  MathSciNet  Google Scholar 

  11. Sankaranarayanan S, Sipma H, and Manna Z, Constructing invariants for hybrid systems, Formal Methods in System Design, 2008, 32: 25–55.

    Article  Google Scholar 

  12. Prajna S, Jadbabaie A, and Pappas G, A framework for worst-case and stochastic safety verification using barrier certificates, IEEE Transactions on Automatic Control, 2007, 52(8): 1415–1429.

    Article  MathSciNet  Google Scholar 

  13. Kong H, He F, Song X, et al., Exponential-condition-based barrier certificate generation for safety verification of hybrid systems, Proceedings of the 25th International Conference on Computer Aided Verification (CAV), Springer, 2013, 242–257.

    Chapter  Google Scholar 

  14. Liu J, Zhan N, and Zhao H, Computing semi-algebraic invariants for polynomial dynamical systems, Proceedings of the International Conference on Embedded Software (EMSOFT), ACM, 2011, 97–106.

    Chapter  Google Scholar 

  15. Kong H, Bartocci E, and Henzinger T A, Reachable set over-approximation for nonlinear systems using piecewise barrier tubes, Proceedings of the 30th International Conference on Computer Aided Verification, 2018, 449–467.

    Chapter  Google Scholar 

  16. Bouissou O, Chapoutot A, Djaballah A, et al., Computation of parametric barrier functions for dynamical systems using interval analysis, Proceedings of the IEEE 53rd Annual Conference on Decision and Control (CDC), IEEE, 2014, 753–758.

    Chapter  Google Scholar 

  17. Majumdar A and Tedrake R, Funnel libraries for real-time robust feedback motion planning, The International Journal of Robotics Research, 2017, 36(8): 947–982.

    Article  Google Scholar 

  18. Tobenkin M M, Manchester I R, and Tedrake R, Invariant funnels around trajectories using sum-of-squares programming, IFAC Proceedings Volumes, 2011, 44(1): 9218–9223.

    Article  Google Scholar 

  19. Majumdar A, Ahmadi A A, and Tedrake R, Control design along trajectories with sums of squares programming, 2013 IEEE International Conference on Robotics and Automation, IEEE, 2013, 4054–4061.

    Chapter  Google Scholar 

  20. Xue B, Fränzle M, and Zhan N, Inner-approximating reachable sets for polynomial systems with time-varying uncertainties, IEEE Transactions on Automatic Control, 2019, 65(4): 1468–1483.

    Article  MathSciNet  Google Scholar 

  21. Xue B, Wang Q, Zhan N, et al., Robust invariant sets generation for state-constrained perturbed polynomial systems, Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, 2019, 128–137.

    Google Scholar 

  22. Jones M and Peet M M, Relaxing the hamilton jacobi bellman equation to construct inner and outer bounds on reachable sets, 2019 IEEE 58th Conference on Decision and Control (CDC), IEEE, 2019, 2397–2404.

    Chapter  Google Scholar 

  23. Henrion D and Korda M, Convex computation of the region of attraction of polynomial control systems, IEEE Transactions on Automatic Control, 2013, 59(2): 297–312.

    Article  MathSciNet  Google Scholar 

  24. Majumdar A, Vasudevan R, Tobenkin M M, et al., Convex optimization of nonlinear feedback controllers via occupation measures, The International Journal of Robotics Research, 2014, 33(9): 1209–1230.

    Article  Google Scholar 

  25. Holmes P, Kousik S, Mohan S, et al., Convex estimation of the a-confidence reachable set for systems with parametric uncertainty, 2016 IEEE 55th Conference on Decision and Control (CDC), IEEE, 2016, 4097–4103.

    Chapter  Google Scholar 

  26. She Z and Li M, Over- and under-approximations of reachable sets with series representations of evolution functions, IEEE Trans. Autom. Control, 2021, 66(3): 1414–1421.

    Article  MathSciNet  Google Scholar 

  27. Yin H, Packard A, Arcak M, et al., Reachability analysis using dissipation inequalities for uncertain nonlinear systems, Systems & Control Letters, 2020, 142: 104736.

    Article  MathSciNet  Google Scholar 

  28. Xue B, Easwaran A, Cho N, et al., Reach-avoid verification for nonlinear systems based on boundary analysis, IEEE Trans. Autom. Control, 2017, 62(7): 3518–3523.

    Article  MathSciNet  Google Scholar 

  29. Parrilo P, Structured semidefinite programs and semialgebraic geometry methods in robustness and optimization, Ph.D. thesis, California Institute of Technology, 2000.

    Google Scholar 

  30. Shen L, Wu M, Yang Z, et al., Generating exact nonlinear ranking functions by symbolic-numeric hybrid method, Journal of Systems Science & Complexity, 2013, 26(2): 291–301.

    Article  MathSciNet  Google Scholar 

  31. Stephen Boyd E F, El Ghaoui L, and Balakrishnan V, Linear Matrix Inequalities in Systems and Control Theory, SIAM, Philadelphia, 1994.

    Book  Google Scholar 

  32. Jones M and Peet M M, Using SOS and sublevel set volume minimization for estimation of forward reachable sets, IFAC-PapersOnLine, 2019, 52(16): 484–489.

    Article  Google Scholar 

  33. Chen X, Ábrahám E, and Sankaranarayanan S, Flow*: An analyzer for non-linear hybrid systems, Proceedings of the 25th International Conference on Computer Aided Verification, CAV2013, 2013, 258–263.

    Chapter  Google Scholar 

  34. Löfberg J, YALMIP: A toolbox for modeling and optimization in Matlab, Proceedings of the CACSD, Taipei, Taiwan, 2004, http://control.ee.ethz.ch/~joloef/yalmip.php.

    Google Scholar 

  35. Sturm J F, Using SeDuMi 1.02, a Matlab toolbox for optimization over symmetric cones, Optimization Methods and Software, 1999, 11/12: 625–653.

    Article  MathSciNet  Google Scholar 

  36. Prajna S and Rantzer A, Primal-dual tests for safety and reachability, Proceedings of the 8th International Workshop on Hybrid Systems: Computation and Control, 2005, 542–556.

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Information Science and Technology, Zhejiang Sci-Tech University, Hangzhou, 310018, China

    Wang Lin & Zuohua Ding

  2. Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, 200062, China

    Wang Lin & Zhengfeng Yang

Authors
  1. Wang Lin
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Zhengfeng Yang
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Zuohua Ding
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Zhengfeng Yang.

Additional information

This research was supported in part by the National Natural Science Foundation of China under Grant Nos. 12171159 and 61772203, and in part by the Zhejiang Provincial Natural Science Foundation of China under Grant No. LY20F020020.

This paper was recommended for publication by Editor FENG Ruyong.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Lin, W., Yang, Z. & Ding, Z. Reachable Set Estimation and Safety Verification of Nonlinear Systems via Iterative Sums of Squares Programming. J Syst Sci Complex 35, 1154–1172 (2022). https://doi.org/10.1007/s11424-022-1121-9

Download citation

  • Received:

  • Revised:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s11424-022-1121-9

Keywords

Search

Navigation