Abstraction of Dynamical Systems by Timed Automata

Rafael Wisniewski, Christoffer Sloth

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningpeer review

6 Citationer (Scopus)
367 Downloads (Pure)

Abstract

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.
OriginalsprogEngelsk
TidsskriftModeling, Identification and Control (Online Edition)
Vol/bind32
Udgave nummer2
Sider (fra-til)79-90
Antal sider12
ISSN0332-7353
DOI
StatusUdgivet - 2011

Fingeraftryk

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

Citationsformater