Anschlussprojekte
Prof. Dr. Majid Zamani
Technische Universität München
Professur für Hybride Regelungssysteme
Prof. Dr. Murat Arcak
University of California, Berkeley
EECS - Electrical Engineering and Computer Science
Zertifizierbare Synthese von autonomen Systemen
Dieses Projekt zielt darauf ab, eine skalierbare Entwurfsmethodik zu entwickeln, bei der die
eingebetteten Regler für stochastische cyber-physikalische Systeme mit High-Level-
Spezifikationen auf formale Art und quasi auf Knopfdruck synthetisiert werden.
Sicherheitskritische und operationskritische Systeme wie etwa autonomer Transport und
Energienetzwerke sind Beispiele für cyber-physikalische Systeme. In cyber-physikalischen
Systemen arbeiten räumlich verteilte physikalische Systeme in unsicheren oder
störungsintensiven Umgebungen und interagieren über eingebettete Regler mit verteilten
Rechenkomponenten.
Um die Entwurfskosten von eingebetteter Regelungssoftware zu senken und deren Korrektheit zu
garantieren, stellen wir eine Teile-und-Herrsche-Strategie vor, um eine automatisierte Synthese
für cyber-physikalische Systeme durch die Kombination von kompositionellen Methoden aus der
Informatik (z.B. Assume-Guarantee-Regeln) mit solchen aus der Kontrolltheorie (z.B. Small-
Gain und Dissipativitätsresultate) zu skalieren.
Ausgangsprojekt: Automatisierte Synthese Cyber-Physikalischer Systeme: Eine passivitätsbasierte Methode
Abschlussbericht
Unter der gemeinsamen Leitung von Prof. Majid Zamani, Prof. Murat Arcak, Herrn Bingzhuo Zhong (Doktorand an der TU München) und Dr. Paul Griffioen (Postdoc an der UC Berkeley) zielte dieses Projekt darauf ab, hierarchische Kontrollmethoden zu erneuern und Techniken zur Berechnung von probabilistischen kontrollierten invarianten Mengen für nichtlineare Systeme zu entwickeln. Der Höhepunkt dieses Projekts führte zu zwei bedeutenden Ergebnissen, die sich mit kritischen Herausforderungen in der Kontrolltheorie und -anwendung befassen.
Ergebnis 1: Verbesserte hierarchische Kontrollarchitekturen
Dieses Ergebnis konzentrierte sich auf die Verfeinerung hierarchischer Kontrollmethoden, um Fehler zwischen abstrakten und konkreten Systemen abzumildern. Herkömmliche Methoden stoßen oft auf erhebliche Diskrepanzen, was die Wirksamkeit hierarchischer Kontrollarchitekturen einschränkt. Um diese Einschränkung zu überwinden, wurde eine neuartige Simulationsbeziehung eingeführt, die als "allgemeine ungefähre alternative Simulationsbeziehung" bezeichnet wird. Diese Relation bezieht Eingabesätze von abstrakten Systemen ein, um Systemähnlichkeiten effektiv zu erfassen und Fehlerquoten zu reduzieren. Es wurden Methoden zur Erstellung dieser Beziehung für zeitdiskrete Kontrollsysteme mit endlichen Zustands- und Eingabemengen sowie für lineare Kontrollsysteme und ihre kontinuierlichen Abstraktionen vorgestellt. Die Praktikabilität und Effektivität dieses Ansatzes wurde anhand von anschaulichen Beispielen demonstriert, die sein Potenzial für reale Anwendungen aufzeigten.
Ergebnis 2: Berechnung probabilistischer kontrollierter invarianter Mengen
Das zweite Ergebnis konzentrierte sich auf die Berechnung von probabilistischen kontrollierten invarianten Mengen für unbekannte nichtlineare Systeme unter Verwendung datengesteuerter Techniken. Insbesondere wurden Gauß-Prozess-Zustandsraummodelle verwendet, um nichtlineare Systeme zu modellieren, wobei nicht modellierte und unbekannte Dynamiken berücksichtigt wurden. Es wurde ein auf semidefiniter Programmierung basierendes Optimierungsschema vorgeschlagen, um probabilistische kontrollierte invariante Mengen zu berechnen, begleitet von Zustandsrückkopplungsreglern zur Maximierung der Systemstabilität unter Berücksichtigung von Eingabebeschränkungen. Darüber hinaus wurde die Beziehung zwischen probabilistischer Invarianz und Sicherheit für endliche Zeithorizonte untersucht, was zum Entwurf von Sicherheitsreglern führte, um die Systemsicherheit innerhalb endlicher Zeithorizonte zu gewährleisten. Die Wirksamkeit dieser Techniken wurde durch Simulationen und physikalische Experimente auf einer Quadrotor-Plattform validiert.