Time-Varying Reach-Avoid Control Certificates for Stochastic Systems

Dieses Papier stellt ein Rahmenwerk für zeitvariierende und zeitinvariierende Reach-Avoid-Zertifikate für diskrete stochastische Systeme vor, das die Synthese von Reglern und die Verifizierung von Sicherheits- und Zielbedingungen mittels Sum-of-Squares-Optimierung ermöglicht.

Das Wesentliche

Das große Problem: Der unsichere Weg zum Ziel

Stellen Sie sich vor, Sie wollen mit einem Auto von Ihrem Zuhause (dem Start) zu einem Freund nach Hause (dem Ziel). Aber es gibt ein Problem: Auf dem Weg gibt es eine Baustelle oder einen See, in den Sie auf keinen Fall hineinfahren dürfen (die Gefahrenzone).

Zusätzlich ist der Tag sehr neblig und der Boden rutschig. Sie können nicht genau wissen, wohin das Auto genau rollt, wenn Sie lenken. Es ist ein stochastisches System – das bedeutet, es gibt Zufall und Unsicherheit.

Die große Frage lautet: Wie können wir garantieren, dass wir mit einer sehr hohen Wahrscheinlichkeit (z. B. 99 %) sicher beim Ziel ankommen, ohne jemals in die Gefahr zu geraten?

Das ist genau das Problem, das diese Forscher lösen wollen.

Die Lösung: Ein "magischer" Sicherheitszertifikat

Früher haben Forscher versucht, das Auto in winzige Kästchen zu unterteilen (wie ein Schachbrett), um den Weg zu berechnen. Aber wenn das Auto in einer riesigen, komplexen Stadt fährt, wird dieses Schachbrett so groß, dass kein Computer mehr damit rechnen kann.

Diese Forscher haben eine neue Methode entwickelt, die wie ein magischer Sicherheitszertifikat funktioniert. Stellen Sie sich dieses Zertifikat als eine unsichtbare, intelligente Landkarte vor, die dem Auto sagt: "Du bist hier sicher, aber wenn du dorthin fährst, wird es gefährlich."

Das Besondere an dieser neuen Landkarte ist, dass sie zeitabhängig ist.

1. Die statische Landkarte (Zeit-unabhängig)

Stellen Sie sich eine alte, statische Landkarte vor, die für immer gleich bleibt. Sie sagt: "Wenn du hier bist, bist du sicher." Das ist einfach zu berechnen, aber oft nicht präzise genug. Um diese Karte genau genug zu machen, muss man sie extrem kompliziert zeichnen (mit vielen Details), was den Computer sehr langsam macht.

2. Die dynamische Landkarte (Zeit-veränderlich) – Der Clou der Forscher

Die Forscher sagen: "Warum eine einzige Karte für immer verwenden? Warum nicht eine neue Karte für jede Minute der Reise?"

Stellen Sie sich vor, Sie haben einen Wegbegleiter, der Ihnen jede Minute eine neue Anweisung gibt:

• Minute 1: "Du bist noch weit weg vom Ziel, aber pass auf, der See ist links."
• Minute 5: "Jetzt bist du näher am Ziel, aber der See ist rechts."
• Minute 10: "Fast da! Halte geradeaus."

Diese zeitveränderliche Landkarte ist viel flexibler. Sie muss nicht extrem kompliziert gezeichnet sein, weil sie sich ständig anpasst. Das ist wie der Unterschied zwischen einem starren, steifen Anzug (statisch) und einem flexiblen, dehnbaren Sportanzug (dynamisch), der sich perfekt an jede Bewegung anpasst.

Wie funktioniert das im Computer? (Die "Zucker-Methode")

Um diese Landkarten zu berechnen, nutzen die Forscher eine mathematische Technik namens "Sum-of-Squares" (SOS).

Stellen Sie sich vor, Sie wollen beweisen, dass eine Funktion immer positiv ist (also immer "sicher"). Normalerweise ist das sehr schwer zu prüfen. Aber diese Methode verwandelt das Problem in ein Kochrezept.

• Sie nehmen verschiedene Zutaten (Polynome).
• Sie mischen sie so zusammen, dass das Ergebnis immer wie eine Summe von Quadraten aussieht (z. B. $x^2 + y^2$).
• Da ein Quadrat immer positiv ist, wissen Sie sofort: Das ganze Rezept ist sicher!

Das Tolle ist: Diese "Kochrezepte" können Computer sehr schnell lösen, weil sie in eine Form gebracht werden, die für Maschinen sehr einfach zu berechnen ist (wie ein einfaches Puzzle).

Was haben die Forscher damit erreicht?

