Abstraction of Dynamical Systems by Timed Automata

Rafael Wisniewski, Christoffer Sloth

Research output: Contribution to journalJournal articleResearchpeer-review

6 Citations (Scopus)
288 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.
Original languageEnglish
JournalModeling, Identification and Control (Online Edition)
Issue number2
Pages (from-to)79-90
Number of pages12
Publication statusPublished - 2011


  • verification
  • stability
  • abstraction
  • timed automata

Fingerprint Dive into the research topics of 'Abstraction of Dynamical Systems by Timed Automata'. Together they form a unique fingerprint.

Cite this