Abstraction of Dynamical Systems by Timed Automata

Rafael Wisniewski, Christoffer Sloth

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningpeer review

6 Citationer (Scopus)
287 Downloads (Pure)


To enable formal verification of a dynamical system, given by a set of differential equations, it is abstracted by a finite state model. This allows for application of methods for model checking. Consequently, it opens the possibility of carrying out the verification 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.
TidsskriftModeling, Identification and Control (Online Edition)
Udgave nummer2
Sider (fra-til)79-90
Antal sider12
StatusUdgivet - 2011


Dyk ned i forskningsemnerne om 'Abstraction of Dynamical Systems by Timed Automata'. Sammen danner de et unikt fingeraftryk.