Theorie und Anwendungen der Erreichbarkeitsanalyse im diskreten Raum

• Antragsteller: Professor Dr. Amr Alanwar
• Fachliche Zuordnung: Automatisierungstechnik, Mechatronik, Regelungssysteme, Intelligente Technische Systeme, Robotik
• Förderung: Förderung seit 2025
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 564740977

Die Erreichbarkeitsanalyse ist ein wichtiges Werkzeug in Kontrollsystemen, um das Verhalten logischer Systeme formal zu überprüfen und unerwünschte Zustände zu verhindern. Bei logischen Systemen über booleschen Vektorräumen wächst die Rechenkomplexität jedoch exponentiell mit der Dimension, was eine große Herausforderung darstellt. Dieser "Fluch der Dimensionalität" macht innovative Ansätze zur Verringerung der Komplexität erforderlich. Inspiriert von der Effektivität der mengenbasierten Theorie in realen Vektorräumen werden in diesem Vorschlag neuartige Anwendungen meiner zuvor vorgeschlagenen binären Mengendarstellungen - logische Zonotope und polynomiale logische Zonotope - vorgestellt, die durch XOR-Verknüpfung eines binären Vektors mit einer Kombination anderer binärer Vektoren, den sogenannten Generatoren, konstruiert werden. Es wird ein Ansatz für die formale Verifikation von logischen Systemen entwickelt, um mit unsicheren Eingaben unter Verwendung von Binärmengen umzugehen. Dabei werden logische Zonotope und polynomiale logische Zonotope genutzt, die in der Lage sind, bis zu 2^n Punkte mit nur n Generatoren darzustellen, effiziente logische Operationen im Generatorraum zu ermöglichen und die Erreichbarkeitsanalyse zu rationalisieren. Anstatt einzelne Eingaben zu verifizieren, gewährleisten die vorgeschlagenen Methoden Korrektheit und Sicherheit, indem sie erreichbare Mengen von Systemausgaben berechnen und dabei binäre Mengen nutzen. Darüber hinaus wird eine Strategie innerhalb des Generatorraums binärer Mengen vorgeschlagen, die die Effizienz der Modellprüfung anhand linearer temporaler Logikspezifikationen erhöht. Darüber hinaus wird die Anwendung von Binärmengendarstellungen auf die Suche nach Verschlüsselungsschlüsseln ausgedehnt, um unsichere Verschlüsselungssysteme zu erkennen, indem sie in ein vorwärtsmodellbasiertes Erreichbarkeitsanalyseproblem mit dem unsicheren Bit-Schlüssel umgewandelt wird, der 0 und 1 in einer Menge enthält. Durch die Nutzung der Mengenlehre zur Darstellung von Mengen unsicherer Bits verbessert dieser Ansatz die Effizienz der erschöpfenden Schlüsselsuche erheblich, da für jedes Bit gleichzeitig sowohl 0- als auch 1-Schlüsselwerte untersucht werden. Unter Berücksichtigung der Nachrichten und ihrer Chiffretexte besteht das Ziel darin, die Verschlüsselung unter Verwendung von Schlüsselmengen durchzuführen, was zu einer entsprechenden Menge von Chiffretexten führt. Wenn der gegebene Chiffretext nicht zur Menge der Chiffren gehört, kann ich die Menge der Schlüssel getrost aus meiner erschöpfenden Suche ausschließen. Andernfalls kann ich diese Schlüsselmenge in kleinere Teilmengen unterteilen und die Suche fortsetzen, bis ich den geheimen Schlüssel gefunden habe. Insgesamt zielt dieser Vorschlag darauf ab, die Erreichbarkeitsanalyse als eine wirksame Methode zu unterstreichen, die auf verschiedene Probleme anwendbar ist, einschließlich digitaler Verifikation, Modellprüfung und erschöpfender Schlüsselsuche.

• DFG-Verfahren: Emmy Noether-Nachwuchsgruppen
• Internationaler Bezug: Schweden
• Kooperationspartner: Professor Karl Henrik Johansson, Ph.D.