Abstract
In this paper, we present a novel abstraction technique and a model-checking algorithm for verifying Lyapunov and asymptotic stability of a class of hybrid systems called piecewise constant derivatives. We propose a new abstract data structure, namely, finite weighted graphs, and a modification of the predicate abstraction based on the faces in the system description. The weights on the edges trace the distance of the executions from the origin, and are computed by using linear programming. Model-checking consists of analyzing the finite weighted graph for the absence of certain kinds of cycles which can be solved by dynamic programming. We show that the abstraction is sound in that a positive result on the analysis of the graph implies that the original system is stable. Finally, we present our experiments with a prototype implementation of the abstraction and verification procedures which demonstrate the feasibility of the approach.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Alur, R., Dang, T., Ivančić, F.: Counter-Example Guided Predicate Abstraction of Hybrid Systems. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 208–223. Springer, Heidelberg (2003)
Asarin, E., Dang, T., Girard, A.: Hybridization methods for the analysis of nonlinear systems. Acta Informatica 43(7), 451–476 (2007)
Asarin, E., Maler, O., Pnueli, A.: Reachability analysis of dynamical systems having piecewise-constant derivatives. Theoretical Computer Science 138(1), 35–65 (1995)
Branicky, M.S.: Stability of hybrid systems. In: Unbehauen, H. (ed.) Encylopedia of Life Support Systems. Control Sytems, Robotics and Automation, volume Theme 6.43, chapter Article 6.43.28.3. UNESCO Publishing (2004)
Chen, X., Abraham, E., Sankaranarayanan, S.: Taylor model flowpipe construction for non-linear hybrid systems. In: Proceedings of the IEEE Real-Time Systems Symposium (2012)
Clarke, E.M., Fehnker, A., Han, Z., Krogh, B., Ouaknine, J., Stursberg, O., Theobald, M.: Abstraction and Counterexample-Guided Refinement in Model Checking of Hybrid Systems. International Journal on Foundations of Computer Science 14(4), 583–604 (2003)
Davrazos, G., Koussoulas, N.T.: A review of stability results for switched and hybrid systems. In: Proceedings of the Mediterranean Conference on Control (2001)
Dierks, H., Kupferschmid, S., Larsen, K.G.: Automatic Abstraction Refinement for Timed Automata. In: Proceedings of Formal Modeling and Analysis of Timed Systems, pp. 114–129 (2007)
Duggirala, P.S., Mitra, S.: Lyapunov abstractions for inevitability of hybrid systems. In: Proceedings of the International Conference on Hybrid Systems: Computation and Control, pp. 115–124 (2012)
Frehse, G.: PHAVer: Algorithmic verification of hybrid systems past hytech. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 258–273. Springer, Heidelberg (2005)
Girard, A.: Reachability of uncertain linear systems using zonotopes. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 291–305. Springer, Heidelberg (2005)
Goebel, R., Sanfelice, R., Teel, A.: Hybrid dynamical systems. IEEE Control Systems, Control Systems Magazine 29, 28–93 (2009)
Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What’s decidable about hybrid automata? In: Proceedings of the ACM Symposium on Theory of Computation, pp. 373–382 (1995)
Henzinger, T.A.: The Theory of Hybrid Automata. In: Proceedings of the IEEE Symposium on Logic in Computer Science, pp. 278–292 (1996)
Khalil, H.K.: Nonlinear Systems. Prentice-Hall, Upper Saddle River (1996)
Liberzon, D.: Switching in Systems and Control. Birkhuser, Boston (2003)
Oehlerking, J., Burchardt, H., Theel, O.: Fully automated stability verification for piecewise affine systems. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol. 4416, pp. 741–745. Springer, Heidelberg (2007)
Parrilo, P.A.: Structure Semidefinite Programs and Semialgebraic Geometry Methods in Robustness and Optimization. PhD thesis, California Institute of Technology, Pasadena, CA (May 2000)
Platzer, A., Quesel, J.-D.: KeYmaera: A hybrid theorem prover for hybrid systems (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 171–178. Springer, Heidelberg (2008)
Podelski, A., Wagner, S.: Model checking of hybrid systems: From reachability towards stability. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC 2006. LNCS, vol. 3927, pp. 507–521. Springer, Heidelberg (2006)
Prabhakar, P., Vladimerou, V., Viswanathan, M., Dullerud, G.E.: Verifying tolerant systems using polynomial approximations. In: Proceedings of the IEEE Real-Time Systems Symposium, pp. 181–190 (2009)
Prabhakar, P., Duggirala, P.S., Mitra, S., Viswanathan, M.: Hybrid automata-based CEGAR for rectangular hybrid systems. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 48–67. Springer, Heidelberg (2013)
Prabhakar, P., Dullerud, G.E., Viswanathan, M.: Pre-orders for reasoning about stability. In: Proceedings of the International Conference on Hybrid Systems: Computation and Control, pp. 197–206 (2012)
Prabhakar, P., Viswanathan, M.: A dynamic algorithm for approximate flow computations. In: Proceedings of the International Conference on Hybrid Systems: Computation and Control, pp. 133–143 (2010)
Prabhakar, P., Viswanathan, M.: On the decidability of stability of hybrid systems. In: Proceedings of the International Conference on Hybrid Systems: Computation and Control (2013)
Prajna, S., Jadbabaie, A.: Safety verification of hybrid systems using barrier certificates. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 477–492. Springer, Heidelberg (2004)
Puri, A., Borkar, V.S., Varaiya, P.: ε-approximation of differential inclusions. In: Proceedings of the International Conference on Hybrid Systems: Computation and Control, pp. 362–376 (1995)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Prabhakar, P., Garcia Soto, M. (2013). Abstraction Based Model-Checking of Stability of Hybrid Systems. In: Sharygina, N., Veith, H. (eds) Computer Aided Verification. CAV 2013. Lecture Notes in Computer Science, vol 8044. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39799-8_20
Download citation
DOI: https://doi.org/10.1007/978-3-642-39799-8_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-39798-1
Online ISBN: 978-3-642-39799-8
eBook Packages: Computer ScienceComputer Science (R0)