Raumfahrzeugkontrolle

Spacecraft Proximity Operations umfassen Manöver, bei denen zwei oder mehr Raumfahrzeuge in unmittelbarer Nähe zueinander operieren, wie sie beispielsweise beim On-Orbit-Servicing, bei der aktiven Trümmerbeseitigung, beim automatisierten Andocken oder bei der In-Orbit-Montage auftreten. Für diese Szenarien entwickeln wir automatisierte Regelungsalgorithmen, mit besonderem Fokus auf sicheres Reinforcement Learning mittels Shielding. Darüber hinaus erfordert die rasant wachsende Anzahl eingesetzter Raumfahrzeuge in zukünftigen Systemen ein deutlich höheres Maß an Autonomie, da menschliche Operatoren nicht mehr in der Lage sein werden, alle Systeme direkt zu steuern. Um dieser Herausforderung zu begegnen, entwickeln wir Methoden, die die Sicherheit autonomer Entscheidungsprozesse gewährleisten, beispielsweise durch die Korrektur unsicherer Aktionen oder durch die Einschränkung des Systems auf eine vordefinierte Menge sicherer Handlungsalternativen.

Formale Verifikation mittels Erreichbarkeitsanalyse

Da sie echtzeitfähig ist, Robustheit gegenüber Störungen, Messfehlern und Modellunsicherheiten formal garantieren kann und zudem für sich dynamisch verändernde Umgebungen geeignet ist, gilt die Erreichbarkeitsanalyse als eine der vielversprechendsten Methoden zur formalen Verifikation dynamischer Systeme, wie beispielsweise Raumfahrzeuge, Roboter,  und autonome Fahrzeuge. Allerdings hängt die Qualität der berechneten erreichbaren Mengen häufig entscheidend von einer sorgfältigen Abstimmung von Hyperparametern ab, die in der Regel Expertenwissen erfordert. Neben der Entwicklung neuer Erreichbarkeitsalgorithmen für lineare (HSCC 2023), nichtlineare (CDC 2020), von neuralen Netzen gesteuerten (NASA 2023) und hybride Systeme (HSCC 2020) ist es daher eines unserer zentralen Forschungsziele, vollständig automatisierte Verifikationsverfahren zu entwerfen, die ohne Hyperparameterabstimmung auskommen und zuverlässig auch von Nicht-Experten angewendet werden können (TAC 2023, HSCC 2023, NAHS 2024).

Safe-by-Construction Reglersynthese

Ein gängiger Ansatz zur Regelung mit formalen Sicherheitsgarantien besteht darin, zunächst einen Regler für ein nominales Modell zu entwerfen und anschließend mithilfe der Erreichbarkeitsanalyse dessen Robustheit gegenüber Störungen und Modellunsicherheiten zu verifizieren. Dieses sequentielle Vorgehen scheitert jedoch häufig, da Unsicherheiten in der Entwurfsphase des Reglers nicht explizit berücksichtigt werden. Um diese Einschränkung zu überwinden, konzentriert sich unsere Forschung auf die Entwicklung von Reglern nach dem Safe-by-Construction Prinzip. Diese Methoden integrieren die Erreichbarkeitsanalyse direkt in den Entwurfsprozess, sodass Regler entstehen, welche robuste Sicherheit gegenüber Störungen, Modellunsicherheiten, Messfehlern und Stellgrößenbeschränkungen garantieren (CDC 2018, TAC 2021, HSCC 2021, Automatica 2022).

Sichere Reinforcement-Learning-Verfahren und Verifikation neuronaler Netze

Während künstliche Intelligenz in einer Vielzahl von Anwendungen bemerkenswerte Erfolge erzielt hat, bleibt das Fehlen strenger Sicherheitsgarantien eine zentrale Herausforderung. Diese Problematik wird durch die begrenzte Interpretierbarkeit neuronaler Netze zusätzlich verschärft, da oft schwer nachvollziehbar ist, was genau gelernt wurde. Um diesen Herausforderungen zu begegnen, entwickeln wir sowohl Methoden zur Open-Loop-Verifikation, bei der das neuronale Netz isoliert analysiert wird (NASA 2023), als auch zur Closed-Loop-Verifikation, bei der das Netz als Regler für ein dynamisches System fungiert (NASA 2023). Darüber hinaus arbeiten wir an sicheren Reinforcement-Learning-Verfahren, welche Safety-Shields verwenden, um zu verhindern, dass der Agent unsichere Aktionen ausführt (Open Journal of Control Systems 2023). Gemeinsam ermöglichen diese Ansätze die Bereitstellung formaler Sicherheitsgarantien für Systeme mit KI-Komponenten und tragen damit zu einem zuverlässigen Einsatz von KI in sicherheitskritischen Anwendungen bei.

Konforme Systemidentifikation

Die manuelle Modellierung des dynamischen Verhaltens eines Systems ist häufig zeitaufwendig und arbeitsintensiv, weshalb es vorteilhaft ist, die Systemdynamik direkt aus Messdaten zu erlernen. Dieser Prozess wird als Systemidentifikation bezeichnet. Unsere Forschung konzentriert sich insbesondere auf das Lernen hybrider Automaten aus verrauschten Daten (HSCC 2025) sowie auf Systemidentifikation mittels Koopman-Operator-Linearisierung (ATVA 2023). Die zentrale Idee des Koopman-Ansatzes besteht darin, das System in einen höherdimensionalen Zustandsraum zu überführen, in dem sich die Dynamik gut durch ein lineares Modell approximieren lässt. Da viele Aufgaben, wie Verifikation und Regelung, für lineare Systeme deutlich effizienter lösbar sind als für nichtlineare, bieten Koopman-basierte Modelle in zahlreichen Anwendungen erhebliche Vorteile (CAV 2022, HSCC 2024). Für die formale Verifikation sind jedoch rein approximative Modelle aus der Systemidentifikation nicht ausreichend. Stattdessen werden überapproximierende Modelle benötigt, die alle möglichen Verhaltensweisen des realen Systems umfassen. Solche Modelle lassen sich durch konforme Synthese konstruieren, für die wir spezialisierte Algorithmen für Koopman-linearisierte (CDC 2022) und hybride Systeme (ASP-DAC 2020) entwickelt haben.

Mengenbasiertes Rechnen

Die Effizienz von Algorithmen, welche mit Mengen rechnen, wie etwa Erreichbarkeitsanalyse und abstrakte Interpretation, hängt maßgeblich von der verwendeten Mengendarstellung ab. Ein zentraler Schwerpunkt unserer Forschung liegt daher auf der Entwicklung neuartiger Mengendarstellungen, die eine besonders effiziente Berechnung aller grundlegenden Mengenoperationen wie Vereinigungen, Schnitte, und Minkowski-Summen ermöglichen. In früheren Arbeiten haben wir mit Sparse Polynomial Zonotopes (TAC 2020) und Constrained Polynomial Zonotopes (Acta Informatica 2023) bereits zwei nichtkonvexe Mengendarstellungen eingeführt, die unter allen wesentlichen Mengenoperationen geschlossen sind. Eine weitere Herausforderung ist, dass die Anwendung von Mengenoperationen häufig zu einem erheblichen Anwachsen der Repräsentationsgröße führt. Daher konzentriert sich unsere aktuelle Forschung auch auf die Entwicklung neuartiger Methoden zur Begrenzung dieses Wachstums und der damit verbundenen Aufrechterhaltung der rechnerischen Effizienz (Control Systems Letters 2025).