1. Bessere Sicherheit: Mit ihrer neuen, dynamischen Methode können sie viel genauere Vorhersagen treffen als alte Methoden. Sie können beweisen: "Mit diesem neuen Wegbegleiter erreichen Sie Ihr Ziel zu 99 % sicher."
2. Bessere Steuerung: Nicht nur können sie prüfen, ob ein Weg sicher ist, sie können auch den perfekten Weg selbst erfinden. Das System berechnet automatisch, wie das Lenkrad gedreht werden muss, um das Ziel sicher zu erreichen.
3. Schneller und effizienter: Besonders bei komplexen, hochdimensionalen Systemen (wie einem Flugzeug oder einem Roboterarm) ist ihre Methode viel schneller als die alten, statischen Methoden.

Zusammenfassung in einem Satz

Die Forscher haben eine neue Art von intelligentem, sich ständig anpassenden Sicherheits-Guide entwickelt, der mithilfe von mathematischen "Kochrezepten" berechnet wird, um sicherzustellen, dass unsichere Systeme (wie autonome Autos oder Roboter) trotz Zufall und Unsicherheit immer sicher ihr Ziel erreichen und keine Gefahren berühren.

Warum ist das wichtig?
Weil wir bald überall autonome Systeme haben werden. Damit wir ihnen vertrauen können, brauchen wir Beweise, dass sie nicht einfach so in den See fahren. Diese Methode liefert genau diesen Beweis.

Technische Zusammenfassung

Titel: Zeitvariante Reach-Avoid-Control-Zertifikate für stochastische Systeme

Autoren: Rayan Mazouz, Luca Laurenti, Morteza Lahijanian
Eingereicht bei: IEEE Transactions on Automatic Control

---

1. Problemstellung

Das Paper adressiert die Herausforderung, die Sicherheit und das Zielerreichungsverhalten von diskretzeitigen, kontinuierlich-räumlichen stochastischen Systemen mit nichtlinearen Dynamiken zu garantieren.

• Kontext: Autonome Systeme in sicherheitskritischen Bereichen operieren unter Unsicherheit und stochastischen Störungen.
• Ziel: Die Analyse und Synthese von Reglern, die eine „Reach-Avoid"-Eigenschaft erfüllen. Das System muss mit einer bestimmten Wahrscheinlichkeit $\delta$ eine Zielmenge ($X_r$) erreichen, während es gleichzeitig eine Unsafe-Menge ($X_u$) vermeidet und in einer sicheren Menge ($X_s$) bleibt.
• Herausforderungen:
  • Kontinuierliche Zustands- und Aktionsräume erschweren die Berechnung exakter Wahrscheinlichkeiten.
  • Bestehende Methoden basieren oft auf endlichen Abstraktionen (Diskretisierung), die in hohen Dimensionen rechnerisch untragbar werden, oder auf konvexen Optimierungsansätzen, die zu konservativ sind oder nur für unendliche Horizonte gelten.
  • Die gemeinsame Synthese von Regler und Nachweis (Certificate) ist oft nicht-konvex und schwer zu verifizieren.

2. Methodik

Die Autoren schlagen einen Rahmenwerk vor, das auf Bellmans Optimalitätsprinzip (Dynamische Programmierung) basiert und dieses mit Sum-of-Squares (SOS)-Optimierung verbindet.

A. Reach-Avoid-Zertifikate

Es werden zwei Arten von Zertifikaten eingeführt, die als reellwertige Funktionen definiert sind und hinreichende Bedingungen erfüllen, um eine untere Schranke für die Erfolgswahrscheinlichkeit zu garantieren:

1. Zeitvariante Zertifikate ($R(x, i)$): Die Funktion hängt von der Zeit $i$ ab. Dies ermöglicht eine genauere Approximation der Wertefunktion über den Horizont, führt aber zu mehr Entscheidungsvariablen.
2. Zeitinvariante Zertifikate ($R(x)$): Eine einzige Funktion für den gesamten Horizont. Dies ist rechnerisch effizienter, kann aber konservativer sein.

Beide Ansätze gelten für endliche und unendliche Horizonte. Ein entscheidendes Merkmal ist die Einführung von Schlupfvariablen ($\alpha, \beta$), um die harten Randbedingungen (z. B. dass die Funktion in der Zielmenge 1 und in der Unsafe-Menge 0 sein muss) für kontinuierliche Polynome relaxierbar zu machen. Dies verhindert Infeasibility-Probleme bei der numerischen Optimierung.

B. SOS-Optimierung und Konvexe Formulierung

