⚡ electrical engineering

A Pragmatic Guide to Building Conservative Discrete Abstractions of Cyber-Physical Systems

Dieses Paper präsentiert einen pragmatischen, konstruktionsbedingt konservativen Workflow zur Erstellung diskreter Abstraktionen von cyber-physischen Systemen, der durch die Adressierung gängiger Fallstricke mittels eines modularen vierstufigen Prozesses, bestehend aus Zustandsraumpartitionierung, konservativer Übergangskonstruktion, Milderung spurioser Verhaltensweisen und sounder Spezifikationshebung, fundierte Verifikationsgarantien sicherstellt.

Ursprüngliche Autoren: Jordan Peper, Krish Kapadia, James Gast, Ethan Howes, Ivan Ruchkin

Veröffentlicht 2026-08-12

📖 7 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Jordan Peper, Krish Kapadia, James Gast, Ethan Howes, Ivan Ruchkin

Originalarbeit lizenziert unter CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dies ist eine KI-generierte Erklärung des untenstehenden Papers. Sie wurde nicht von den Autoren verfasst oder gebilligt. Für technische Genauigkeit konsultieren Sie das Originalpaper. Vollständigen Haftungsausschluss lesen

Stellen Sie sich vor, Sie versuchen, einem Roboter beizubringen, ein Auto durch eine belebte Stadt zu steuern. Die reale Welt ist chaotisch und kontinuierlich; das Auto kann sich an jedem exakten Punkt auf der Straße befinden, mit jeder exakten Geschwindigkeit fahren und in jedem exakten Winkel lenken. Aber Computer, insbesondere solche, die beweisen müssen, dass ein Roboter sicher ist, bevor er sich überhaupt bewegt, haben Schwierigkeiten mit unendlichen Möglichkeiten. Sie arbeiten am besten mit endlichen Listen, wie bei einem Brettspiel mit einer festen Anzahl von Feldern. Dies ist das Herzstück von Cyber-Physischen Systemen (CPS): der Verschmelzung von digitalen Gehirnen und physischen Körpern. Um zu prüfen, ob ein Roboter kollidieren wird, verwenden Ingenieure eine Methode namens symbolische Modellprüfung. Betrachten Sie dies als einen superpräzisen Detektiv, der jede einzelne mögliche Bewegung eines Roboters prüft, um sicherzustellen, dass er niemals gegen eine Wand fährt. Aber um dies zu tun, muss der Detektiv die fließende, sanfte reale Welt in eine blockartige, schrittweise Karte verwandeln. Dieser Prozess wird diskrete Abstraktion genannt.

Der knifflige Teil ist: Wenn man die Karte zu einfach gestaltet, übersieht man vielleicht eine echte Gefahr (der Roboter kollidiert in der Realität, sieht aber auf der Karte sicher aus). Wenn man die Karte zu kompliziert macht, wird der Detektiv überfordert und kann die Aufgabe nicht abschließen. Das Ziel ist es, eine Karte zu erstellen, die „konservativ“ ist – das heißt, sie mag einige Gefahren imaginieren, die eigentlich nicht existieren (Pessimismus), aber sie wird niemals eine echte Gefahr übersehen. Dieses Paper dient Ingenieuren als Leitfaden, wie sie diese Karten korrekt erstellen, um häufige Fallen zu vermeiden, die zu falschen Sicherheitsgarantien führen.

Der Bauplan für eine sichere Roboterkarte

Dieses Paper fungiert als pragmatischer Leitfaden für den Bau „konservativer“ Karten komplexer Maschinen. Das Team der Autoren von der University of Florida argumentiert, dass es zwar notwendig ist, einen kontinuierlichen Roboter in ein blockartiges Spiel zu verwandeln, um Sicherheitsprüfungen durchzuführen, viele Ingenieure jedoch versehentlich Karten bauen, die entweder zu gefährlich (reale Risiken übersehend) oder zu paranoid (imaginäre Risiken erfindend) sind. Sie schlagen einen vierstufigen Workflow vor, um diese Abstraktionen „durch Konstruktion“ zu erstellen, wodurch sichergestellt wird, dass die Karte durch Design immer sicher ist.

