Dynamically-Driven Timed Automaton Abstractions for Proving Liveness of Continuous Systems
- 432 Downloads
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.
KeywordsContinuous-time systems Abstraction Automated verification Liveness properties Timed automata
Unable to display preview. Download preview PDF.
- 4.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)Google Scholar
- 5.Duggirala, P.S., Mitra, S.: Lyapunov Abstractions for Inevitability of Hybrid Systems. In: Hybrid Systems: Computation and Control (HSCC), pp. 115–123 (2012)Google Scholar
- 8.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)Google Scholar
- 12.Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th International Symposium on the Foundations of Computer Science, pp. 46–57 (1977)Google Scholar