Data-Driven Reachability of Nonlinear Lipschitz Systems via Koopman Operator Embeddings

1. Problématique

La vérification de la sécurité des systèmes robotiques dans des environnements dynamiques et incertains repose souvent sur l'analyse de la faisabilité (reachability).

• Limites des méthodes existantes : Les approches basées sur des modèles formels nécessitent des dynamiques de système précises, ce qui est difficile à obtenir pour des plateformes complexes. Les méthodes data-driven (basées sur les données) utilisant des représentations zonotopiques existent, mais elles deviennent souvent trop conservatrices (surestimation excessive de l'incertitude) sur de longues horizons de prédiction, en particulier pour les systèmes non linéaires et en présence de bruit de mesure.
• Objectif : Développer un cadre d'analyse de faisabilité data-driven pour des systèmes non linéaires (non affines) et lipschitziens, capable de fournir des sur-approximations garanties et moins conservatrices que les méthodes linéaires classiques, tout en gérant le bruit et l'incertitude de modélisation.

2. Méthodologie

L'approche proposée combine la théorie de l'opérateur de Koopman avec des représentations zonotopiques pour propager les ensembles de faisabilité.

A. Linéarisation par Opérateur de Koopman

Au lieu d'approximer directement la dynamique non linéaire par un modèle linéaire temps-invariant (LTI), la méthode "élève" (lifts) le système dans un espace de dimension supérieure (espace des observables) où la dynamique est approximativement linéaire.

• Fonctions de relèvement (Lifting) : Le système est transformé via des fonctions $\psi(x, u)$ qui dépendent à la fois de l'état $x$ et de l'entrée $u$. Cela permet de capturer des dynamiques non affines complexes.
• Identification : L'opérateur de Koopman est identifié directement à partir de données bruitées (trajectoires état-entrée) via une régression des moindres carrés (Least Squares), évitant ainsi le besoin d'un modèle physique explicite.

B. Gestion des Erreurs et Incertitudes

Pour garantir formellement que l'ensemble calculé contient la vraie trajectoire, l'article modélise rigoureusement plusieurs sources d'erreur sous forme d'ensembles zonotopiques :

1. Erreur de linéarisation locale : L'erreur introduite par l'approximation linéaire de la dynamique élevée est bornée via un développement de Taylor et majorée par un zonotope $\bar{L}_k$.
2. Erreur de modélisation de Koopman (Résidu) : L'écart entre la prédiction du modèle linéaire élevé et les données réelles est calculé sur l'ensemble des trajectoires disponibles. Ces résidus sont agrégés pour former un ensemble d'erreur $\mathcal{L}_k$.
3. Bruit de processus : Le bruit $w_k$ est borné par un zonotope connu et propagé dans l'espace élevé.
4. Couverture des données (Covering Radius) : Une hypothèse de Lipschitz est utilisée pour étendre les bornes d'erreur calculées sur les points de données discrets à l'ensemble continu de l'espace d'état, en utilisant un rayon de couverture $\delta$.

C. Algorithme de Propagation

1. Propagation dans l'espace élevé : Les ensembles faisables (zonotopes) sont propagés à travers la dynamique linéaire élevée identifiée.
2. Projection : Les ensembles sont projetés de l'espace élevé vers l'espace d'état original.
3. Combinaison : Une somme de Minkowski est effectuée avec les ensembles d'erreur (résidu, bruit, couverture) pour obtenir la sur-approximation finale garantie de l'ensemble faisable du système non linéaire original.

3. Contributions Clés

• Cadre Data-Driven pour systèmes non affines : Introduction d'une méthode capable de traiter des systèmes non linéaires non affines avec du bruit de processus, directement à partir de données mesurées.
• Relèvement État-Entrée Dépendant : Développement d'une identification basée sur des observables dépendant de l'état et de l'entrée, offrant une précision supérieure par rapport aux modèles LTI élevés standards.
• Garanties Formelles : Preuve théorique que les ensembles faisables calculés sur-approximent strictement les ensembles faisables exacts, en intégrant explicitement les erreurs d'apprentissage, le bruit et les erreurs de linéarisation.
• Efficacité et Précision : Utilisation de zonotopes pour une propagation scalable et computationnellement efficace, réduisant significativement le conservatisme sur les longs horizons.

4. Résultats et Évaluation

Les auteurs ont validé leur approche sur trois cas d'usage :

1. Système dynamique affine (Réacteur CSTR) : Comparaison avec CORA (méthode basée sur modèle) et une méthode data-driven par moindres carrés (LS). La méthode proposée montre une réduction significative du conservatisme sur de longs horizons.
2. Système dynamique non affine : Sur un système non linéaire complexe, la méthode proposée fournit des ensembles faisables beaucoup plus serrés que les approches LS classiques et les méthodes basées sur modèle.
3. Véhicule Autonome (JetRacer) : Expérience réelle sur un robot de course autonome. Les résultats expérimentaux confirment que la méthode Koopman proposée génère des sur-approximations nettement plus précises que la méthode LS, permettant une vérification de sécurité plus fiable sur de longues distances.

5. Signification et Impact

Ce travail comble un vide important entre l'identification de systèmes data-driven et la vérification formelle de sécurité.

• Avantage principal : Il permet d'utiliser des modèles appris à partir de données pour la sécurité formelle sans sacrifier la garantie de sécurité (contrairement aux méthodes probabilistes) ni subir un conservatisme excessif (contrairement aux méthodes linéaires simples).
• Applicabilité : La méthode est particulièrement pertinente pour les systèmes robotiques complexes opérant dans des environnements réels où les modèles physiques exacts sont inconnus ou trop coûteux à obtenir, mais où des données de trajectoire sont disponibles.
• Futur : L'approche ouvre la voie à l'application de ces techniques sur des systèmes non linéaires variant dans le temps.

En résumé, l'article propose une solution robuste pour la vérification de sécurité des robots non linéaires, transformant des données bruitées en garanties de sécurité formelles et précises grâce à une ingénierie intelligente de l'espace d'état via l'opérateur de Koopman.