Beginn des Projekts 2004, Ende des Projekts 2016

Hybride Systeme sind Regelsysteme, die sowohl zeitkontinuierliches Verhalten als auch diskrete Zustandssprünge beinhalten können. Sie stellen daher eine Kombination von klassichen Reglern (zeitkontinuierlich) und rechnergestützten Reglern (zeitdiskret) dar und sind deshalb besonders praxisrelevant. Hybride Modelle werden beispielsweise eingesetzt zur Modellierung von eingebetteten Systemen, biologischen Systemen oder Industrieprozessen. Stabilität bezeichnet die Eigenschaft, dass zeitlich begrenzte Störungen des Systems das Verhalten nicht dauerhaft beeinflussen, sondern vom System eigenständig wieder ausgeglichen werden. Ein stabiles Regelsystem ist damit inhärent robust gegenüber unvorhergesehenen Störungen. Stabilität ist eine Liveness-Eigenschaft eines Systems und damit in der Regel schwierig nachzuweisen. Wir konzentrieren uns auf den Beweis der sogenannten asymptotischen Stabilität. Ein Regelsystem ist global asymptotisch stabil, wenn es sich für jeden möglichen Startzustand, unter Abwesenheit von Störungen, letzendlich in einen Ruhepunkt einpendelt. Dieser Ruhepunkt kann als wünschenswerter Zustand des Systems angesehen werden. Die Konsequenz ist Robustheit gegenüber temporären Störungen des Systems: das System wird bei Nachlassen der Störerffekte immer in die Nähe des Ruhepunkts zurückkehren. Der Beweis solch einer Eigenschaft kann mittels Lyapunov-Funktionen erbracht werden. Solch eine Funktion kann als Maß der Energie des Systems verstanden werden. Wenn sichergestellt wird, dass das Energieminimum im Ruhepunkt liegt und dass das Energieniveau im Laufe der Zeit fortwährend sinkt, so kann dies zum Beweis globaler asymptotischer Stabilität verwendet werden. Das zentrale Problem hierbei ist, dass solch eine Funktion gefunden werden muss -- dies ist eine nichttriviale Aufgabe. Das Problem der Suche nach solch einer Lyapunov-Funktion kann in ein effizient lösbares Optimierungsproblem verwandelt werden, dessen optimale Lösung die Parametrisierung solch einer Lyapunov-Funktion ist. Unser Ziel ist es, diese Berechnungsmethoden voranzutreiben, so dass sie in Verifikationswerkzeuge integriert werden können. Hierbei werden z.B. Dekompositionsmethoden verwendet, die ein großes, eventuell nicht numerisch robustes Optimierungsproblem in mehrere robustere zerlegen. Hierdurch ist es möglich, komplexere Systeme zu analysieren, als es sonst möglich wäre. Desweiteren befassen wir uns mit der Erweiterung dieser Methoden auf Systeme mit probabilistischem Verhalten und Zeitverzögerungen.

• Prof. Dr.-Ing. Oliver Theel
• Dipl.-Inform. Eike Möhlmann
• Dr.-Ing. Jens Oehlerking, Dipl.-Inform.

• Deutsche Forschungsgemeinschaft (DFG)
• AVACS-Webseite
• Universität des Saarlandes, Saarbrücken
• Albert-Ludwig-Universität Freiburg
• Max-Planck-Institut für Informatik, Saarbrücken
• Tschechische Akademie der Wissenschaften