⚡ electrical engineering

Bernstein-based polynomial approach to study the stability of switched systems and formal verification using HOL Light

Cet article propose une approche préliminaire pour étudier la stabilité des systèmes commutés en les transformant en expressions polynomiales via l'interpolation de Bernstein afin de construire des fonctions de Lyapunov, lesquelles sont ensuite vérifiées formellement à l'aide de l'assistant de preuve HOL Light.

Auteurs originaux : Loïc Michel

Publié 2026-06-04

📖 4 min de lecture☕ Lecture pause café

CC BY 3.0

Auteurs originaux : Loïc Michel

Article original sous licence CC BY 3.0 (http://creativecommons.org/licenses/by/3.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez que vous conduisez une voiture qui possède deux moteurs différents : un Moteur Sport pour la course et un Moteur Éco pour économiser du carburant. Un « système à commutation » est comme une voiture qui bascule instantanément entre ces deux moteurs selon une règle (comme « si la route est escarpée, utiliser le mode Sport ; si elle est plate, utiliser le mode Éco »).

La grande question pour les ingénieurs est la suivante : Est-ce que cette voiture restera sur la route et ne s'écrasera pas, peu importe la fréquence à laquelle elle change de moteur ?

Cet article propose une nouvelle méthode ingénieuse pour répondre à cette question en utilisant les mathématiques, plus précisément une méthode appelée Interpolation de Bernstein. Voici comment l'auteur décompose la démarche :

1. Le Problème : Trop de règles

Habituellement, pour vérifier si la voiture est sûre, vous devez examiner les règles du Moteur Sport et celles du Moteur Éco séparément, puis essayer de deviner ce qui se passe lorsque l'on bascule de l'un à l'autre. C'est comme essayer de prédire la météo en regardant deux modèles de prévisions différents et en essayant de deviner comment ils se mélangent. Cela devient complexe et désordonné.

2. La Solution : Mélanger les moteurs en une seule recette fluide

L'auteur suggère une astuce : au lieu de traiter la « commutation » comme un saut soudain, décrivons-la comme une courbe lisse et continue en utilisant un type spécial de mathématiques appelé polynômes de Bernstein.

Pensez à cela comme à un variateur d'intensité pour une lumière, plutôt qu'à un bouton on/off.

Au lieu de dire « Le Moteur A est ALLUMÉ, le Moteur B est ÉTEINT », les mathématiques créent une formule unique et fluide qui mélange les deux moteurs.
Si l'interrupteur est à 30 % vers le mode Sport et à 70 % vers le mode Éco, la formule crée un « moteur hybride » qui est exactement 30 % Sport et 70 % Éco.
Cela transforme un système complexe et saccadé en une seule équation polynomiale fluide (une recette algébrique sophistiquée).

3. Le Test de Sécurité : Le test « Lyapunov »

Une fois que la voiture est décrite par cette seule recette fluide, l'auteur veut prouver qu'elle est sûre. En ingénierie, il existe un test de sécurité célèbre appelé fonction de Lyapunov.

La Métaphore : Imaginez la voiture comme une balle roulant à l'intérieur d'un bol. Si la balle roule toujours vers le fond (le centre), le système est stable. Si elle roule vers le bord et sort du bol, elle est instable.
La fonction de Lyapunov est comme une carte mathématique qui prouve que la balle doit rouler vers le fond.

4. L'Avocat Informatique « HOL Light »

Voici la partie la plus unique de l'article. Habituellement, les humains vérifient ces cartes de sécurité, et ils peuvent commettre des erreurs.

L'auteur utilise un outil informatique appelé HOL Light.
Considérez HOL Light comme un avocat informatique extrêmement strict. Il ne se contente pas de deviner ; il lit la preuve mathématique étape par étape et vérifie chaque mouvement logique avec une certitude de 100 %.
Si l'avocat informatique dit : « Oui, cette fonction de Lyapunov prouve que la balle reste dans le bol », alors vous savez avec certitude que le système est stable. Il n'y a aucune place pour l'erreur humaine.

Ce que l'article a réellement fait

L'auteur n'a pas inventé une nouvelle voiture ou un nouveau moteur. Il a démontré cette méthode avec deux exemples :

Un Système Stable : Il a montré une voiture qui reste naturellement en sécurité. Sa méthode a réussi à mélanger les moteurs et l'avocat informatique a confirmé la sécurité.
Un Système Instable : Il a montré une voiture qui s'écrase naturellement. Sa méthode a mélangé les moteurs, et l'avocat informatique a correctement identifié que la carte de sécurité échouait (la balle roulerait hors du bol).

L'essentiel à retenir

Cet article est un « travail préliminaire », ce qui signifie qu'il s'agit d'une preuve de concept. L'auteur dit :
« Nous avons trouvé un moyen de transformer un système de commutation complexe en une seule formule mathématique fluide en utilisant les polynômes de Bernstein. Ensuite, nous avons utilisé un avocat informatique (HOL Light) pour prouver formellement si cette formule représente un système sûr ou dangereux. »

Le but est de rendre le processus de vérification de la sécurité de ces systèmes à commutation plus fiable et plus facile à vérifier à l'aide d'ordinateurs.

Résumé technique : Approche polynomiale basée sur les polynômes de Bernstein pour la stabilité des systèmes commutés et la vérification formelle

Énoncé du problème
Les systèmes commutés, composés de plusieurs sous-systèmes régis par un signal de commutation, présentent des défis importants en matière d'analyse de stabilité. Les méthodes traditionnelles peinent souvent à fournir une description mathématique unifiée du comportement complet du système, particulièrement lorsque le signal de commutation est complexe (par exemple, dépendant de l'état ou du temps). Bien que de nombreuses méthodes existent pour analyser ces systèmes, il est nécessaire de disposer d'une formulation capable de transformer la logique de commutation discrète en une expression polynomiale continue, facilitant ainsi la construction de fonctions de Lyapunov et permettant une vérification formelle rigoureuse.

