Skalierbare formale Methoden für cyber-physische Systeme durch Generator-basierte Mengenrepräsentationen

• Antragsteller: Professor Dr.-Ing. Matthias Althoff
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung seit 2025
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 556510606

Es gibt zwar bereits Methoden, mit denen sich cyber-physische Systeme mit einer gemischten diskreten/kontinuierlichen Dynamik formal verifizieren lassen, doch werden sie nur dann eine weite Verbreitung finden, wenn diese Methoden skalierbarer werden. In den letzten Jahren wurden viele der größten Fortschritte in Richtung skalierbarerer Ansätze durch neue Mengenrepräsentationen erzielt. Basierend auf einer kürzlich gemachten Entdeckung schlagen wir neuartige generatorbasierte Mengendarstellungen vor. Die Grundlage unserer zu entwickelnden Mengendarstellungen ist eine neuartige Art der Darstellung von Polytopen. Obwohl Polytope mindestens seit dem 19. Jahrhundert erforscht werden, war die Komplexität der Minkowski-Summe aufgrund der großen Anzahl der resultierenden Flächen bisher enorm. So ist beispielsweise die Anzahl der erforderlichen Eckpunkte exponentiell zur Dimension des Raums. Unsere neuartige Mengendarstellung ermöglicht es jedoch, die Minkowski-Summe von Polytopen mit linearer Komplexität in Bezug auf die Systemdimension zu berechnen. Da die Minkowski-Summe eine zentrale Operation für die formale Verifikation von cyber-physischen Systemen ist, wird unsere neuartige Mengendarstellung es ermöglichen, Systeme mittels Polytope in polynomieller Zeit in Bezug auf die Systemdimension formal zu verifizieren. Insbesondere werden in diesem Projekt erforscht: a) skalierbare Mengenrepräsentationen, die für verschiedene Algorithmen angepasst werden können; b) effiziente und enge Überapproximationen von Operationen, um polynomielle Komplexität in Bezug auf die Dimension des Raums zu erreichen; und c) effiziente Ordnungsreduktionstechniken für Mengenrepräsentationen. Die noch zu entwickelnden Erweiterungen unserer neuen Mengendarstellung für Polytope werden es ermöglichen, nicht-konvexe Mengen mit Löchern darzustellen, die die vorteilhaften Eigenschaften für die Berechnung von Minkowski-Summen, linearen Abbildungen und konvexen Hüllen erben. Wir werden unseren Ansatz nicht nur an ARCH-Benchmarks, sondern auch an Energiesystemen im CoSES-Labor der Technischen Universität München demonstrieren.

• DFG-Verfahren: Sachbeihilfen