h1

h2

h3

h4

h5
h6
http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.png

Reachability analysis of non-linear hybrid systems using Taylor Models = Erreichbarkeitsanalyse für nicht-lineare hybride Systeme unter Verwendung von Taylor-Modellen



Verantwortlichkeitsangabevorgelegt von Xin Chen

ImpressumAachen : Publikationsserver der RWTH Aachen University 2015

Umfang166 S. : graph. Darst.

ReiheAachener Informatik Berichte ; 2015, 09


Dissertation, RWTH Aachen University, 2015


Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
;

Tag der mündlichen Prüfung/Habilitation
2015-03-24

Online
URN: urn:nbn:de:hbz:82-rwth-2015-016535
URL: https://publications.rwth-aachen.de/record/465295/files/465295.pdf
URL: https://publications.rwth-aachen.de/record/465295/files/465295.pdf?subformat=pdfa

Einrichtungen

  1. Lehr- und Forschungsgebiet Theorie Hybrider Systeme (123420)
  2. Fachgruppe Informatik (120000)

Inhaltliche Beschreibung (Schlagwörter)
ODE (frei) ; Taylor model (frei) ; continuous system (frei) ; hybrid system (frei)

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
Mit der allgegenwärtigen Verwendung von Computern in der Regelung von physikalischen Systemen entstand der Bedarf für neue Formalismen, die in der Lage sind, sowohl kontinuierliches als auch diskretes Verhalten zu behandeln. Hybride Systeme wurden für diesen Zweck eingeführt. Ein hybrides System, welches in dieser Arbeit durch hybride Automaten modelliert wird, ist ausgestattet mit endlich vielen diskreten Modi und kontinuierlichen reell-wertigen Variablen. Der Systemzustand ist repräsentiert durch den aktuellen Modus zusammen mit der Evaluierung der Variablen. In einem gegebenen Modus l, ändern sich die Variablenwerte entweder kontinuierlich entsprechend den Differentialgleichungen die l zugeordnet sind, oder aber diskret einer von l ausgehenden Transition folgend. Diese Arbeit konzentriert sich auf Techniken, die es ermöglichen, alle in einem vorgegebenen Zeithorizont mit einer eingeschränkten Anzahl von diskreten Transitionen erreichbaren Zustände eines hybriden Systems mit nicht-linearer Dynamik zu bestimmen.Obwohl die Erreichbarkeitsanalyse für hybride Systeme mit linearer Dynamik bereits intensiv erforscht wurde, stehen nur wenige Techniken für nicht-lineare Dynamiken, die in Anwendungen sehr häufig vorkommen, zur Verfügung. Solche Techniken zu entwickeln ist aus zwei Gründen schwierig. Erstens ist es nicht einfach eine hinreichend präzise Überapproximation für die Lösungen der nicht-linearen Differentialgleichungen zu finden. Zweitens müssen, um die Erreichbarkeit entlang diskreter Transitionen zu berechnen, schwere nicht-lineare reell-arithmetische Probleme gelöst werden. Wir stellen in dieser Arbeit Ansätze zur Lösung dieser Probleme vor. Um das erste Problem zu lösen, verwenden wir Taylor Modelle, um die Lösungen von nicht-linearen Differentialgleichungen überapproximierend zu repräsentieren. Unser Ansatz kann als eine Variante der Taylor Model Methode von Berz et al. betrachtet werden. Wir sind in der Lage, hinreichend genaue überapproximierende Repräsentierungen für die Lösungsmengen von Beispielen mit mehr als 10 Variablen effizient zu bestimmen. Zusätzlich erweitern wir die Arbeit von Lin und Stadtherr um Differentialgleichungen mit beschränkten zeit-varianten Parametern behandeln zu können. Um die zweite Schwierigkeit zu meistern, stellen wir zwei Techniken vor: (a) Domänen-Verengung (domain contraction) und (b) Wertebereich-Überapproximation(range over-approximation), um erreichbare Zustandsmengen, aus denen eine Transition genommen werden kann, überapproximierend zu beschreiben. Diese Methoden verwenden SAT Modulo Theories (SMT) Algorithmen, die auf die Erreichbarkeitsanalyse von hybriden Systemen angepasst wurden. Um den Berechnungsaufwand zu reduzieren schlagen wir unterschiedliche Methoden für die Zusammenfassung von mehreren Taylor Modellenvor. Zusätzlich stellen wir eine Methode zur schnellen Berechnung von Taylor-Modell-Überapproximationen für Lösungen von linearen Differentialgleichungen vor.Damit unsere Methoden anderen zugänglich wird, haben wir sie in dem Flow* Programm implementiert. Um die Wirksamkeit zu untersuchen, vergleichen wir Flow* ausführlich zu anderen häufig verwendeten Programmen anhand mehrerer, nicht-trivialer Anwendungen, die wir aus den Bereichen der Mechanik, Biologie, Elektrotechnik und Medizin entnahmen. Aus den experimentellen Ergebnissen werden mit immer größer werdendenBeispielen die Vorteile von Flow* im Vergleich zu anderen Programmen klar ersichtlich. Die Ergebnisse zeigen, dass das Programm auf Beispiele realistischer Größe angewandt werden kann.

