×

Abstraction based verification of stability of polyhedral switched systems. (English) Zbl 1441.93225

Summary: This paper presents a novel abstraction technique for analyzing Lyapunov and asymptotic stability of polyhedral switched systems. A polyhedral switched system is a hybrid system in which the continuous dynamics is specified by polyhedral differential inclusions, the invariants and guards are specified by polyhedral sets and the switching between the modes do not involve reset of variables. A finite state weighted graph abstracting the polyhedral switched system is constructed from a finite partition of the state-space, such that the satisfaction of certain graph conditions, such as the absence of cycles with product of weights on the edges greater than (or equal) to 1, implies the stability of the system. However, the graph is in general conservative and hence, the violation of the graph conditions does not imply instability. If the analysis fails to establish stability due to the conservativeness in the approximation, a counterexample (cycle with product of edge weights greater than or equal to 1) indicating a potential reason for the failure is returned. Further, a more precise approximation of the switched system can be constructed by considering a finer partition of the state-space in the construction of the finite weighted graph. We present experimental results on analyzing stability of switched systems using the above method.

MSC:

93D20 Asymptotic stability in control theory
93D05 Lyapunov and other classical stabilities (Lagrange, Poisson, \(L^p, l^p\), etc.) in control theory
93C30 Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Liberzon, D., Switching in Systems and Control (2003), Boston : Birkhäuser · Zbl 1036.93001
[2] T.A. Henzinger, The theory of hybrid automata, in: Proceedings of the IEEE Symposium on Logic in Computer Science, 1996, pp. 278-292. · Zbl 0959.68073
[3] Lin, H.; Antsaklis, P. J., Stability and stabilizability of switched linear systems: A survey of recent results, IEEE Trans. Automat. Control, 54, 2, 308-322 (2009) · Zbl 1367.93440
[4] Sontag, E. D., Input to state stability: Basic concepts and results, (Nonlinear and Optimal Control Theory (2006), Springer), 163-220 · Zbl 1175.93001
[5] Goebel, R.; Sanfelice, R.; Teel, A., Hybrid dynamical systems, IEEE Control Syst. Mag., 29, 28-93 (2009) · Zbl 1395.93001
[6] Geromel, J. C.; Colaneri, P., Stability and stabilization of continuous-time switched linear systems, SIAM J. Control Optim., 45, 5, 1915-1930 (2006) · Zbl 1130.34030
[7] Hespanha, J. P., Uniform stability of switched linear systems: extensions of LaSalle’s invariance principle, IEEE Trans. Automat. Control, 49, 4, 470-482 (2004) · Zbl 1365.93348
[8] Mason, P.; Boscain, U. V.; Chitour, Y., Common polynomial Lyapunov functions for linear switched systems, SIAM J. Control Optim., 45, 1, 226-245 (2006) · Zbl 1132.93038
[9] Parrilo, P. A., Structure Semidefinite Programs and Semialgebraic Geometry Methods in Robustness and Optimization (2000), California Institute of Technology: California Institute of Technology Pasadena, CA, May, (Ph.D. thesis)
[10] A. Papachristodoulou, S. Prajna, On the construction of Lyapunov functions using the sum of squares decomposition, in: Conference on Decision and Control, 2002. · Zbl 1138.93391
[11] Möhlmann, E.; Theel, O., Stabhyli: a tool for automatic stability verification of non-linear hybrid systems, (Proceedings of the International Conference on Hybrid Systems: Computation and Control (2013), ACM: ACM New York, NY, USA), 107-112 · Zbl 1362.93111
[12] Kapinski, J.; Deshmukh, J. V.; Sankaranarayanan, S.; Arechiga, N., Simulation-guided Lyapunov analysis for hybrid dynamical systems, (Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control (2014), ACM), 133-142 · Zbl 1362.93108
[13] H. Dierks, S. Kupferschmid, K. Larsen, Automatic abstraction refinement for timed automata, in: Proceedings of Formal Modeling and Analysis of Timed Systems, 2007, pp. 114-129. · Zbl 1141.68431
[14] P. Prabhakar, S. Duggirala, S. Mitra, M. Viswanathan, Hybrid automata-based CEGAR for rectangular hybrid automata, in: Proceedings of the International Conference on Verification, Model Checking, and Abstract Interpretation, 2013. · Zbl 1426.68175
[15] R. Alur, T. Dang, F. Ivancic, Counter-example guided predicate abstraction of hybrid systems, in: Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2003, pp. 208-223. · Zbl 1031.68074
[16] Clarke, E.; Fehnker, A.; Han, Z.; Krogh, B.; Ouaknine, J.; Stursberg, O.; Theobald, M., Abstraction and counterexample-guided refinement in model checking of hybrid systems, Int. J. Found. Comput. Sci., 14, 4, 583-604 (2003) · Zbl 1101.68678
[17] Prabhakar, P.; Soto, M. G., AVERIST: An algorithmic verifier for stability, Electron. Notes Theor. Comput. Sci., 317, 133-139 (2015)
[18] P. Prabhakar, M.G. Soto, Counterexample guided abstraction refinement for stability analysis, in: Proceedings of the International Conference on Computer Aided Verification, 2016. · Zbl 1411.68071
[19] Puri, A.; Varaiya, P., Verification of hybrid systems using abstractions, (Hybrid Systems II (1994)), 359-369
[20] Asarin, E.; Dang, T.; Girard, A., Hybridization methods for the analysis of nonlinear systems, Acta Inform., 43, 7, 451-476 (2007) · Zbl 1134.93026
[21] P. Prabhakar, M.G. Soto, An algorithmic approach to stability verification of polyhedral switched systems, in: American Control Conference, 2014.
[22] de Moura, L.; Bjørner, N., Z3: An efficient SMT solver, (Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, vol. 4963 (2008), Springer), 337-340
[23] Ho, P.-H., Automatic Analysis of Hybrid Systems (1995), Cornell University, (Ph.D. thesis)
[24] P. Prabhakar, M. Viswanathan, On the decidability of stability of hybrid systems, in: Proceedings of the International Conference on Hybrid Systems: Computation and Control, 2013, pp. 53-62. · Zbl 1362.68180
[25] P. Prabhakar, M.G. Soto, Abstraction based model-checking of stability of hybrid systems, in: Proceedings of the International Conference on Computer Aided Verification, 2013, pp. 280-295.
[26] Bellman, R., On a routing problem, Quart. Appl. Math., 16, 87-90 (1958) · Zbl 0081.14403
[27] Nuutila, E.; Soisalon-Soininen, E., On finding the strongly connected components in a directed graph, Inf. Process. Lett., 49, 1, 9-14 (1994) · Zbl 0787.68082
[28] Bagnara, R.; Hill, P. M.; Zaffanella, E., The parma polyhedra library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems, Sci. Comput. Program., 72, 1-2, 3-21 (2008)
[29] A.A. Hagberg, D.A. Schult, P.J. Swart, Exploring network structure, dynamics, and function using NetworkX, in: Proceedings of the Python in Science Conference, 2008, pp. 11-15.
[30] A. Makhorin, GLPK (GNU Linear Programming Kit), Available at http://www.gnu.org/software/glpk/glpk.html.
[31] Möhlmann, E.; Theel, O., Stabhyli: A tool for automatic stability verification of non-linear hybrid systems, (Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control (2013), ACM), 107-112 · Zbl 1362.93111
[32] G. Frehse, C. Le Guernic, A. Donzé, S. Cotton, R. Ray, O. Lebeltel, R. Ripado, A. Girard, T. Dang, O. Maler, SpaceEx: Scalable verification of hybrid systems, in: Proceedings of the International Conference on Computer Aided Verification, 2011.
[33] E. Clarke, O. Grumberg, S. Jha, Y. Lu, H. Veith, Counterexample-guided abstraction refinement, in: Proceedings of the International Conference on Computer Aided Verification, 2000, pp. 154-169. · Zbl 0974.68517
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.