On transferring safety certificates across dynamical systems

1. Problématique

L'assurance de la sécurité des systèmes autonomes (robotique, aérospatial) repose souvent sur des Fonctions de Barrière de Contrôle (CBF). Ces fonctions permettent de garantir formellement que le système reste dans un ensemble sûr (évitement de collisions, respect des contraintes).

Cependant, une lacune majeure existe entre la théorie et la pratique :

• Complexité des modèles réels : Les systèmes physiques réels (ex: drones quadrotors) ont des dynamiques non linéaires, complexes et de haute dimension, rendant la synthèse directe de CBFs difficile, voire impossible en temps réel.
• Modèles abstraits : Les spécifications de sécurité sont souvent conçues et vérifiées sur des modèles simplifiés (ex: double intégrateur) qui sont plus faciles à analyser.
• Le défi du transfert : Déployer une garantie de sécurité conçue sur un modèle abstrait ($\Sigma_1$) sur un système concret ($\Sigma_2$) avec des dynamiques différentes pose un problème critique. Les erreurs de modélisation et les dynamiques non capturées peuvent invalider les certificats de sécurité, conduisant potentiellement à des collisions.

L'objectif de cet article est de combler ce fossé en développant un cadre formel pour transférer les certificats de sécurité d'un système abstrait vers un système concret, même en présence de dynamiques non correspondantes.

2. Méthodologie : Le cadre tCBF (Transferred Control Barrier Function)

Les auteurs proposent une méthode basée sur les relations de simulation et l'introduction d'une marge explicite pour compenser les erreurs de modélisation.

A. Concepts Fondamentaux

• Systèmes :
  • $\Sigma_1$ : Système abstrait (modèle simplifié, ex: double intégrateur).
  • $\Sigma_2$ : Système concret (modèle physique complet, ex: quadrotor non linéaire).
• Fonction de Simulation ($V$) : Une fonction qui mesure la "distance" ou l'écart entre l'état du système concret et son représentant le plus proche dans l'espace abstrait. Elle garantit que si $V$ est petit, les sorties des deux systèmes sont proches.
• Carte Témoin (Witness Map, $\Pi$) : Pour un état concret $x_2$, $\Pi(x_2)$ est l'état abstrait qui minimise la fonction de simulation $V$. Cela permet de projeter l'état réel sur le modèle abstrait.

B. Construction de la tCBF

Au lieu d'appliquer directement la barrière abstraite $b_1$ sur le système concret, les auteurs définissent une Fonction de Barrière Transférée ($b_2$) :

$$b_2(x_2) := b_1(\Pi(x_2)) - \phi(V(\Pi(x_2), x_2))$$

Où :

• $b_1(\Pi(x_2))$ est la valeur de la barrière de sécurité sur le modèle abstrait.
• $\phi$ est une fonction de marge (de classe $\mathcal{K}_\infty$) qui dépend de l'erreur de simulation $V$.
• Intuition : La marge $\phi$ "rétrécit" l'ensemble sûr abstrait pour tenir compte de l'incertitude et de l'écart dynamique. Tant que $b_2(x_2) \ge 0$, la sécurité est garantie sur le système concret.

C. Conditions de Validité et Synthèse

Pour garantir que $b_2$ est une CBF valide pour $\Sigma_2$, les auteurs dérivent une condition sur la dérivée temporelle de $b_2$. Ils montrent que la dérivée dépend de :

1. La dynamique de la barrière abstraite.
2. La décroissance de la fonction de simulation (garantie par la relation de simulation).
3. Un terme de "mismatch" (écart dynamique) dû à la différence entre les trajectoires réelles et projetées.

Condition clé (Hypothèse 2) : La fonction de marge $\phi$ doit croître suffisamment vite pour compenser la croissance potentielle de la barrière abstraite et les erreurs de dynamique. Cela se traduit par une inégalité différentielle scalaire :
$$\phi'(s)\alpha_V(s) \ge \alpha_b(\phi(s)) + r(s)$$
Où $\alpha_V$ et $\alpha_b$ sont des fonctions de décroissance et de croissance respectives, et $r$ borne l'erreur de mismatch.

