STLCG

JAX-Toolkit für differenzierbare Robustheit der Signal Temporal Logic

Lizenz

BSD-2-Clause

Überblick

STLCG (vertrieben als die JAX-Bibliothek stljax) ist ein Toolkit zur Berechnung der Robustheit von Formeln der Signal Temporal Logic (STL) mithilfe von Berechnungsgraphen. STL ist eine formale Sprache zur Beschreibung räumlich-zeitlicher Anforderungen wie "betrete den Zielbereich innerhalb von 10 Sekunden und verweile dort 5 Sekunden", und ihr Robustheitsmaß quantifiziert, wie stark ein Signal eine Spezifikation erfüllt oder verletzt. stljax setzt das ursprüngliche stlcg von 2019 des Stanford ASL (in PyTorch) in JAX neu um und ersetzt die sequenzielle rekurrente Auswertung durch eine vollständig parallelisierbare, maskierungsbasierte Formulierung, die auf der GPU bis zu ~1000x schneller läuft. Da die gesamte Pipeline differenzierbar ist, lassen sich STL-Spezifikationen direkt in gradientenbasierte Trajektorienoptimierung, das Belohnungsdesign im Reinforcement Learning und das Parameter-Mining einbetten. Veröffentlicht in den IEEE Robotics and Automation Letters (RA-L) 2025; per pip installierbar als stljax.

stljax ermöglicht es Robotik-Ingenieuren, menschenlesbare Missionsspezifikationen in temporaler Logik in differenzierbare Zielfunktions- und Nebenbedingungsterme umzuwandeln. Sie erstellen STL-Formeln aus Expressions und Predicates, werten ihre Robustheit über ein Signal oder eine Trajektorie aus und erhalten – da alles in JAX implementiert ist – per vmap eine gebündelte Auswertung sowie exakte Gradienten für den Einsatz in Optimierern und Lernschleifen. Die zentrale Designentscheidung ist eine maskierungsbasierte Neuformulierung der temporalen Operatoren (Always/Eventually/Until), die das parallelisiert, was zuvor eine sequenzielle rekurrente Berechnung war, und so um Größenordnungen schnellere Auswertungen liefert, während die Gradienten zugleich korrekt über alle min/max-Operationen verteilt werden.

Warum es wichtig ist

Die Signal Temporal Logic gibt der Robotik eine präzise, menschenlesbare Möglichkeit, zeitliche und räumliche Missionsanforderungen zu spezifizieren, doch jahrelang war ihre Robustheitsberechnung sequenziell, langsam und schwer zu differenzieren – was STL aus modernen Lern- und Optimierungspipelines fernhielt. stljax beseitigt diese Hürde: Eine parallelisierte, von Haus aus autodiff-fähige Implementierung macht STL schnell genug für Echtzeit-Regelung und Training mit großen Batches, sodass Spezifikationen direkt als Planer-Zielfunktionen, RL-Belohnungen oder Verifikationssignale dienen können.

Welches Problem es löst

Frühere STL-Robustheits-Tools beruhten auf sequenzieller rekurrenter Berechnung, die langsam und schwer zu differenzieren war, was den Einsatz formaler Spezifikationen der temporalen Logik in der gradientenbasierten Trajektorienoptimierung und im Lernen einschränkte.

Wichtigste Punkte

• Maskierungsbasierte parallele STL-Robustheit, auf der GPU bis zu ~1000x schneller als rekurrente Methoden
• JAX-nativ: vmap-Batching und exakte Gradienten, mit korrekter Gradientenverteilung über min/max
• Expression- und Predicate-APIs zum Erstellen von Always/Eventually/Until-Formeln
• Differenzierbare Spezifikationen als Zielfunktionen/Nebenbedingungen in der Trajektorienoptimierung und im RL nutzbar
• Per pip installierbar (stljax); RA-L 2025; Nachfolger des PyTorch-stlcg des Stanford ASL

Für wen

• Forschende in Bewegungsplanung und Trajektorienoptimierung
• Forschende in Regelungstechnik und formalen Methoden
• Designer von Belohnungen im Reinforcement Learning
• Ingenieure für sichere Autonomie und Verifikation

Einschränkungen

• Erfordert Vertrautheit mit der Signal Temporal Logic, um nützliche Spezifikationen zu verfassen
• Die Glättung/Approximation der Robustheitsfunktion bringt Kompromisse bei Genauigkeit/Gradienten mit sich
• Abhängigkeit von JAX und dessen Toolchain
• Eine Bibliothek zur Spezifikationsauswertung – enthält selbst keinen Planer oder Regler