Méthodologie
L'article propose une stratégie pour reformuler les systèmes commutés en utilisant l'interpolation de Bernstein. L'approche centrale comprend les étapes suivantes :

Reformulation polynomiale : Le signal de commutation $\sigma$ , qui dicte l'activation des sous-systèmes $f_i$ , est approximé à l'aide de polynômes de Bernstein. En exprimant le signal de commutation comme une combinaison linéaire de fonctions de base de Bernstein, l'ensemble du système commuté (initialement défini par des équations différentielles par morceaux) est transformé en une expression polynomiale unique et unifiée.
- Le système est initialement décrit comme une combinaison convexe de sous-systèmes : $\dot{x} = \sum f_i(x)\sigma_i$ , où $\sum \sigma_i = 1$ et $\sigma_i \geq 0$ .
- Le signal de commutation $\sigma_i$ est remplacé par son approximation en série de Bernstein $B_{i,m}^\sigma(\sigma(\nu), \nu)$ , résultant en un « système B-commuté » décrit par une seule équation différentielle polynomiale.
Gestion des types de commutation : La méthode prend en compte différents comportements de commutation :
- Commutation dépendante de l'état : Modélisée à l'aide de fonctions de signe (par exemple, $\sigma \equiv \text{sign}(\delta x_1 x_2)$ ), approximée par des polynômes de Bernstein de degré $m$ .
- Commutation dépendante du temps : Modélisée à l'aide de fonctions d'impulsion pour représenter une activation périodique.
- Flexibilité : Le degré $m$ du polynôme de Bernstein peut être ajusté pour affiner l'approximation, ou des règles de composition peuvent être appliquées pour une plus grande précision, bien que cela augmente la complexité des expressions résultantes.
Vérification formelle : Une fois le système représenté comme un polynôme, les auteurs proposent d'utiliser l'assistant de preuve HOL Light pour vérifier formellement les propriétés de stabilité.
- Une fonction de Lyapunov candidate $V(x)$ est identifiée pour le système polynomial.
- La tâche de vérification est réduite à la preuve de l'inégalité $\dot{V}(x) < \epsilon$ (où $\epsilon$ est une petite constante positive) sur un domaine défini $D$ .
- Ceci est réalisé en utilisant l'arithmétique d'intervalles avec approximations de Taylor, une méthode précédemment validée dans le projet Flyspeck. Cela permet de certifier rigoureusement que la dérivée de Lyapunov est négative (ou suffisamment proche de zéro) dans les bornes spécifiées.

Résultats clés
L'article illustre l'approche proposée à travers deux exemples numériques dérivés de la littérature existante, comparant la représentation polynomiale « B-commutée » au système commuté « standard » :

Exemple 1 (Système stable) : Un système commuté linéaire avec deux sous-systèmes stables a été analysé. L'approximation de Bernstein a réussi à imiter le comportement stabilisant du système standard.
Exemple 2 (Système instable) : Un système commuté linéaire avec des sous-systèmes instables a été analysé. La méthode a correctement capturé le comportement divergent, notant que lorsque le produit d'état $x_1 x_2$ croît au-delà de l'intervalle $[0, 1]$ , la série de Bernstein diverge naturellement, reflétant l'instabilité du système.
Vérification formelle : Un système stable linéaire de base a été utilisé pour démontrer le processus de vérification HOL Light. Les auteurs ont généré avec succès un certificat de preuve formelle confirmant que la dérivée d'une fonction de Lyapunov quadratique restait en dessous d'un seuil ( $\epsilon = 0,01$ ) dans l'intervalle $[0, 1]$ .

Signification et revendications
Les auteurs présentent ce travail comme une étude préliminaire avec les contributions et limites spécifiques suivantes :

Unification : La principale contribution est la capacité d'« unifier » plusieurs sous-systèmes commutés en une seule expression polynomiale via l'interpolation de Bernstein. Cela simplifie la recherche de fonctions de Lyapunov candidates.
Certification formelle : L'approche comble le fossé entre la simulation numérique et la preuve formelle, permettant à l'assistant HOL Light de vérifier les propriétés de stabilité des fonctions de Lyapunov dérivées.
Portée modeste : L'article stipule explicitement qu'il suppose que les propriétés de stabilité du système B-commuté sont équivalentes à celles du système commuté standard (du moins concernant la stabilité de Lyapunov), mais ne prétend pas avoir encore prouvé cette équivalence de manière rigoureuse.
Travaux futurs : Les auteurs identifient plusieurs domaines pour des investigations futures, notamment :
- Prouver l'équivalence mathématique complète entre les représentations standard et B-commutées concernant la stabilité.
- Étendre la méthode aux systèmes non linéaires et non polynomiaux.
- Utiliser des outils de Sommes de Carrés (SOS) pour calculer des fonctions de Lyapunov « optimales » plutôt que de simplement vérifier des candidats identifiés.

En conclusion, l'article propose un nouveau cadre qui exploite les polynômes de Bernstein pour convertir l'analyse des systèmes commutés en un problème polynomial, soluble via des outils de vérification formelle, offrant ainsi une voie potentielle vers une certification de stabilité rigoureuse.