Les auteurs fournissent des solutions analytiques (forme close) pour $\phi$ dans des cas courants (fonctions linéaires), évitant ainsi des optimisations numériques lourdes.

D. Implémentation en Temps Réel (tCBF-QP)

Le filtre de sécurité est implémenté via un Programme Quadratique (QP) :

• Objectif : Minimiser l'écart entre la commande de contrôle nominale ($u_{nom}$) et la commande de sécurité ($u^*$), assurant ainsi une intervention minimale.
• Contrainte : La dérivée de la tCBF doit satisfaire la condition de sécurité ($\dot{b}_2 \ge -\alpha(b_2)$).
• Grâce à la structure affine des dynamiques de contrôle, cette contrainte reste linéaire par rapport à l'entrée de commande, rendant le QP très rapide à résoudre.

3. Contributions Clés

1. Construction Formelle de tCBF : Une formulation rigoureuse permettant de transférer des certificats de sécurité d'un modèle abstrait à un modèle concret via une fonction de simulation et une marge explicite.
2. Garanties Théoriques : Preuve que si la fonction de marge est correctement conçue (satisfaisant l'inégalité différentielle), la sécurité est garantie sur le système concret, même avec des dynamiques non linéaires et des dimensions d'état différentes.
3. Guides de Conception Pratiques : Fourniture de conditions explicites et de solutions analytiques pour la fonction de marge $\phi$, rendant la méthode applicable sans optimisation complexe en ligne.
4. Découplage Sécurité/Synthèse : La méthode permet de concevoir la sécurité sur un modèle simple (off-line) et de l'appliquer sur un système complexe (on-line), ce qui est crucial pour les systèmes embarqués aux ressources limitées.

4. Résultats Expérimentaux

L'approche a été validée sur une tâche de navigation d'un quadrotor dans un environnement 3D encombré d'obstacles.

• Configuration :
  • Modèle abstrait ($\Sigma_1$) : Double intégrateur 3D.
  • Modèle concret ($\Sigma_2$) : Quadrotor rigide complet (dynamique non linéaire, sous-actionné, 12 états).
  • Obstacles : Sphères statiques.
• Scénario : Le quadrotor doit aller d'un point A à un point B en évitant les obstacles.
• Observations :
  • Efficacité du filtre : La trajectoire nominale (sans sécurité) entrait en collision avec les obstacles. Le filtre tCBF-QP a modifié la trajectoire localement uniquement près des obstacles pour éviter les collisions.
  • Minimale Invasivité : Loin des obstacles, la trajectoire suivait fidèlement la commande nominale, préservant les performances de suivi.
  • Validation de la Sécurité : Les barrières transférées ont activé précisément lorsque le quadrotor s'approchait des obstacles. La distance géométrique réelle par rapport aux obstacles est restée strictement positive, confirmant l'évitement de collision malgré le mismatch de modèle.
  • Rôle de la Marge : Les résultats montrent que la marge $\phi$ compense efficacement l'écart entre le modèle double intégrateur et la dynamique réelle du quadrotor.

5. Signification et Perspectives

Signification :
Ce travail résout un problème fondamental en robotique autonome : comment utiliser des modèles simplifiés pour garantir la sécurité de systèmes complexes sans devoir redessiner des contrôleurs de sécurité coûteux en calcul pour chaque plateforme. Le cadre tCBF offre une méthode générique, mathématiquement prouvée, pour "hériter" de la sécurité d'un modèle abstrait.

Perspectives Futures :

• Apprentissage des Composantes : La construction manuelle de fonctions de simulation et d'interfaces de contrôle peut être difficile pour des systèmes très complexes. Les auteurs suggèrent d'utiliser l'apprentissage automatique (Machine Learning) pour apprendre ces fonctions à partir de données, élargissant ainsi l'applicabilité de la méthode à des systèmes où les modèles analytiques précis sont inaccessibles.
• Extension à d'autres relations : Généralisation à d'autres types de relations entre systèmes au-delà des simulations classiques.

En résumé, cet article propose un pont théorique et pratique robuste entre la vérification formelle sur des modèles simples et le contrôle sûr sur des systèmes physiques complexes, ouvrant la voie à une autonomie plus fiable et plus rapide à déployer.