Strukturierte Synthese symbolischer Abstraktionen für unendliche Kopplungen dynamischer Systeme

• Antragsteller: Professor Dr. Majid Zamani, seit 12/2021
• Fachliche Zuordnung: Automatisierungstechnik, Mechatronik, Regelungssysteme, Intelligente Technische Systeme, Robotik
• Förderung: Förderung von 2018 bis 2023
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 407680529

ZusammenfassungDie heutige Verfügbarkeit großer Rechenleistung, günstiger verteilter Sensorsysteme und der Verwaltung großer Datenmengen ermöglicht neuartige Anwendungen, bei denen eine Vielzahl verteilter Agenten im Hinblick auf ein gemeinsames Ziel geregelt werden müssen. Im Bereich der "Smart Cities" etwa kann ein wichtiger Schritt hin zu energieeffizienten und umweltbewussten Verkehrskonzepten verwirklicht werden durch z.B. stadtweite Verkehrsregelung basierend auf preiswerter persönlicher Kommunikation, Kommunikation zwischen den Fahrzeugen sowie einer Vielzahl von lokalen Sensoren. Die Vision, derartig große Systeme verteilter Agenten zu regeln, erfordert skalierbare Methoden, die Aufgaben wie unsichere und zeitvariante Anzahl von Subsystemen, Begrenzungen in der Kommunikation und strenge Sicherheitsanforderungen bewältigen können.Sowohl die Kosten für fehlerhafte Konfiguration als auch Sicherheitsvorgaben erfordern automatisierte und beweisbar korrekte Verfahren für die Synthese und Verifikation komplexer Systeme. Weiterhin erfordern neuartige Anwendungen komplexe Regelziele, die über die klassischen Ziele der Regelungstheorie hinausgehen. Ein komplexes Regelungsziel ist z.B. die Regelung von Ampeln, um Staus zu reduzieren und eine gewünschte untere Grenze für den Verkehrsfluss einzuhalten. Die Komplexität sowohl der Anforderungen als auch der Systembeschreibung und die Anzahl der teilnehmenden Agenten erfordern automatisierte Entwurfsverfahren für beweisbar korrekte Regler, wobei Ansätze der Regelungstheorie und der Informatik zusammengeführt werden. Zur Behandlung der dargestellten Aufgaben eigen sich insbesondere Verfahren zur automatisierten Verifikation und Synthese unter Verwendung der "correct-by-construction"-Methodik, die ursprünglich zur Spezifikation und Verifikation von Soft- und Hardwareverhalten entwickelt wurde.Die Untersuchung des automatisierten Reglerentwurfs auf Grundlage symbolischer Modelle hat in den letzten Jahren wesentliche Fortschritte erzielt. Es fehlt jedoch ein direkter, effizienter Zugang zur Behandlung hochdimensionaler Systeme, da die Komplexität der Konstruktion symbolischer Modelle vielfach exponentiell mit der Dimension des Systems wächst. Stattdessen schlagen wir vor, die Systemstruktur zu verwenden, um Methoden auf Basis von Small-Gain- oder Dissipativitätsargumenten zu entwickeln.Das Projekt zielt auf einen rigorosen mathematischen Rahmen für verteilte symbolische Regelungssysteme, die aus der Kopplung von abzählbar unendlich vielen Subsystemen entstehen. Die vorgeschlagenen Methoden erhalten die Kopplungsstruktur, wodurch verteilte Entwurfsverfahren unterstützt werden. Zur Darstellung der Wirksamkeit der entwickelten Verfahren werden sie auf Verkehrsnetze angewendet.

• DFG-Verfahren: Sachbeihilfen
• Ehemalige Antragsteller: Dr. Navid Noroozi, von 12/2018 bis 11/2021; Professor Dr. Fabian Wirth, bis 12/2018