• Die Autoren beschränken die Zertifikate und Regler auf Polynomfunktionen.
• Die Nicht-Negativitätsbedingungen auf semi-algebraischen Mengen werden durch SOS-Relaxationen (basierend auf Putinar's Positivstellensatz) in Semidefinite Programme (SDP) umgewandelt.
• Dies ermöglicht eine konvexe Formulierung des Problems, die mit Standard-SDP-Lösern effizient gelöst werden kann.

C. Gemeinsame Synthese (Joint Synthesis)

Ein wesentlicher Beitrag ist die Formulierung eines Problems zur gleichzeitigen Synthese des optimalen Feedback-Reglers $\pi$ und des Zertifikats $R$.

• Das nicht-konvexe Min-Max-Problem (Optimierung über Reglerparameter und Worst-Case-Zustände) wird durch eine Dualisierung und SOS-Relaxation in ein konvexes Problem überführt.
• Dies eliminiert die Notwendigkeit, separate Regler- und Verifikationsprobleme zu lösen oder auf nicht-verifizierbare Deep-Learning-Ansätze zurückzugreifen.

3. Hauptbeiträge

1. Einheitliche Formulierung: Ein Rahmenwerk für zeitvariante und zeitinvariante Reach-Avoid-Zertifikate für diskretzeitige, stochastische Systeme mit kontinuierlichen Räumen, anwendbar auf endliche und unendliche Horizonte.
2. Konvexe Optimierung: Eine Methode zur gemeinsamen Synthese von Zertifikat und Regler mittels SOS-Polynomen, die eine garantierte untere Schranke für die Erfolgswahrscheinlichkeit liefert.
3. Theoretische Garantien: Beweis, dass die vorgeschlagenen Bedingungen eine untere Schranke für die Reach-Avoid-Wahrscheinlichkeit liefern, wobei die Schranken durch die Relaxationsparameter kontrolliert werden.
4. Benchmarking: Umfassende Validierung an linearen und nichtlinearen Systemen (1D bis 3D), die die Überlegenheit des Ansatzes gegenüber state-of-the-art Methoden (insbesondere [8] und [19]) zeigt.

4. Ergebnisse und Experimente

Die Autoren evaluierten ihren Ansatz an mehreren Beispielen, darunter 1D/2D lineare Systeme, Kontraktionsabbildungen, ein 3D-Flugzeugmodell und Raumtemperatursysteme.

• Vergleich mit [8] (Zeitinvariant, unendlicher Horizont):

  • Der vorgeschlagene Ansatz liefert signifikant stärkere untere Schranken für die Wahrscheinlichkeit.
  • Beispiel: Bei einem 1D-System erreichte die Methode von [8] bei Polynomgrad 10 nur eine Schranke von 0,17, während der neue Ansatz 0,96 erreichte.
  • Die Methode von [8] scheiterte in mehreren Fällen (z. B. bei komplexeren Startmengen), während der neue Ansatz erfolgreich war.

• Vergleich mit [19] (Zeitinvariant, endlicher Horizont):

  • Die zeitinvariante Formulierung des Papers liefert bei moderaten Polynomgraden deutlich bessere Schranken als [19].
  • Die zeitvariante Formulierung liefert die besten Ergebnisse, oft mit deutlich niedrigeren Polynomgraden, was die Konservativität weiter reduziert.

• Regler-Synthese:

  • Die gemeinsame Synthese von Regler und Zertifikat erhöhte die erreichte Wahrscheinlichkeit drastisch.
  • Beispiel: Bei einem 2D-Kontraktionsmodell mit Rotation stieg die Erfolgswahrscheinlichkeit von ca. 0,19 (ohne Kontrolle) auf ca. 0,95 (mit synthetisiertem Regler).
  • Zeitvariante Zertifikate ermöglichten hohe Wahrscheinlichkeiten (z. B. >0,99) bereits mit sehr niedrigen Polynomgraden (z. B. Grad 2 oder 6), während zeitinvariante Zertifikate oft hohe Grade (z. B. 24) benötigten, um ähnliche Ergebnisse zu erzielen.

• Rechenkomplexität:

  • Zeitvariante Ansätze sind rechenintensiver (Skalierung mit $O((H+1)^3)$), bieten aber in hochdimensionalen Räumen eine bessere Skalierbarkeit als zeitinvariante Ansätze, da sie mit niedrigeren Polynomgraden auskommen.

5. Bedeutung und Fazit

Das Paper stellt einen bedeutenden Fortschritt in der formalen Verifikation und Synthese stochastischer Systeme dar:

• Überwindung der Diskretisierung: Es ermöglicht die Arbeit direkt im kontinuierlichen Raum ohne die „Fluch der Dimensionalität"-Problematik von Gitter-basierten Methoden.
• Vermeidung von Conservatismus: Durch die Einführung von Zeitvariabilität und Relaxationsparametern werden die oft zu konservativen Schranken bestehender Methoden deutlich verbessert.
• Praktische Anwendbarkeit: Die Fähigkeit, Regler und Nachweis gleichzeitig zu synthetisieren, macht den Ansatz für das Design sicherheitskritischer autonomer Systeme (z. B. Robotik, Luftfahrt) äußerst relevant.
• Skalierbarkeit: Die Ergebnisse zeigen, dass zeitvariante Zertifikate eine vielversprechende Strategie sind, um in hochdimensionalen Systemen robuste probabilistische Garantien zu erhalten, ohne auf extrem hohe Polynomgrade angewiesen zu sein.

Zusammenfassend bietet das vorgestellte Framework ein rigoroses, aber rechnerisch handhabbares Werkzeug, um Sicherheits- und Zielerreichungsziele für stochastische Systeme mit kontinuierlichen Zustands- und Aktionsräumen zu zertifizieren und zu steuern.