Schritt 1: Die Welt in Kacheln schneiden

Zuerst müssen Sie den glatten, unendlichen Zustandsraum (in dem sich der Roboter überall befinden kann) in ein Gitter aus endlichen Kacheln verwandeln. Stellen Sie sich vor, Sie nehmen ein riesiges, kontinuierliches Blatt Graphpapier und schneiden es in unterschiedliche, sich nicht überschneidende Quadrate. Jedes Quadrat repräsentiert eine „Kachel“ oder einen abstrakten Zustand. Die Autoren schlagen die Verwendung eines gleichmäßigen Gitters vor, ähnlich einem Schachbrett, bei dem Sie entscheiden, wie viele Kacheln Sie entlang jeder Dimension (Länge, Breite, Winkel) haben möchten. Wenn Sie sich für 10 Kacheln für jede der drei Dimensionen eines Einrad-Roboters entscheiden, erhalten Sie insgesamt 1.000 Kacheln ( $10 \times 10 \times 10$ ). Dieser Schritt stellt sicher, dass jede mögliche reale Position, an der sich der Roboter befinden könnte, von mindestens einer Kachel abgedeckt wird.

Schritt 2: Die Pfeile zeichnen (Der knifflige Teil)

Nun müssen Sie herausfinden, zu welchen Kacheln der Roboter von seiner aktuellen Kachel aus springen kann. Hier bietet das Paper drei verschiedene Werkzeuge an, die jeweils eine andere Nuance von „Konservatismus“ besitzen:

Die Begrenzungsbox (AABB): Stellen Sie sich vor, der Roboter befindet sich in einer Kachel. Sie berechnen, wo er sich nach einer Sekunde möglicherweise befinden könnte. Um sicher zu gehen, zeichnen Sie das kleinstmögliche Rechteck (Axis-Aligned Bounding Box), das all diese möglichen zukünftigen Orte vollständig umschließt. Wenn dieses Rechteck eine benachbarte Kachel berührt, zeichnen Sie einen Pfeil zu dieser Kachel. Es ist, als würde man die Zukunft des Roboters in eine große, klobige Box einpacken. Es ist schnell, aber die Box könnte zu groß sein, was „falsche“ Pfeile zu Kacheln erzeugt, die der Roboter eigentlich niemals erreichen könnte.
Das Polytope: Dies ist eine dichtere, flexiblere Form (wie ein gedehntes Gummituch), die sich enger an die Zukunft des Roboters anschmiegt als eine Box. Es ist genauer, benötigt aber mehr Rechenleistung zur Berechnung.
Die Sampling-Methode (PAC): Anstatt jede Möglichkeit zu berechnen, werfen Sie Dartpfeile. Sie wählen zufällige Startpunkte innerhalb der Kachel, simulieren, wohin der Robot geht, und protokollieren die beobachteten Pfeile. Das Paper führt ein cleveres „Zertifikat“ (eine statistische Garantie) ein, das besagt: „Wir sind zu 99 % sicher, dass wir jeden Pfeil gesehen haben, der häufiger als 1 % der Zeit auftritt.“ Dies ist ideal für komplexe Black-Box-Roboter, bei denen man keine perfekte Formel aufschreiben kann, basiert jedoch auf Wahrscheinlichkeit statt auf absolutem Beweis.

Schritt 3: Das „Aufräumen“ der falschen Pfade

Da die Methoden in Schritt 2 konservativ sind, erzeugen sie oft spure (scheinbare) Übergänge – Pfeile, die auf der Karte zwar existieren scheinen, in der Realität aber unmöglich sind. Schlimmer noch, sie erzeugen oft Selbstschleifen (Self-Loops), bei denen die Karte behauptet, der Roboter könne in derselben Kachel für immer verbleiben. Dies ist ein Albtraum für Sicherheitsprüfungen, denn wenn ein Roboter ewig in einer Kachel bleiben kann, erreicht er unter Umständen sein Ziel nie, selbst wenn er es in der Realität könnte.