With the ubiquitous use of computers in controlling physical systems, it requires to have a new formalism that could model both continuous flows and discrete jumps. Hybrid systems are introduced to this purpose. A hybrid system, which is modeled by a hybrid automaton in the thesis, is equipped with finitely many discrete modes and continuous real-valued variables. A state of it is then represented by a mode along with a valuation of the variables. Given that the system is in a mode l, the variable values are changed continuously according to the Ordinary Differential Equation (ODE) associated to l, or discretely by a jump starting from l. The thesis focuses on the techniques to compute all reachable states over a bounded time horizon and finitely many jumps for a hybrid system with non-linear dynamics. The results of that can then be used in safety verification of the system.Although a great amount of work has been devoted to the reachability analysis of hybrid systems with linear dynamics, there are few effective approaches proposed for the non-linear case which is very often in applications. The difficulty is twofold. Firstly, it is not easy to find an over-approximation with acceptable accuracy for a set of the solutions of a non-linear ODE. Secondly, to detect and compute the reachable states under a jump requires solving non-linear real arithmetic problems which is also difficult in general. In the thesis, we present our approaches to deal with the above difficulties. For the first one, we present the use of Taylor models as the over-approximate representations for non-linear ODE solutions. Our work can be viewed as a variant of the Taylor model method proposed by Berz et al., such that we are able to efficiently deal with some examples with more than $10$ variables. Besides, we also extend the work of Lin and Stadtherr to handle the ODEs with bounded time-varying parameters. For the second difficulty, we present two techniques: (a) domain contraction and (b) range over-approximation to compute an enclosure for the reachable set from which a jump is enabled. They can be seen as Satisfiability Modulo Theories (SMT) solving algorithms which are specialized for the reachability analysis of hybrid systems. In order to reduce the computational cost, we also propose different heuristics for aggregating Taylor models. Besides the above contributions, we describe a method to fast generate Taylor model over-approximations for linear ODE solutions. Its performance is demonstrated via a comparison with the tool SpaceEx. To make our methods accessible by other people, we implement them in a tool named Flow*. To examine the effectiveness, we thoroughly compare it with some related tools which are popularly used, according to their functionalities, over a set of non-trivial benchmarks that are collected by us from the areas of mechanics, biology, electronic engineering and medicine. From the experimental results, the advantage of Flow* over the other tools becomes more apparent when the scale of the system grows. On the other hand, it also shows that Flow* can be applied to analyzing realistic systems.

OpenAccess:
Download fulltext PDF Download fulltext PDF (PDFA)
(additional files)

Dokumenttyp
Dissertation / PhD Thesis/Book

Format
online, print

Sprache
English

Externe Identnummern
HBZ: HT018627997

Interne Identnummern
RWTH-2015-01653
Datensatz-ID: 465295

Beteiligte Länder
Germany

 GO


OpenAccess

QR Code for this record

The record appears in these collections:
Document types > Theses > Ph.D. Theses
Document types > Books > Books
Faculty of Mathematics, Computer Science and Natural Sciences (Fac.1) > Department of Computer Science
Publication server / Open Access
Public records
Publications database
120000
123420

 Record created 2015-04-08, last modified 2023-04-08