Abstraction of dynamical systems by timed automata

Rafael Wisniewski*, Christoffer Sloth

*Kontaktforfatter for dette arbejde

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningpeer review

Resumé

To enable formal verification of a dynamical system, given by a set of difierential 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
Vol/bind32
Udgave nummer2
Sider (fra-til)79-90
ISSN0332-7353
DOI
StatusUdgivet - 2011
Udgivet eksterntJa

Fingeraftryk

Timed Automata
Equivalence classes
Dynamical systems
State Space
Dynamical system
Equivalence class
Partition
Formal Verification
Model checking
Lyapunov functions
Discrete Model
Reachability
Level Set
Lyapunov Function
Model Checking
Timing
Partitioning
Entire
Requirements
Abstraction

Citer dette

@article{d435c5b22c4243a28a3b19cf69c24197,
title = "Abstraction of dynamical systems by timed automata",
abstract = "To enable formal verification of a dynamical system, given by a set of difierential 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.",
keywords = "Abstraction, Stability, Timed automata, Verication",
author = "Rafael Wisniewski and Christoffer Sloth",
year = "2011",
doi = "10.4173/mic.2011.2.3",
language = "English",
volume = "32",
pages = "79--90",
journal = "Modeling, Identification and Control (Online)",
issn = "0332-7353",
publisher = "Norwegian Society of Automatic Control",
number = "2",

}

Abstraction of dynamical systems by timed automata. / Wisniewski, Rafael; Sloth, Christoffer.

I: Modeling, Identification and Control, Bind 32, Nr. 2, 2011, s. 79-90.

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningpeer review

TY - JOUR

T1 - Abstraction of dynamical systems by timed automata

AU - Wisniewski, Rafael

AU - Sloth, Christoffer

PY - 2011

Y1 - 2011

N2 - To enable formal verification of a dynamical system, given by a set of difierential 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.

AB - To enable formal verification of a dynamical system, given by a set of difierential 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.

KW - Abstraction

KW - Stability

KW - Timed automata

KW - Verication

U2 - 10.4173/mic.2011.2.3

DO - 10.4173/mic.2011.2.3

M3 - Journal article

VL - 32

SP - 79

EP - 90

JO - Modeling, Identification and Control (Online)

JF - Modeling, Identification and Control (Online)

SN - 0332-7353

IS - 2

ER -