Das Paper schlägt zwei Wege vor, um dies zu bereinigen:

CEGAR (Counterexample-Guided Abstraction Refinement): Wenn der Sicherheitsprüfer einen „falschen“ Pfad findet, bei dem der Roboter kollidiert, teilt das System die Kacheln entlang dieses Pfades auf, um die Karte detaillierter zu gestalten und so den falschen Pfad effektiv zu löschen.
Löschen von Selbstschleifen (Self-Loop Erasure): Die Autoren zeigen, wie man beweist, dass ein Roboter innerhalb einer bestimmten Anzahl von Schritten eine Kachel verlassen muss. Wenn Sie beweisen können, dass der Roboter nicht ewig dort bleiben kann, können Sie den „Bleib für immer hier“-Pfeil sicher löschen. Sie haben dies am „Mountain Car“-Problem und einem „Einrad“-Roboter getestet und gezeigt, dass das Entfernen dieser falschen Schleifen die Genauigkeit der Sicherheitsprüfungen erheblich verbessert hat.

Schritt 4: Die Regeln übersetzen

Schließlich müssen Sie die Sicherheitsregeln aus der realen Welt in die blockartige Karte übersetzen. Wenn die Regel lautet: „Bleibe innerhalb der Stadtgrenzen“, bedeutet dies auf der realen Karte: „Berühre nicht den Rand“. Auf der blockartigen Karte ändert sich die Regel. Das Paper erklärt, wie man die „May“- und „Must“-Logik verwendet. Eine Regel „Muss“ (Must) nur dann für eine Kachel gelten, wenn jeder Punkt in dieser realen Kachel die Regel erfüllt. Eine Regel „Kann“ (May) gilt, wenn mindestens ein Punkt sie erfüllt. Durch die sorgfältige Übersetzung der Regeln stellen sie sicher, dass der Roboter, wenn er den Test auf der blockartigen Karte besteht, garantiert auch in der realen Welt sicher ist.

Was sie herausgefunden haben

Die Autoren testeten diese vierstufige Pipeline in drei Szenarien: einem einfachen synthetischen System, einem „Mountain Car“ (eine klassische Herausforderung des Reinforcement Learning) und einem autonomen Einrad.

Sie fanden heraus, dass die Sampling-basierte Methode (Schritt 3) oft die saubersten Karten mit den wenigsten falschen Pfeilen und Selbstschleifen lieferte, insbesondere für komplexe, nicht-lineare Roboter wie das Einrad. Während die „Bounding Box“-Methode schneller aufzubauen war, erzeugte sie so viele falsche Pfade, dass der Sicherheitsprüfer größere Schwierigkeiten hatte, die Sicherheit des Roboters zu beweisen.

Entscheidend war, dass das Löschen von Selbstschleifen (Schritt 3) einen gewaltigen Unterschied machte. Für das Einrad verbesserte das bloße Löschen der falschen „Bleib für immer“-Pfeile die Erfolgsquote der Sicherheitsprüfung in einigen Fällen von etwa 19 % auf über 60 %. Dies beweist, dass eine etwas komplexere, aber „sauberere“ Karte oft besser ist als eine einfache Karte voller falscher Möglichkeiten.

Das Paper kommt zu dem Schluss, dass Ingenieure durch die Befolgung dieses strukturierten, konservativen Workflows – Partitionierung des Raums, sorgfältiger Aufbau der Übergänge, Bereinigung falscher Pfade und korrekte Übersetzung der Regeln – digitale Zwillinge physischer Roboter bauen können, die vertrauenswürdig sind. Sie behaupten nicht, alle Probleme der Robotik gelöst zu haben, aber sie bieten ein klares, getestetes Rezept, um die häufigsten Fehler zu vermeiden, die zu unsicheren oder nutzlosen Sicherheitsprüfungen führen.

