Automatisierte Erkennung und Eliminierung impliziter Äquivalenzen in quantifizierten nicht-linearen Ungleichungssystemen zur Stabilitätsverifikation hybrider Systeme mittels Lyapunov-Theorie
Automatisierte Erkennung und Eliminierung impliziter Äquivalenzen in quantifizierten nicht-linearen Ungleichungssystemen zur Stabilitätsverifikation hybrider Systeme mittels Lyapunov-Theorie
Automatisierte Erkennung und Eliminierung impliziter Äquivalenzen in quantifizierten nicht-linearen Ungleichungssystemen zur Stabilitätsverifikation hybrider Systeme mittels Lyapunov-Theorie
Bachelorarbeit
abgeschlossen 2015 von Philipp Zschoche
Themengebiete
- Hybride Systems
- Lyapunov Stabilität
- Automatische Verifikation
- Numerische Optimierung
- Graphentheorie
Hintergrund
Hybride Systeme sind dynamische Systeme, die sowohl diskretes als auch kontinuierliches Verhalten ausweisen.
Die Stabilitätsverifikation von linearen und nicht linearen hybriden Systemen ist im Allgemeinen ein unentscheidbares Problem. Es ist möglich durch Lyapunov-Funktionen die Stabilität eines hybriden Systems zu verifizieren.
Stabhyli ist ein Programm zur automatischen Stabilitätsverifizierung von nicht linearen hybriden Systemen mittels Lyapunov-Funktionen. Bei der Suche nach geeigneten Lyapunov-Funktionen entstehen ein nicht lineares Ungleichungssystem aus Bedingungen in der jede Bedingung der folgenden Form entspricht:
f(0) = 0 ∧ ∀ x ∈ R : 0 ≤ f(x) wobei f in Polynom und R eine Region des Hybriden Systems
Numerische Probleme können zu nicht korrekten Lösungen dieser Bedingungen führen. Es werden kleine Abstände, "gaps", eingefügt, um die Robustheit gegenüber numerischen Problemen zu vergrößern.
Enthält ein Ungleichungssystem implizite Äquivalenzen, kann diese Robustheitserweiterung dazu führen, dass es keine Lösung mehr gibt. Die Stabilitätsverifizierung ist nicht mehr möglich.
Daher ist es besonders wichtig implizite Äquivalenzen zu finden und zu eliminieren.
Aufgabenbeschreibung
In dieser Bachelorarbeit soll die Erkennung und Eliminierung von impliziten Äquivalenzen in Bezug auf die Stabilitätsverifikation von hybriden Systemen mittels Lyapunov-Funktionen untersucht werden.
Insbesondere wird Stabhyli um eine bereits beschriebene Heuristik erweitert, um implizite Äquivalenzen zu erkennen.
Für die Eliminierung soll ein Backtracking-Algorithmus entwickelt und implementiert werden, der bekannte implizite Äquivalenzen aus dem gegebenen Gleichungssystem entfernt und für Problemlöser, wie CSDP und SDPA, optimiert.
Des Weiteren soll evaluiert werden, ob sich das entwickelte Verfahren noch weiter verfeinern lässt, wie z.B.:
- Mit einer Bewertungsfunktion für den Backtracking-Algorithmus
- Erneut nach impliziten Äquivalenzen suchen, nachdem eine implizite Äquivalenz beseitigt wurde.