Synthesis and analysis of neural-network-based control in cyber-physical systems

Antal, László; Ábrahám, Erika; Madureira, Ana Maria

doi:10.18154/RWTH-2026-04618

Synthesis and analysis of neural-network-based control in cyber-physical systems

Antal, László^RWTH*

2026

Verantwortlichkeitsangabevorgelegt von László Antal, Master of Science

ImpressumAachen : RWTH Aachen University 2026

Umfang1 Online-Ressource : Illustrationen

Dissertation, RWTH Aachen University, 2026

Veröffentlicht auf dem Publikationsserver der RWTH Aachen University

Genehmigende Fakultät
Fak09

Hauptberichter/Gutachter
Ábrahám, Erika (Thesis advisor)^RWTH* ; Madureira, Ana Maria (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2026-04-16

Online
DOI: 10.18154/RWTH-2026-04618
URL: https://publications.rwth-aachen.de/record/1034305/files/1034305.pdf

Einrichtungen

Lehr- und Forschungsgebiet Theorie Hybrider Systeme (123420)

Projekte

Inhaltliche Beschreibung (Schlagwörter)
autonomous systems (frei) ; control synthesis (frei) ; cyber-physical systems (frei) ; deep learning (frei) ; formal methods (frei) ; neural network verification (frei) ; object detection (frei) ; reachability analysis (frei) ; robustness (frei) ; underwater robotics (frei)

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
Autonome Unterwasserfahrzeuge stützen sich zunehmend auf tiefenlern-basierte Methoden für Wahrnehmung, Steuerung und Entscheidungsfindung in marinen Umgebungen, die durch starkes Sensorrauschen, eingeschränkte Kommunikation und hohe Umweltunsicherheit gekennzeichnet sind. Obwohl neuronale Netze in solchen Szenarien eine beeindruckende empirische Leistungsfähigkeit zeigen, wirft ihr Einsatz in sicherheits- und missionskritischen Anwendungen grundlegende Fragen hinsichtlich Zuverlässigkeit, Robustheit und funktionaler Korrektheit auf. Diese Dissertation adressiert diese Herausforderungen durch die Kombination von Methoden zur robusten Synthese neuronaler Netze mit formalen Analyseverfahren, die mathematisch fundierte Garantien über deren Verhalten liefern. Auf der Syntheseseite untersucht diese Arbeit datengetriebene Lernansätze für die Unterwasserrobotik. Wir entwickeln einen auf neuronalen Netzen basierenden Kollisionsvermeidungsregler für Bottom-Tracking-Missionen und zeigen dessen verbesserte Anpassungsfähigkeit unter verrauschten Sensorbedingungen im Vergleich zu einem traditionellen regelbasierten Ansatz. Für die Unterwasserwahrnehmung untersuchen wir die Objekterkennung in Side-Scan-Sonar-Bildern, deren Rauschcharakteristika und Objektstrukturen sich stark von natürlichen Bildern unterscheiden. Wir stellen eine Objekterkennungsarchitektur vor, die einen modernen One-Stage-Detektor um eine Vision-Transformer-Schicht erweitert, und setzen Knowledge Distillation ein, um kompakte und effiziente Modelle für den Einsatz auf eingebetteter Hardware zu erhalten. Zur weiteren Verbesserung der Robustheit schlagen wir ein Verfahren vor, das Knowledge Distillation mit adversarialem Retraining kombiniert, das durch formal spezifizierte Sicherheitseigenschaften gesteuert wird, wodurch die Robustheit gegenüber sonarspezifischen Störungen verbessert wird, ohne die Erkennungsgenauigkeit zu beeinträchtigen. Auf der Analyseebene erweitert diese Arbeit die erreichbarkeitsbasierte Verifikation neuronaler Netze auf Basis von Star-Mengen für Feedforward-Netze. Wir erweitern bestehende Verifikationsmethoden, um die gesamte Klasse stückweise linearer Aktivierungsfunktionen sowie sowohl beschränkte als auch unbeschränkte Eingabemengen zu unterstützen, und liefern dabei korrekte und enge konvexe Überapproximationen erreichbarer Mengen. Darüber hinaus untersuchen wir die Abwägungen zwischen exakter und überapproximativer Analyse hinsichtlich Vollständigkeit, Skalierbarkeit und Präzision. Zur Überwindung von Skalierungsproblemen führen wir ein Framework zur gegenbeispielgesteuerten Abstraktionsverfeinerung ein, das relaxierte Analysen mit gezielten exakten Verfeinerungen auf Basis von Schein-Gegenbeispielen kombiniert. Das resultierende Verifikationsverfahren ist sowohl korrekt als auch vollständig und verbessert gleichzeitig die Effizienz gegenüber exakten Ansätzen.

Autonomous underwater vehicles increasingly rely on deep-learning-based methods for perception, control, and decision making in submarine environments characterized by severe sensor noise, limited communication, and strong environmental uncertainty. While neural networks demonstrate impressive empirical performance in such settings, their deployment in safety- and mission-critical applications raises fundamental concerns regarding reliability, robustness, and functional correctness. This thesis addresses these challenges by combining techniques for the robust synthesis of neural networks with formal analysis methods providing mathematically rigorous guarantees of their behaviour. On the synthesis side, this thesis investigates data-driven learning approaches for underwater robotics. We develop a neural-network-based collision-avoidance controller for bottom-tracking missions and demonstrate its improved adaptability under noisy sensor conditions compared to a traditional rule-based approach. For underwater perception, we study object detection in side-scan sonar imagery, where noise characteristics and object appearance differ greatly from those in natural images. We introduce an object-detection architecture that extends a modern one-stage detector with a vision transformer layer and apply knowledge distillation to obtain compact and efficient models suitable for deployment on embedded hardware. To further improve robustness, we propose a framework that combines knowledge distillation with adversarial retraining guided by formally specified safety properties, resulting in improved robustness against sonar-specific perturbations while preserving detection accuracy. On the analysis side, this thesis advances star-set-based reachability analysis for feedforward neural networks. We extend existing verification techniques to support the full class of piecewise-linear activation functions and both bounded and unbounded input sets, providing sound and tight convex over-approximations of reachable sets. We study the trade-offs between exact and over-approximative analysis in terms of completeness, scalability, and precision. To overcome scalability limitations, we introduce a counterexample-guided abstraction refinement framework that combines relaxed analysis with targeted exact refinements based on spurious counterexamples. The resulting verification method is sound and complete while improving efficiency compared to the exact approach.

OpenAccess:
PDF
(additional files)