Abstract
We look at the problem of proving inevitability of continuous dynamical systems. An inevitability property says that a region of the state space will eventually be reached: this is a type of liveness property from the computer science viewpoint, and is related to attractivity of sets in dynamical systems. We consider a method of Maler and Batt to make an abstraction of a continuous dynamical system to a timed automaton, and show that a potentially infinite number of splits will be made if the splitting of the state space is made arbitrarily. To solve this problem, we define a method which creates a finite-sized timed automaton abstraction for a class of linear dynamical systems, and show that this timed abstraction proves inevitability.
This paper has been made under the framework of the EPSRC-funded project “DYVERSE: A New Kind of Control for Hybrid Systems” (EP/I001689/1). The second author is also grateful for the support of the RCUK (EP/E50048/1).
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Batt, G., Belta, C., Weiss, R.: Model Checking Liveness Properties of Genetic Regulatory Networks. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 323–338. Springer, Heidelberg (2007)
Behrmann, G., David, A., Larsen, K.G.: A Tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004)
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 of Foundations of Computer Science 14(4), 583–604 (2003)
D’Innocenzo, A., Julius, A.A., Di Benedetto, M.D., Pappas, G.J.: Approximate timed abstractions of hybrid automata. In: 46th IEEE Conference on Decision and Control, pp. 4045–4050 (2007)
Duggirala, P.S., Mitra, S.: Lyapunov Abstractions for Inevitability of Hybrid Systems. In: Hybrid Systems: Computation and Control (HSCC), pp. 115–123 (2012)
Heinrich, R., Neel, B.G., Rapoport, T.A.: Mathematical Models of Protein Kinase Signal Transduction. Molecular Cell 9(5), 957–970 (2002)
Johansson, K.H., Egerstedt, M., Lygeros, J., Sastry, S.: On the regularization of Zeno hybrid automata. Systems & Control Letters 38(3), 141–150 (1999)
Lyapunov, A.M.: The general problem of the stability of motion. PhD thesis, Moscow University (1892); Reprinted in English in the International Journal of Control 55(3) (1992)
Maler, O., Batt, G.: Approximating Continuous Systems by Timed Automata. In: Fisher, J. (ed.) FMSB 2008. LNCS (LNBI), vol. 5054, pp. 77–89. Springer, Heidelberg (2008)
Mitchell, I., Tomlin, C.J.: Level Set Methods for Computation in Hybrid Systems. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 310–323. Springer, Heidelberg (2000)
Olivero, A., Sifakis, J., Yovine, S.: Using Abstractions for the Verification of Linear Hybrid Systems. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 81–94. Springer, Heidelberg (1994)
Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th International Symposium on the Foundations of Computer Science, pp. 46–57 (1977)
Ratschan, S., She, Z.: Safety verification of hybrid systems by constraint propagation-based abstraction refinement. ACM Transactions on Embedded Computing Systems 6(1), 573–589 (2007)
Sloth, C., Wisniewski, R.: Verification of continuous dynamical systems by timed automata. Formal Methods in System Design 39(1), 47–82 (2011)
Stursberg, O., Kowalewski, S., Engell, S.: On the Generation of Timed Discrete Approximations for Continuous Systems. Mathematical and Computer Modelling of Dynamical Systems: Methods, Tools and Applications in Engineering and Related Sciences 6(1), 51–70 (2000)
Tiwari, A.: Abstractions for hybrid systems. Formal Methods in System Design 32(1), 57–83 (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Carter, R., Navarro-López, E.M. (2012). Dynamically-Driven Timed Automaton Abstractions for Proving Liveness of Continuous Systems. In: Jurdziński, M., Ničković, D. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2012. Lecture Notes in Computer Science, vol 7595. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33365-1_6
Download citation
DOI: https://doi.org/10.1007/978-3-642-33365-1_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-33364-4
Online ISBN: 978-3-642-33365-1
eBook Packages: Computer ScienceComputer Science (R0)