Skalierbare Reglersynthese mit formalen Garantien

• Antragsteller: Professor Dr.-Ing. Matthias Althoff
• Fachliche Zuordnung: Automatisierungstechnik, Mechatronik, Regelungssysteme, Intelligente Technische Systeme, Robotik
• Förderung: Förderung seit 2022
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 511538378

Cyber-physische Systeme sind komplexe Systeme, die physikalische Fähigkeiten mit rechnerischen Fähigkeiten kombinieren. Dazu gehören hochsichere medizinische Geräte und Systeme, Prozesssteuerungen, autonome Fahrzeuge, Flugobjekte, Energiesysteme, Roboter, Fertigungssysteme und intelligente Strukturen. Die immer komplexeren Anforderungen an cyber-physische Systeme machen es sehr schwierig, sie zu regeln oder sogar zu beweisen, dass ihre Spezifikation erfüllt wird. Aus diesem Grund ist die automatische Reglersynthese mit formalen Garantien ein aktives Forschungsgebiet. Es gibt jedoch keine skalierbaren und formal korrekten Synthesemethoden für beliebige nichtlineare Systeme, deren algorithmische Parameter automatisch eingestellt werden. Um dieses Problem anzugehen, schlagen wir einen Syntheseansatz vor, der keine Diskretisierung des Zustandsraumes benötigt und stattdessen Optimierungstechniken in Kombination mit Erreichbarkeitsanalysen verwendet. Zunächst sollen Spezifikationen mittels temporaler Logik in hybride Automaten übersetzen werden, um anschließend den Produktautomaten mit dem zu steuernden System zu berechnen. Auf diese Weise kann jede Reglersynthese als Lösung eines Erreichbarkeitsproblems für hybride Systeme umformuliert werden. Mittels Optimierung erhalten wir eine optimale nominale Lösung. Diese dient als Grundlage für die Reglersynthese, um sicherzustellen, dass auch alle anderen Lösungen aufgrund von unsicheren Anfangszuständen, Störungen und Sensorrauschen die Spezifikationen einhalten. Wir erhalten die Menge aller Lösungen für jede Optimierungsiteration mithilfe der Erreichbarkeitsanalyse. Eine abschließende Analyse wird in einer überapproximativen Weise durchgeführt, um formale Garantien zu gewährleisten. Die Kombination von Optimierungstechniken und Erreichbarkeitsanalyse hat den entscheidenden Vorteil, dass nur Lösungen um eine optimale Referenzlösung herum untersucht werden müssen -- dieses Vorgehen gewährleistet skalierbare Lösungen. Um diesen Prozess vollständig zu automatisieren, werden wir notwendige Parameter für unsere Algorithmen automatisch bestimmen. Neben anderen Anwendungsfällen werden wir unseren Ansatz an unserem autonomen Fahrzeug EDGAR evaluieren. Das Fahrzeug wird gemeinsam mit anderen Lehrstühlen der TUM genutzt und wurde mithilfe einer DFG-Großgeräteförderung finanziert. Alle entwickelten Algorithmen werden über unsere Software-Tools CORA (cora.in.tum.de) für Erreichbarkeitsanalyse und AROC (aroc.cps.in.tum.de) für formale Reglersynthese verfügbar sein.

• DFG-Verfahren: Sachbeihilfen