Abstraction of Continuous Dynamical Systems Utilizing Lyapunov Functions

Christoffer Sloth, Rafal Wisniewski

Research output: Contribution to journalConference article in JournalResearchpeer-review

6 Citations (Scopus)

Abstract

This paper considers the development of a method for abstracting continuous dynamical systems by timed automata. The method is based on partitioning the state space of dynamical systems with invariant sets, which form cells representing locations of the timed automata.

To enable verification of the dynamical system based on the abstraction, conditions for obtaining sound, complete, and refinable abstractions are set up.

It is proposed to partition the state space utilizing sub-level sets of Lyapunov functions, since they are positive invariant sets. The existence of sound abstractions for Morse-Smale systems and complete and refinable abstractions for linear systems are shown.
Original languageEnglish
JournalI E E E Conference on Decision and Control. Proceedings
Pages (from-to)3760-3765
ISSN0743-1546
DOIs
Publication statusPublished - 2010
Event49th IEEE Conference on Decision and Control - Atlanta, United States
Duration: 15 Dec 201017 Dec 2010

Conference

Conference49th IEEE Conference on Decision and Control
CountryUnited States
CityAtlanta
Period15/12/201017/12/2010

Fingerprint

Lyapunov functions
Lyapunov Function
Dynamical systems
Dynamical system
Timed Automata
Invariant Set
Acoustic waves
State Space
Linear systems
Level Set
Partitioning
Linear Systems
Partition
Abstraction
Cell
Sound

Cite this

@inproceedings{98b0f7daa5ef41d9be6a00157a7d867d,
title = "Abstraction of Continuous Dynamical Systems Utilizing Lyapunov Functions",
abstract = "This paper considers the development of a method for abstracting continuous dynamical systems by timed automata. The method is based on partitioning the state space of dynamical systems with invariant sets, which form cells representing locations of the timed automata. To enable verification of the dynamical system based on the abstraction, conditions for obtaining sound, complete, and refinable abstractions are set up. It is proposed to partition the state space utilizing sub-level sets of Lyapunov functions, since they are positive invariant sets. The existence of sound abstractions for Morse-Smale systems and complete and refinable abstractions for linear systems are shown.",
author = "Christoffer Sloth and Rafal Wisniewski",
year = "2010",
doi = "10.1109/CDC.2010.5717270",
language = "English",
pages = "3760--3765",
journal = "I E E E Conference on Decision and Control. Proceedings",
issn = "0743-1546",
publisher = "IEEE Computer Society Press",

}

Abstraction of Continuous Dynamical Systems Utilizing Lyapunov Functions. / Sloth, Christoffer; Wisniewski, Rafal.

In: I E E E Conference on Decision and Control. Proceedings, 2010, p. 3760-3765.

Research output: Contribution to journalConference article in JournalResearchpeer-review

TY - GEN

T1 - Abstraction of Continuous Dynamical Systems Utilizing Lyapunov Functions

AU - Sloth, Christoffer

AU - Wisniewski, Rafal

PY - 2010

Y1 - 2010

N2 - This paper considers the development of a method for abstracting continuous dynamical systems by timed automata. The method is based on partitioning the state space of dynamical systems with invariant sets, which form cells representing locations of the timed automata. To enable verification of the dynamical system based on the abstraction, conditions for obtaining sound, complete, and refinable abstractions are set up. It is proposed to partition the state space utilizing sub-level sets of Lyapunov functions, since they are positive invariant sets. The existence of sound abstractions for Morse-Smale systems and complete and refinable abstractions for linear systems are shown.

AB - This paper considers the development of a method for abstracting continuous dynamical systems by timed automata. The method is based on partitioning the state space of dynamical systems with invariant sets, which form cells representing locations of the timed automata. To enable verification of the dynamical system based on the abstraction, conditions for obtaining sound, complete, and refinable abstractions are set up. It is proposed to partition the state space utilizing sub-level sets of Lyapunov functions, since they are positive invariant sets. The existence of sound abstractions for Morse-Smale systems and complete and refinable abstractions for linear systems are shown.

U2 - 10.1109/CDC.2010.5717270

DO - 10.1109/CDC.2010.5717270

M3 - Conference article in Journal

SP - 3760

EP - 3765

JO - I E E E Conference on Decision and Control. Proceedings

JF - I E E E Conference on Decision and Control. Proceedings

SN - 0743-1546

ER -