Technisches Resümee: Ein pragmatischer Leitfaden zur Konstruktion konservativer diskreter Abstraktionen von cyber-physischen Systemen

Problemstellung

Cyber-physische Systeme (CPS) operieren in sicherheitskritischen Umgebungen, in denen Ausfälle Leben und Sachwerte gefährden können. Während das symbolische Model Checking eine effektive Methode zur Verifizierung komplexer Temporal-Logik-Eigenschaften ist, erfordert es ein endlichen Zustandsmodells. Reale CPS entwickeln sich jedoch über kontinuierliche Zustandsräume. Um Model Checking anwenden zu können, müssen Ingenieure diese kontinuierlichen Dynamiken in eine endliche Zustandsabstraktion diskretisieren.

Die zentrale Herausforderung liegt in der Gewährleistung der Korrektheit (Soundness): Die aus dem abstrakten Modell abgeleiteten Verifizierungsgarantien müssen auf das konkrete System übertragbar sein. Dies erfordert, dass die Abstraktion eine konservative Überapproximation des konkreten Zustandsraums und der Verhaltensweisen ist. In der Praxis stoßen Modellbauer häufig auf vier Fallstricke, welche die Korrektheit gefährden oder zu übermäßiger Pessimismus führen:

Unterdeckung (Under-covering) des konkreten Zustandsraums.
Unterapproximation der Übergangsrelation (Auslassen zulässiger Verhaltensweisen).
Unkorrekte Eliminierung (Unsound Pruning) von „degenerierten“ Verhaltensweisen (z. B. das Entfernen von Selbstschleifen ohne Zertifizierung).
Fehlerhaftes Lifting der Spezifikation, wodurch die logische Implikation von der abstrakten Erfüllung zur konkreten Erfüllung nicht gewahrt bleibt.

Diese Probleme führen oft zu „spuriösen“ Gegenbeispielen, bei denen das abstrakte Modell eine Spezifikation verletzt, die das konkrete System tatsächlich erfüllt, was die Verifizierung unbrauchbar macht.

Methodik

Das Paper schlägt einen vierstufigen, modularen Workflow für die Konstruktion konservativer diskreter Abstraktionen vor. Der Workflow ist „konservativ durch Konstruktion“ (conservative-by-construction), was bedeutet, dass die Korrektheit in jeder Stufe durch spezifische mathematische Garantien aufrechterhalten wird.

Schritt 1: Zustandsraum-Abstraktion

Der kontinuierliche Zustandsraum $X$ wird unter Verwendung eines gleichmäßigen rechtwinkligen Gitters in eine endliche Menge abstrakter Zustände $\hat{X}$ partitioniert. Eine Quantisierungsfunktion $\psi: X \to \hat{X}$ bildet konkrete Zustände auf abstrakte Zellen ab. Die inverse Abbildung $\Psi(\hat{x})$ definiert die konkrete Region (Präimage) jedes abstrakten Zustands. Dieser Schritt stellt sicher, dass jeder konkrete Zustand und jede Anfangsbedingung einen Repräsentanten im abstrakten Modell hat.

Schritt 2: Konstruktion der konservativen Übergangsrelation

Das Paper präsentiert drei austauschbare Methoden zur Berechnung der Übergangsrelation $\hat{f}$ (d. h. zur Bestimmung, welche abstrakten Zustände auf andere folgen können), wobei sichergestellt wird, dass jeder konkrete Übergang im abstrakten Modell repräsentiert ist:

Achsenparallele Begrenzungsbox (AABB): Berechnet die Begrenzungsbox des Bildes einer konkreten Zelle unter den Systemdynamiken. Jede abstrakte Zelle, die diese Box schneidet, wird als Nachfolger hinzugefügt. Dies ist recheneffizient, kann aber für nichtlineare Systeme übermäßig konservativ sein.
Polytop-Propagation: Verwendet ein Polytop (konvexe Hülle), um das Bild der konkreten Zelle zu approximieren. Dies ist präziser als AABB für nichtlineare Dynamiken, aber rechenintensiver. Es nutzt AABB-Culling, um Kandidaten zu filtern, bevor aufwendige Polytop-Schnitttests durchgeführt werden.
Sampling mit PAC-Zertifikaten: Für Black-Box-Systeme oder hochgradig nichtlineare Systeme werden Übergänge durch Sampling des Zustandsraums entdeckt. Anstatt einer deterministischen Garantie bietet diese Methode eine wahrscheinlichkeitsbasierte (Probably Approximately Correct, PAC) Garantie. Sie zertifiziert, dass die konstruierte Übergangsrelation mit hoher Konfidenz ( $1-\delta$ ) alle „signifikanten“ Übergänge (jene, die mit einer Wahrscheinlichkeit $\ge \beta$ auftreten) enthält, indem sie die „fehlende Masse“ unobservierter Übergänge begrenzt.

Schritt 3: Minderung degenerierter Verhaltensweisen

Konservative Abstraktionen führen oft spurische Übergänge (Übergänge, die im konkreten System unmöglich sind) und Selbstschleifen (Übergänge von einem Zustand zu sich selbst) ein. Diese können zu falsch-negativen Ergebnissen in der Verifizierung führen, insbesondere bei Liveness-Eigenschaften.

Spurische Übergänge: Werden mittels Counterexample-Guided Abstraction Refinement (CEGAR) adressiert. Wenn eine Spur eines Gegenbeispiels im abstrakten Modell gefunden wird, validiert der Algorithmus dieses gegen die konkrete Dynamik. Wenn die Trajektorie spuriös ist (die erreichbare Menge wird leer), wird der Zustandsraum verfeinert (gespalten), um den falschen Übergang zu eliminieren.
Selbstschleifen: Werden durch zertifizierte Selbstschleifen-Eliminierung adressiert. Eine Selbstschleife wird nur entfernt, wenn zertifiziert werden kann, dass jede konkrete Trajektorie, die in dieser Zelle startet, innerhalb einer endlichen Anzahl von Schritten ( $K$ ) entweicht. Dies wird entweder durch Iteration der erreichbaren Mengen-Propagation oder über eine Sampling-Strategie mit einer PAC-Garantie verifiziert.

Schritt 4: Korrektes Lifting von LTL-Spezifikationen

Um das abstrakte Modell zu verifizieren, muss die auf dem konkreten Raum $\phi$ definierte LTL-Spezifikation auf eine abstrakte Spezifikation $\hat{\phi}$ gehoben werden. Das Paper verwendet May-Must-Semantik:

Must-Prädikate: Ein atomares Prädikat gilt auf einem abstrakten Zustand nur dann, wenn es für alle konkreten Zustände in dieser Zelle gilt.
May-Prädikate: Ein atomares Prädikat gilt, wenn es für mindestens einen konkreten Zustand gilt.
Der Lifting-Operator $\rho$ transformiert $\phi$ in $\hat{\phi}$ , indem er atomare Prädikate zu „Must“ verstärkt (für Safety) oder zu „May“ abschwächt (wie für die Logikstruktur angemessen), um sicherzustellen, dass $\hat{s} \models \hat{\phi} \implies s \models \phi$ gilt.

Zentrale Beiträge

