×

Construction of parametric barrier functions for dynamical systems using interval analysis. (English) Zbl 1357.93046

Summary: Recently, barrier certificates have been introduced to prove the safety of continuous or hybrid dynamical systems. A barrier certificate needs to exhibit some barrier function, which partitions the state space in two subsets: the safe subset in which the state can be proved to remain and the complementary subset containing some unsafe region. This approach does not require any reachability analysis, but needs the computation of a valid barrier function, which is difficult when considering general nonlinear systems and barriers. This paper presents a new approach for the construction of barrier functions for nonlinear dynamical systems. The proposed technique searches for the parameters of a parametric barrier function using interval analysis. Complex dynamics with bounded perturbations can be considered without needing any relaxation of the constraints to be satisfied by the barrier function.

MSC:

93C10 Nonlinear systems in control theory
93C15 Control/observation systems governed by ordinary differential equations
65G30 Interval and finite arithmetic
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Ahmadi, A. A.; Krstic, M.; Parrilo, P. A., A globally asymptotically stable polynomial vector field with no polynomial Lyapunov function, (CDC and ECC (2011)), 7579-7580
[2] Araya, I.; Trombettoni, G.; Neveu, B.; Chabert, G., Upper bounding in inner regions for global optimization under inequality constraints, Journal of Global Optimization, 60, 2, 145-164 (2012) · Zbl 1312.90057
[3] Aréchiga, N.; Kapinski, J.; Deshmukh, J. V.; Platzer, A.; Krogh, B., Forward invariant cuts to simplify proofs of safety, (ICES (2015), IEEE Press), 227-236
[4] Asarin, E.; Bournez, O.; Dang, T.; Maler, O., Approximate reachability analysis of piecewise-linear dynamical systems, (HSCC (2000), Springer), 20-31 · Zbl 0938.93502
[5] Barrett, C.; Tinelli, C., Satisfiability modulo theories, (Clarke, E.; Henzinger, T.; Veith, H., Handbook of model checking (2017), Springer)
[6] Bellman, R. E.; Cooke, K. L., Differential-difference equations (1963), RAND Corporation
[7] Benhamou, F.; Goualard, F., Universally quantified interval constraints, (CP (2000), Springer), 67-82 · Zbl 1044.68738
[8] Chabert, G.; Jaulin, L., Contractor programming, Artificial Intelligence, 173, 11, 1079-1100 (2009) · Zbl 1191.68628
[9] Chen, X.; Abrahám, E.; Sankaranarayanan, S., Taylor model flowpipe construction for non-linear hybrid systems, (RTSS (2012), IEEE), 183-192
[10] Chutinan, A.; Krogh, B. H., Verification of polyhedral-invariant hybrid automata using polygonal flow pipe approximations, (HSCC (1999), Springer), 76-90 · Zbl 0954.93020
[11] Collins, G. E.; Hong, H., Partial cylindrical algebraic decomposition for quantifier elimination, Journal of Symbolic Computation, 12, 3, 299-328 (1991) · Zbl 0754.68063
[12] Dai, L.; Gan, T.; Xia, B.; Zhan, N., Barrier certificates revisited, Journal of Symbolic Computation (2016)
[13] Frehse, G.; Le Guernic, C.; Donzé, A.; Cotton, S.; Ray, R.; Lebeltel, O., SpaceEx: Scalable verification of hybrid systems, (CAV (2011), Springer), 379-395
[14] Gao, S.; Kong, S.; Clarke, E. M., dReal: An SMT solver for nonlinear theories over the reals, (CADE. CADE, LNCS, vol. 7898 (2013), Springer), 208-214 · Zbl 1381.68268
[15] Genesio, R.; Tartaglia, M.; Vicino, A., On the estimation of asymptotic stability regions: State of the art and new proposals, Transaction on Automatic Control, 30, 8, 747-755 (1985) · Zbl 0568.93054
[17] Gulwani, S.; Tiwari, A., Constraint-based approach for analysis of hybrid systems, (CAV (2008), Springer), 190-203 · Zbl 1155.68437
[18] Huth, M., Logic in computer science: Modelling and reasoning about systems (2004), Cambridge University Press · Zbl 1073.68001
[19] Jaulin, L.; Kieffer, M.; Didrit, O.; Walter, É., Applied interval analysis (2001), Springer
[20] Jaulin, L.; Walter, É., Guaranteed tuning, with application to robust control and motion planning, Automatica, 32, 8, 1217-1221 (1996) · Zbl 0875.93232
[21] Kapinski, J.; Deshmukh, J. V.; Sankaranarayanan, S.; Arechiga, N., Simulation-guided lyapunov analysis for hybrid dynamical systems, (HSCC (2014), ACM), 133-142 · Zbl 1362.93108
[23] Papachristodoulou, A.; Prajna, S., On the construction of Lyapunov functions using the sum of squares decomposition, (CDC, Vol. 3 (2002)), 3482-3487
[24] Papachristodoulou, A.; Prajna, S., Analysis of non-polynomial systems using the SoS decomposition, (Positive Polynomials in Control (2005), Springer), 23-43 · Zbl 1138.93391
[25] Parrilo, P. A., Semidefinite programming relaxations for semialgebraic problems, Mathematical Programming, 96, 2, 293-320 (2003) · Zbl 1043.14018
[26] Platzer, A., Differential dynamic logic for verifying parametric hybrid systems, (TABLEAUX. TABLEAUX, LNCS, vol. 4548 (2007), Springer), 216-232 · Zbl 1132.68478
[27] Platzer, A., Logic analysis of hybrid systems (2010), Springer-Verlag
[28] Prajna, S., Optimization-based methods for nonlinear and hybrid systems verification (2005), California Institute of Technology: California Institute of Technology Pasadena, California, (Ph.D. thesis)
[29] Prajna, S., Barrier certificates for nonlinear model validation, Automatica, 42, 1, 117-126 (2006) · Zbl 1121.93007
[30] Prajna, S.; Jadbabaie, A., Safety verification of hybrid systems using barrier certificates, (HSCC (2004), Springer), 477-492 · Zbl 1135.93317
[31] Prajna, S.; Rantzer, A., Primal-dual tests for safety and reachability, (HSCC. HSCC, LNCS, vol. 3414 (2005), Springer-Verlag), 542-556 · Zbl 1078.93507
[32] Ratschan, S., Efficient solving of quantified inequality constraints over the real numbers, Transaction on Computational Logic, 7, 4, 723-748 (2006) · Zbl 1367.68270
[35] Rebiha, R.; Matringe, N.; Moura, A. V., Transcendental inductive invariants generation for non-linear differential and hybrid systems, (HSCC (2012), ACM), 25-34 · Zbl 1362.68153
[36] Sankaranarayanan, S.; Sipma, H. B.; Manna, Z., Constructing invariants for hybrid systems, (HSCC (2004), Springer), 539-554 · Zbl 1135.93322
[37] Sloth, C.; Pappas, G. J.; Wisniewski, R., Compositional safety analysis using barrier certificates, (HSCC (2012), ACM), 15-24 · Zbl 1362.68185
[38] Sun, Z.; Ge, S. S.; Lee, T. H., Controllability and reachability criteria for switched linear systems, Automatica, 38, 5, 775-786 (2002) · Zbl 1031.93041
[39] Tiwari, A., Approximate reachability for linear systems, (HSCC (2003), Springer), 514-525 · Zbl 1032.93518
[40] Vaněček, A.; Čelikovskỳ, S., Control systems: from linear analysis to synthesis of chaos (1996), Prentice Hall · Zbl 0874.93006
[41] Yang, Z.; Lin, W.; Wu, M., Exact safety verification of hybrid systems based on bilinear SoS representation, Transaction on Embedded Computing Systems, 14, 1 (2015)
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.