On transferring safety certificates across dynamical systems

Titel: Over het overdragen van veiligheidscertificaten tussen dynamische systemen

Auteurs: Nikolaos Bousias, Charalampia Stamouli, Anastasios Tsiamis, en George Pappas.

1. Probleemstelling

In de autonome systemen (robotica, luchtvaart, industriële automatisatie) is het garanderen van veiligheid een fundamentele uitdaging. Control Barrier Functions (CBF's) zijn een krachtig wiskundig kader om veiligheidsbeperkingen in real-time te handhaven door veilige gebieden als voorwaarts-invariante verzamelingen te coderen.

Het centrale probleem dat dit paper adresseert, is de kloof tussen abstracte modellen en fysieke systemen:

• Veiligheidsspecificaties worden vaak het meest natuurlijk ontworpen en geverifieerd op vereenvoudigde, tractabele modellen (bijv. enkel- of dubbelintegratoren).
• Het toepassen van deze certificaten op complexe, fysieke systemen (met niet-lineaire dynamica, onderactuatie en geometrische beperkingen) is echter problematisch.
• Bestaande methoden vereisen vaak het direct ontwerpen van barrièrefuncties op het volledige, hoge-dimensionale niet-lineaire systeem, wat computationeel duur is of veel domeinkennis vereist.
• Er is behoefte aan een methode om veiligheidsbewijzen van een "abstract" model (Σ1) over te dragen naar een "concreet" model (Σ2) met mismatchende dynamica, zonder het ontwerp van de barrière volledig opnieuw te hoeven doen.

2. Methodologie: Het tCBF-kader

De auteurs stellen een Transferred Control Barrier Function (tCBF) framework voor. Dit kader maakt het mogelijk om veiligheidsbeperkingen gedefinieerd op één systeem systematisch af te dwingen op een ander systeem.

Kerncomponenten:

1. Simulatiefunctie ($V$): Een functie die de afstand (mismatch) tussen de toestanden van het abstracte systeem ($x_1$) en het concrete systeem ($x_2$) kwantificeert. Deze functie moet voldoen aan een vervalvoorwaarde (decay inequality) die garandeert dat de fout tussen de systemen niet onbeperkt groeit.
2. Interface ($F$): Een regeling die de input van het concrete systeem ($u_2$) omzet naar een equivalente input voor het abstracte systeem ($u_1$).
3. Getuige-kaart (Witness Map, $\Pi$): Een afbeelding die voor elke concrete staat $x_2$ de "dichtstbijzijnde" abstracte staat $x_1$ bepaalt (via minimalisatie van $V$).
4. De tCBF Constructie:
   De overgedragen barrière $b_2$ voor het concrete systeem wordt gedefinieerd als:
   $$b_2(x_2) := b_1(\Pi(x_2)) - \phi(V(\Pi(x_2), x_2))$$
   Waarbij:
   • $b_1$ de originele CBF is voor het abstracte systeem.
   • $\phi$ een margefunctie is (een klasse-$\mathcal{K}_\infty$ functie) die de grootte van de veiligheidsmarge bepaalt op basis van de simulatiefout $V$.

Wiskundige Garantie:
De auteurs bewijzen dat door de margefunctie $\phi$ correct te kiezen (zodat deze snel genoeg groeit om de vervalrate van de simulatiefunctie en de dynamische mismatch te compenseren), de afgeleide van $b_2$ voldoet aan de standaard CBF-voorwaarde. Hierdoor blijft de veilige verzameling $S_2 = \{x_2 | b_2(x_2) \geq 0\}$ voorwaarts-invariant, zelfs als de systemen verschillende staten en dynamica hebben.

Implementatie (tCBF-QP):
De methode wordt geïmplementeerd als een veiligheidsfilter op basis van een Kwadratisch Programma (QP). Dit filter minimaliseert de afwijking van een nominale controller ($u_{nom}$) terwijl het de CBF-beperking voor het concrete systeem respecteert:
$$\min_{u_2} \|u_2 - u_{nom}\|^2 \quad \text{onder de voorwaarde} \quad \dot{b}_2 + \alpha(b_2) \geq 0$$

3. Belangrijkste Bijdragen

1. Formeel Kader voor Overdracht: Een nieuwe formulering (tCBF) die veiligheidscertificaten van abstracte modellen overdraagt naar complexe niet-lineaire systemen, gebruikmakend van simulatiefuncties en een expliciete marge.
2. Formele Garanties en Ontwerprichtlijnen: Bewijzen dat de overgedragen certificaten geldig zijn onder specifieke voorwaarden voor de margefunctie. De auteurs bieden expliciete voorwaarden en gesloten-oplossingen (via differentiaalvergelijkingen) voor het selecteren van $\phi$, waardoor uitgebreide numerieke optimalisatie overbodig wordt.
3. Generaliteit: De methode vereist niet dat de systemen dezelfde staten-dimensie of dynamica delen.
4. Praktische Validatie: Toepassing op een quadcopter in een complex 3D-omgeving, waarbij veiligheid wordt overgedragen van een eenvoudige dubbelintegrator naar volledige niet-lineaire quadcopter-dynamica.

4. Experimentele Resultaten

Het framework werd getest op een quadcopter die moest navigeren door een omgeving vol met obstakels.

• Opzet: Een abstract model (dubbelintegrator) werd gebruikt om een veilige baan te plannen. Een nominale controller (gebaseerd op SE(3)-geometrische tracking) probeerde deze baan te volgen, maar zou zonder veiligheidsfilter in botsing komen met obstakels.
• Resultaat:
  • De tCBF-QP fungeerde als een minimaal invasief filter. Het paste de besturing alleen aan wanneer het systeem dicht bij de veilige grens kwam.
  • De overgedragen barrière werd actief (nabij nul) wanneer de quadcopter obstakels benaderde, wat leidde tot lokale afwijkingen van de nominale baan om botsingen te voorkomen.
  • De werkelijke geometrische afstand tot obstakels bleef strikt positief, wat aantoont dat botsingsvrijheid werd gegarandeerd voor het volledige niet-lineaire systeem, ondanks de modelmismatch.
  • De methode bleek niet te conservatief; de quadcopter kon nauwe ruimtes tussen obstakels passeren binnen de overgedragen veiligheidsomhulling.

5. Betekenis en Toekomstperspectief

Betekenis:
Dit werk sluit een kritieke kloof in de compositional safety verification. Het stelt ingenieurs in staat om complexe veiligheidsontwerpen offline uit te voeren op vereenvoudigde, tractabele modellen, en vervolgens met wiskundige zekerheid te garanderen dat deze veiligheid behouden blijft bij implementatie op complexe fysieke platforms. Dit is vooral waardevol voor systemen met beperkte rekenkracht tijdens de operatie, waar complexe online berekeningen niet haalbaar zijn.

Toekomstig Werk:
Een uitdaging blijft het analytisch afleiden van geschikte simulatiefuncties en interfaces voor zeer complexe systemen. De auteurs suggereren dat het leren van deze componenten uit data (machine learning) een belangrijke richting is om de toepasbaarheid van tCBF's verder te vergroten, vooral wanneer nauwkeurige analytische modellen ontbreken.

Conclusie:
Het paper introduceert een robuust mechanisme om veiligheid over heterogene dynamische systemen te transfereren, bewezen door zowel theoretische garanties als succesvolle experimenten met een quadcopter.