Durchbruch in der Überprüfung cyber-physischer Systeme

In der Welt der formalen Logik und der mathematischen Modelle, die für cyber-physische Systeme und die Planung von Roboterbewegungen verwendet werden, sind bestimmte Aussagen sehr wichtig. Diese Aussagen benutzen die Wörter "es gibt" und "für alle”. Sie sind jedoch schwer für Menschen und Computer zu verstehen, sobald es um cyber-physische Systeme geht, und nicht nur um Aussagen wie “es gibt eine reelle Zahl deren Quadrat 5 ist” oder “alle reellen Zahlen haben nicht-negative Quadrate”. Der beste Weg, diese Aussagen zu analysieren, ist ein Prozess namens Quantorenelimination (QE). QE wandelt diese komplizierten Aussagen in einfachere aber äquivalente Formeln um, die ohne die Wörter "es gibt" und "für alle" auskommen. Diese einfacheren Formeln können leicht ausgewertet werden.

Für die Sicherheit cyber-physischer Systeme ist es entscheidend, dass die QE-Algorithmen korrekt funktionieren. Um dies sicherzustellen, können die Algorithmen in einen Theorembeweiser implementiert und ihre Richtigkeit mathematisch bewiesen werden. Diese Beweise sind sehr genau, weil sie sich nur auf einen kleinen und vertrauenswürdigen Kern des Programms stützen.

In ihrer Dissertation „Formale Verifikation von Algorithmen zur Quantorenelimination“ unter der Betreuung von Prof. André Platzer hat sich Katherine Kosaian auf diese Problemstellung fokussiert. Kosaian formalisiert die virtuelle Substitution als eine unvollständige, aber praktisch relevante Quantoreneliminierungstechnik und liefert verifizierte Algorithmen mittels Codegenerierung, die experimentell mit nicht verifizierten Algorithmen auf dem neuesten Stand der Technik wettbewerbsfähig ist, aber eben beweisbar korrekt. Neben der virtuellen Substitution behandelt die Doktorarbeit auch vollständige Quantoreneliminierungsalgorithmen. Insbesondere bietet sie den ersten Algorithmus für das vollständige Setting mit Formeln und Quantoren von multivariaten Polynomen, der formal in Isabelle/HOL verifiziert ist.

„Katherine Kosaians Arbeit ist ein bedeutender Fortschritt in der formalen Verifikation und bietet neue Werkzeuge und Methoden, die helfen, sicherere und zuverlässigere cyber-physische Systeme und Roboterbewegungsplanungen zu entwickeln“, erklärt Professor Platzer. Für ihre theoretischen und praktischen Beiträge zur formal verifizierten Quantorenelimination erhielt die Wissenschaftlerin auf der 12. International Conference on Automated Deduction (CADE) den renommierten Bill McCune PhD Award 2024.

Preisträgerin Katherine Kosaian mit Doktorvater André Platzer (links) und Carsten Fuhs (Bild: Jürgen Giesl)

Katherine Kosaian hat bis 2023 bei Prof. André Platzer an der Carnegie Mellon University promoviert und startet nun nach einem Postdocjahr an der Iowa State University als Assistant Professor an der University of Iowa. Platzer hat die Alexander von Humboldt-Professur für Logik autonomer dynamischer Systeme am Karlsruher Institut für Technologie inne und ist Gründer des Logical Systems Lab an der Carnegie Mellon University. In seiner Forschung beschäftigt er sich mit der Entwicklung und Anwendung von differentiellen dynamischen Logiken und hat einen entscheidenden Beitrag zur Sicherheitsprüfung von cyber-physischen Systemen etwa im Verkehr, in der Luft- und Schifffahrt oder der Robotik geliefert.