Previous Articles    

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

LIN Wang1,2, YANG Zhengfeng2, DING Zuohua1   

  1. 1. School of Information Science and Technology, Zhejiang Sci-Tech University, Hangzhou 310018, China; 2. Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai 200062, China
  • Received:2021-04-19 Revised:2021-07-14 Published:2022-06-20

LIN Wang, YANG Zhengfeng, DING Zuohua. Reachable Set Estimation and Safety Verification of Nonlinear Systems via Iterative Sums of Squares Programming[J]. Journal of Systems Science and Complexity, 2022, 35(3): 1154-1172.

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 Lyapunovlike 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 overapproximation 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.
[1] Alur R, Formal verification of hybrid systems, Proceedings of the International Conference on Embedded Software (EMSOFT), IEEE, 2011, 273-278.
[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.
[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.
[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.
[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.
[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.
[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.
[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.
[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.
[10] Alur R, Courcoubetis C, Halbwachs N, et al., The algorithmic analysis of hybrid systems, Theoretical Computer Science, 1995, 138(1):3-34.
[11] Sankaranarayanan S, Sipma H, and Manna Z, Constructing invariants for hybrid systems, Formal Methods in System Design, 2008, 32:25-55.
[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.
[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.
[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.
[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.
[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.
[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.
[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.
[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.
[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.
[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.
[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.
[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.
[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.
[25] Holmes P, Kousik S, Mohan S, et al., Convex estimation of the α-confidence reachable set for systems with parametric uncertainty, 2016 IEEE 55th Conference on Decision and Control (CDC), IEEE, 2016, 4097-4103.
[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.
[27] Yin H, Packard A, Arcak M, et al., Reachability analysis using dissipation inequalities for uncertain nonlinear systems, Systems&Control Letters, 2020, 142:104736.
[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.
[29] Parrilo P, Structured semidefinite programs and semialgebraic geometry methods in robustness and optimization, Ph.D. thesis, California Institute of Technology, 2000.
[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.
[31] Stephen Boyd E F, El Ghaoui L, and Balakrishnan V, Linear Matrix Inequalities in Systems and Control Theory, SIAM, Philadelphia, 1994.
[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.
[33] Chen X, Abrahá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.
[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.
[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.
[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.
No related articles found!
Viewed
Full text


Abstract