×

Exact safety verification of hybrid systems using sums-of-squares representation. (English) Zbl 1343.93051

Summary: In this paper we discuss how to generate inductive invariants for safety verification of hybrid systems. A hybrid symbolic-numeric method is presented to compute inequality inductive invariants of the given systems. A numerical invariant of the given system can be obtained by solving a parameterized polynomial optimization problem via sum-of-squares (SOS) relaxation. And a method based on Gauss-Newton refinement and rational vector recovery is used to obtain the invariants with rational coefficients, which exactly satisfy the conditions of invariants. Several examples are given to illustrate our algorithm.

MSC:

93C30 Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems)
90C22 Semidefinite programming
PDFBibTeX XMLCite
Full Text: DOI arXiv Link

References:

[1] Henzinger, T., The theory of hybrid automata, 278-292 (1996)
[2] Alur R, Courcoubetis C, Halbwachs N, et al. The algorithmic analysis of hybrid systems. Theor Comput Sci, 1995, 1: 3-34 · Zbl 0874.68206 · doi:10.1016/0304-3975(94)00202-T
[3] Wang Y, Wang W, Liu G. Stability of linear discrete switched systems with delays based on average dwell time method. Sci China Inf Sci, 2010, 53: 1216-1223 · Zbl 1497.93183 · doi:10.1007/s11432-010-0115-8
[4] Feng W, Zhang J. Input-to-state stability of switched nonlinear systems. Sci China Inf Sci, 2008, 51: 1992-2004 · Zbl 1291.93284 · doi:10.1007/s11432-008-0161-7
[5] Chutinan A, Krogh B H. Computational techniques for hybrid system verification. IEEE Trans Automat Contr, 2003, 48: 64-75 · Zbl 1364.93457 · doi:10.1109/TAC.2002.806655
[6] Lafferriere G, Pappas G J, Yovine S. Symbolic reachability computations for families of linear vector fields. J Symb Comput, 2001, 32: 231-253 · Zbl 0983.93004 · doi:10.1006/jsco.2001.0472
[7] Tiwari, A., Approximate reachability for linear systems, 514-525 (2003) · Zbl 1032.93518 · doi:10.1007/3-540-36580-X_37
[8] Platzer A, Clarke E M. Computing differential invariants of hybrid systems as fixedpoints. Form Method Syst Des, 2009, 35: 98-120 · Zbl 1180.93024 · doi:10.1007/s10703-009-0079-8
[9] Prajna S. Optimization-based methods for nonlinear and hybrid systems verification. Dissertation of Doctoral Degree. California Institute of Technology, 2005
[10] Prajna, S.; Jadbabaie, A., Safety verification of hybrid systems using barrier certificates, 271-274 (2004) · Zbl 1135.93317
[11] Sankaranarayanan S, Sipma H, Manna Z. Constructing invariants for hybrid systems. Form Method Syst Des, 2008, 32: 25-55 · Zbl 1133.68365 · doi:10.1007/s10703-007-0046-1
[12] Sankaranarayanan, S., Automatic invariant generation for hybrid systems using ideal fixed points, 221-230 (2010) · Zbl 1360.34082
[13] Rodríguez-Carbonell E, Tiwari A. Generating polynomial invariants for hybrid systems. In: Proceedings of the International Workshop on Hybrid Systems: Computation and Control, Zurich, 2005. 5 590-605 · Zbl 1078.93026
[14] Gulwani, S.; Tiwari, A., Constraint-based approach for analysis of hybrid systems, 190-203 (2008) · Zbl 1155.68437 · doi:10.1007/978-3-540-70545-1_18
[15] Liu, J.; Zhan, N. J.; Zhao, H. J., Computing semi-algebraic invariants for polynomial dynamical systems, 97-106 (2011)
[16] Matringe, N.; Moura, A. V.; Rebiha, R., Morphisms for non-trivial non-linear invariant generation for algebraic hybrid systems, 445-449 (2009) · Zbl 1237.93090 · doi:10.1007/978-3-642-00602-9_32
[17] Platzer A. Differential-algebraic dynamic logic for differential-algebraic programs. J Logic Comput, 2007, 20: 309-352 · Zbl 1191.03024 · doi:10.1093/logcom/exn070
[18] Platzer A. Differential dynamic logic for hybrid systems. J Autom Reasoning, 2008, 41: 143-189 · Zbl 1181.03035 · doi:10.1007/s10817-008-9103-8
[19] Sturm, T.; Tiwari, A., Verification and synthesis using real quantifier elimination, 329-336 (2011) · Zbl 1323.68385
[20] Tiwari, A.; Khanna, G., Nonlinear systems: approximating reach sets, 600-614 (2004) · Zbl 1135.93318 · doi:10.1007/978-3-540-24743-2_40
[21] Wu, M.; Yang, Z. F., Generating invariants of hybrid systems via sums-of-squares of polynomials with rational coefficients, 104-111 (2011) · Zbl 1345.65046
[22] Kaltofen E, Li B, Yang Z F, et al. Exact certification in global polynomial optimization via sums-of-squares of rational functions with rational coefficients. J Symb Comput, 2012, 47: 1-15 · Zbl 1229.90115 · doi:10.1016/j.jsc.2011.08.002
[23] Platzer, A.; Clarke, E. M., The image computation problem in hybrid systems model checking, 473-486 (2007) · Zbl 1221.93118 · doi:10.1007/978-3-540-71493-4_37
[24] Talky, A.; Tiwari, A., Deductive verification of continuous dynamical systems, 383-394 (2009) · Zbl 1248.68336
[25] Brown C W. QEPCAD B: a program for computing with semi-algebraic sets using CADs. ACM SIGSAM Bull, 2003, 37: 97-108 · Zbl 1083.68148 · doi:10.1145/968708.968710
[26] Xia B C. DISCOVERER: a tool for solving semi-algebraic systems. ACM Commun Comput Algebr, 2007, 41: 102-103 · doi:10.1145/1358190.1358197
[27] Lasserre J B. Moments, Positive Polynomials and Their Applications. Imperial College Press. 2010 · Zbl 1211.90007
[28] Prajna, S.; Papachristodoulou, A.; Seiler, P.; etal., SOSTOOLS: sum of squares optimization toolbox for MATLAB (2004)
[29] Löberg, J., YALMIP: a toolbox for modeling and optimization in MATLAB, 284-289 (2004)
[30] Sturm J F. Using SeDuMi 1.02, a MATLAB toolbox for optimization over symmetric cones. Optim Method Softw, 1999, 12: 625-653 · Zbl 0973.90526 · doi:10.1080/10556789908805766
[31] Laggards J C. The computational complexity of simultaneous diophantine approximation problems. SIAM J Comput, 1985, 14: 196-209 · Zbl 0563.10025 · doi:10.1137/0214016
[32] Ranchman S, She Z K. Safety verification of hybrid systems by constraint propagation-based abstraction refinement. ACM Trans Embed Comput Syst, 2007, 6: 573-589
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.