Ein pragmatischer Workflow: Eine einheitliche, vierstufige Pipeline, die Zustandspartitionierung, Übergangskonstruktion, Minderung degenerierter Verhaltensweisen und Spezifikationslifting in ein einziges korrektes Framework integriert.
Austauschbare Subroutinen: Die Methodik unterstützt mehrere Ansätze für die Übergangskonstruktion (AABB, Polytop, Sampling) und die Entfernung degenerierter Verhaltensweisen (CEGAR, zertifizierte Eliminierung), wodurch Anwender zwischen Rechenaufwand und Abstraktionsgenauigkeit wählen können.
PAC-Garantien für Sampling: Führt einen datengesteuerten Ansatz für die Übergangskonstruktion ein, der rigorose probabilistische Abdeckungszertifikate (über den Good-Turing-Schätzer und McAllester-Schapire-Schranken) für Systeme bereitstellt, bei denen eine analytische Überapproximation unpraktikabel ist.
Systematische Handhabung von Degeneriertheit: Adressiert explizit die Entfernung von spuriösen Selbstschleifen und Übergängen durch zertifizierte Eliminierung und CEGAR, wodurch der Pessimismus verhindert wird, der konservative Abstraktionen typischerweise plagt.

Experimentelle Ergebnisse

Die Autoren evaluierten die Pipeline anhand von drei Fallstudien: ein synthetisches lineares System, den Mountain Car Benchmark (nichtlinear, gelernte Policy) und ein autonomes Unicycle (Dubins-Modell).

Übergangskonstruktion: Sampling-basierte Methoden erzeugten im Vergleich zu AABB- und Polytop-Methoden im Allgemeinen dünnere Übergangsrelationen mit weniger Selbstschleifen und geringerer Variabilität der Nachfolgeranzahl, insbesondere bei nichtlinearen Systemen. Dies führte zu höheren True Positive Rates (TPR) in der Verifizierung.
Selbstschleifen-Eliminierung: Das Entfernen von Selbstschleifen verbesserte die Verifizierungsergebnisse signifikant. Für den Unicycle-Fall stieg die TPR von ~0,19 auf ~0,63 nach der Eliminierung. Im Mountain Car-Fall verbesserte sich die TPR von ~0,83 auf ~0,93.
CEGAR: Während CEGAR die Modellgröße und die Konstruktionszeit erheblich steigerte, reduzierte es konsistent den Anteil der Selbstschleifen (SLP). Es lieferte deutliche TPR-Verbesserungen für das Mountain Car-System, hatte jedoch einen minimalen Einfluss auf das Unicycle-System, wo eine hohe SLP auf triviale Gegenbeispiele zurückgeführt wurde, die ohne gezielte Eliminierung schwer zu beseitigen waren.
Granularität: Feinere Granularitäten des Zustandsraums lieferten konsistent höhere TPR, was den Trade-off zwischen Modellgröße und Verifizierungsgenauigkeit bestätigt.

Bedeutung

Das Paper beansprucht für sich, ein pragmatischer Leitfaden für Ingenieure und Forscher zu sein, die Abstraktionen für CPS erstellen. Es schließt die Lücke zwischen theoretischen Abstraktionstechniken und der praktischen Implementierung durch:

Einen „korrekt durch Konstruktion“ (sound-by-construction) Workflow, der häufige Fehler verhindert, die zu einer unkorrekten Verifizierung führen könnten.
Die Bereitstellung modularer Werkzeuge, die es Praktikern ermöglichen, zwischen deterministischen (AABB/Polytop) und probabilistischen (Sampling) Methoden basierend auf der Systemkomplexität und den verfügbaren Ressourcen zu wählen.
Den Nachweis, dass die Minderung degenerierter Verhaltensweisen (spurische Übergänge und Selbstschleifen) nicht bloß eine Optimierung, sondern ein kritischer Schritt ist, um aussagekräftige Verifizierungsergebnisse zu erzielen, insbesondere für Liveness-Eigenschaften.

Die Autoren kommen zu dem Schluss, dass das symbolische Model Checking zwar leistungsstark ist, sein Nutzen für CPS jedoch vollständig von der Qualität der Abstraktion abhängt. Dieser Workflow bietet einen rigorosen, adaptiven Rahmen, um diese Qualität unter Abwägung von Pessimismus und Praktikabilität zu erreichen.