arXiv · 1008.3222
Proofs for an Abstraction of Continuous Dynamical Systems Utilizing Lyapunov Functions
Abstract
In this report proofs are presented for a method for abstracting continuous dynamical systems by timed automata. The method is based on partitioning the state space of dynamical systems with invariant sets, which form cells representing locations of the timed automata. To enable verification of the dynamical system based on the abstraction, conditions for obtaining sound, complete, and refinable abstractions are set up. It is proposed to partition the state space utilizing sub-level sets of Lyapunov functions, since they are positive invariant sets. The existence of sound abstractions for Morse-Smale systems and complete and refinable abstractions for linear systems are proved.
Explore related subjects
Keep this discovery
Christoffer Sloth, Rafael Wisniewski. 2010-08-19. Proofs for an Abstraction of Continuous Dynamical Systems Utilizing Lyapunov Functions. https://arxiv.org/abs/1008.3222
Cite the original work for its findings. Save a collection to share your selection of sources.