Abstraction of Dynamical Systems by Timed
Rafael Wisniewski · 2011
To enable formal verication of a dynamical system, given by a set of dierential equations, it is abstracted by a nite state model. This allows for application of methods for model checking. Consequently, it opens the possibility of carrying out the verication of reachability and timing requirements, which by classical control methods is impossible. We put forward a method for abstracting dynamical systems, where level sets of Lyapunov functions are used to generate the partitioning of the state space. We propose to partition the state space using an entire family of functions. The properties of these functions ensure that the discrete model captures the behaviors of a dynamical system by generating appropriate equivalence classes of the states. These equivalence classes make up the partition of the state space.