🤖 AI

Uppaal Coshy: Automatic Synthesis of Compact Shields for Hybrid Systems

Cet article présente Uppaal Coshy, un outil automatique qui synthétise des boucliers de sécurité compacts pour les systèmes hybrides en approximant les partitions complexes de l'espace d'états par des simulations et en employant l'algorithme Caap pour représenter efficacement les stratégies résultantes sous forme d'arbres de décision.

Auteurs originaux : Asger Horn Brorholt, Andreas Holck Høeg-Petersen, Peter Gjøl Jensen, Kim Guldstrand Larsen, Marius Mikučionis, Christian Schilling, Andrzej Wąsowski

Publié 2026-08-06

📖 8 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Asger Horn Brorholt, Andreas Holck Høeg-Petersen, Peter Gjøl Jensen, Kim Guldstrand Larsen, Marius Mikučionis, Christian Schilling, Andrzej Wąsowski

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.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 essayez d'apprendre à un robot comment jouer à un jeu, comme garder une balle en l'air ou conduire une voiture à travers une tempête. Vous voulez que le robot soit aussi performant que possible, mais vous devez également vous assurer qu'il ne fasse jamais quelque chose de dangereux, comme s'écraser contre un mur ou laisser la balle tomber. Dans le monde de l'informatique, c'est ce qu'on appelle la « synthèse de bouclier » (shield synthesis). Imaginez un bouclier non pas comme une pièce de métal, mais comme un entraîneur de sécurité strict qui se tient aux côtés du robot. Si le robot tente de faire un mouvement qui pourrait mener au désastre, l'entraîneur intervient et dit : « Non, pas celui-là ! Essaie plutôt ce mouvement sûr. » Cela est crucial pour les systèmes complexes où les règles changent constamment, comme une balle qui rebondit en réaction au vent ou un circuit qui traite de l'électricité. Le défi est que ces systèmes possèdent des possibilités infinies, ce qui rend extrêmement difficile l'écriture d'une liste parfaite de mouvements « sûrs » et « dangereux » pour chaque situation.

C'est là qu'intervient l'article « Uppaal Coshy: Automatic Synthesis of Compact Shields for Hybrid Systems ». Les chercheurs, une équipe du Danemark, ont conçu un nouvel outil appelé Uppaal Coshy qui agit comme un entraîneur de sécurité super intelligent pour ces systèmes délicats et mixtes (que l'on appelle « systèmes hybrides » car ils mélangent des changements continus et fluides, comme la vitesse, avec des sauts numériques soudains, comme l'activation d'un interrupteur). Leur grande idée est de diviser d'abord l'univers entier des situations possibles en une grille géante de petites boîtes. Ils lancent ensuite des milliers de simulations pour déterminer quelles boîtes sont sûres et lesquelles sont dangereuses, créant ainsi une carte massive de mouvements autorisés. Cependant, cette carte peut devenir si énorme qu'il est impossible de la stocker ou de l'utiliser. Pour résoudre cela, ils ont inventé un algorithme ingénieux appelé « Caap » (qui ressemble à un nom de robot amical) qui prend cette carte géante et désordonnée et la comprime en un arbre de décision compact et ordonné — comme transformer un manuel d'instructions de 100 pages en un simple organigramme. Ils ont testé cela sur un modèle de balle rebondissante et ont découvert que leur méthode pouvait réduire les règles de sécurité de milliers de fois sans perdre en sécurité, rendant possible l'installation de ces entraîneurs de sécurité sur de vrais appareils.

L'histoire de la balle rebondissante et de l'entraîneur de sécurité

Plongeons au cœur de l'histoire avec un personnage que nous connaissons tous : une balle rebondissante. Imaginez une balle qui rebondit de haut en bas. Un joueur humain peut la frapper pour la maintenir en mouvement, mais s'il la frappe trop fort ou au mauvais moment, la balle pourrait s'envoler dans le ciel ou cesser de rebondir complètement. L'objectif est de faire rebondir la balle éternellement sans qu'elle ne s'arrête ou ne s'envole.

Dans l'ancien temps, déterminer exactement quand frapper la balle pour rester en sécurité aurait été un cauchemar. La position et la vitesse de la balle changent de manière fluide et continue, ce qui signifie qu'il existe une infinité d'endroits où elle pourrait se trouver à chaque seconde. Les chercheurs ont utilisé un outil appelé Uppaal Coshy pour résoudre ce problème. Ils ont traité le monde de la balle comme un immense damier. Ils ont découpé l'espace où la balle pouvait se trouver en des millions de petites boîtes rectangulaires. Pour chaque boîte, l'outil posait une question simple : « Si la balle est dans cette boîte, quels mouvements sont sûrs ? »

Pour répondre à cela, l'outil ne s'est pas contenté de deviner ; il a joué le jeu encore et encore. Il choisissait un point à l'intérieur d'une boîte, simulait le rebond de la balle et observait où elle atterrissait. Si la balle atterrissait dans une boîte « sûre », ce mouvement était bon. Si elle atterrissait dans une boîte « dangereuse » (comme celle où la balle s'arrête), ce mouvement était interdit. Comme le comportement de la balle peut être un peu aléatoire (peut-être que le sol est bosselé, ou que le coup n'est pas parfait), l'outil a lancé ces simulations de nombreuses fois pour en être sûr. Ils ont même dû gérer le fait que la balle puisse rebondir si haut qu'elle quitte entièrement le « plateau ». L'outil a géré cela en créant une zone spéciale « hors limites » et en décidant si quitter le plateau était sûr ou non en fonction de ce qui se passait lors des simulations.

Le problème de la carte géante

C'est ici que l'histoire rencontre un obstacle. Parce que la grille était très fine (pour être très précise), l'outil s'est retrouvé avec une liste massive de règles. Pour leur exemple de la balle rebondissante, la carte de sécurité initiale comprenait plus de 1,4 million de petites boîtes, chacune ayant sa propre règle sur ce qu'il faut faire. Stocker une liste aussi grande, c'est comme essayer de transporter une bibliothèque dans son sac à dos ; c'est trop lourd pour qu'un vrai robot puisse l'utiliser.

Les chercheurs ont remarqué quelque chose d'intéressant : beaucoup de boîtes situées juste à côté les unes des autres avaient exactement les mêmes règles. Si la balle est dans une boîte où il est sûr de la frapper, la balle dans la boîte juste à côté est probablement sûre à frapper aussi. Ainsi, au lieu de conserver des millions de petites règles, pourquoi ne pas les regrouper ?

Entrée en scène Caap : Le compresseur magique

C'est ici que leur nouvel algorithme, Caap, entre en scène. Voyez Caap comme un éditeur magique qui regarde la carte géante et désordonnée et dit : « Hé, ces 500 boîtes disent toutes "Frapper la balle". Regroupons-les en une seule grande zone. » Il y parvient en cherchant des motifs et en fusionnant les boîtes voisines en de plus grandes régions rectangulaires, tant que les règles restent les mêmes.

Le résultat est un arbre de décision. Imaginez un organigramme : « La balle est-elle haute ? Oui ? Est-elle rapide ? Non ? Alors frappe-la. » Cet arbre est beaucoup plus petit et plus facile à lire que la carte originale d'un million de boîtes. Dans leurs tests, Caap a réussi à réduire les règles de sécurité de la balle rebondissante de 1 430 000 cellules minuscules à seulement 2 972 régions. C'est une réduction énorme ! C'est comme transformer un roman de 1 000 pages en une bande dessinée de 20 pages qui raconte exactement la même histoire.

Est-ce que cela fonctionne vraiment ?

L'équipe n'a pas seulement rendu la carte plus petite ; elle s'est assurée qu'elle fonctionnait toujours. Ils ont testé leur nouveau bouclier compact sur la balle rebondissante. Ils ont lancé 10 000 simulations où la balle était contrôlée par ce nouvel entraîneur de sécurité compressé. Le résultat ? Lors d'aucune de ces 10 000 exécutions, la balle ne s'est jamais arrêtée de rebondir ou ne s'est jamais envolée. La sécurité a été parfaitement préservée, même si les règles étaient désormais assez petites pour tenir sur une carte postale.

Ils ont également montré que cet entraîneur de sécurité pouvait être utilisé pour apprendre au robot à être meilleur. D'abord, ils ont laissé le robot apprendre à frapper la balle efficacement (en utilisant le moins d'énergie possible) pendant que le bouclier montait la garde pour l'empêcher de commettre des erreurs dangereuses. Le robot a appris à maintenir la balle en l'air avec très peu de coups, prouvant que l'on peut avoir à la fois la sécurité et l'efficacité en même temps.

Pourquoi cela importe

Cet article ne concerne pas seulement les balles rebondissantes. Les mêmes mathématiques s'appliquent à des choses du monde réel comme les circuits électriques (appelés convertisseurs boost) qui doivent maintenir une tension stable, ou les réservoirs d'eau qui doivent éviter de déborder. Les chercheurs ont également testé leur outil sur ces modèles et, dans chaque cas, l'algorithme Caap a réussi à réduire les règles de sécurité de façon massive — réduisant parfois des millions de règles à seulement quelques dizaines — tout en maintenant le système en sécurité.

La beauté d'Uppaal Coshy est qu'il est entièrement automatique. Vous n'avez pas besoin d'être un génie des mathématiques pour l'utiliser ; vous décrivez simplement votre système, et l'outil détermine les règles de sécurité, les compresse et vous donne un bouclier compact prêt à l'emploi. C'est un grand pas en avant pour garantir que les robots intelligents et les systèmes automatisés du futur soient non seulement intelligents, mais aussi sûrs, fiables et assez petits pour fonctionner sur les appareils que nous utilisons chaque jour.

Résumé Technique : Uppaal Coshy – Synthèse Automatique de Boucliers Compacts pour les Systèmes Hybrides

1. Énoncé du Problème

L'article traite du défi de la synthèse de stratégies de sécurité (boucliers ou shields) pour les Processus de Décision Markoviens (MDP) sur des espaces d'états continus présentant des dynamiques hybrides complexes. Contrairement aux espaces d'états discrets où la synthèse de boucliers est bien établie, les systèmes hybrides présentent des difficultés algorithmiques, particulièrement en ce qui concerne l'analyse de raggiungibilité pour les dynamiques non linéaires et la gestion des espaces d'états infinis.

Un goulot d'étranglement pratique majeur identifié est la scalabilité et le stockage des boucliers synthétisés. Les approches traditionnelles basées sur le partitionnement stockent les actions autorisées pour chaque cellule individuelle d'une grille, ce qui génère des structures de données massives, inefficaces pour le stockage et le déploiement, notamment sur les dispositifs embarqués. De plus, la détermination des cellules sûres et des transitions dans les systèmes hybrides généraux implique souvent des problèmes de raggiungibilité indécidables.

2. Méthodologie

Les auteurs présentent Uppaal Coshy, un outil entièrement intégré à l'environnement de modélisation Uppaal. La méthodologie combine un algorithme de synthèse basé sur le partitionnement avec des approximations par simulation et une nouvelle technique de compression.

2.1 Synthèse de Bouclier Basée sur le Partitionnement

L'algorithme central abstrait l'espace d'états continu $S \subseteq \mathbb{R}^k$ en un ensemble fini de cellules rectangulaires disjointes à l'aide d'une grille régulière définie par un vecteur de granularité $\gamma$ et un décalage $\omega$ .

Formulation du Jeu de Sécurité : La synthèse est formulée comme un jeu de sécurité à deux joueurs. L'objectif est de calculer l'ensemble maximal de « cellules sûres » ( $C_\phi$ ) à partir desquelles le système peut rester dans une propriété de sécurité $\phi$ indéfiniment.
Approximation via Simulation : Puisque la raggiungibilité exacte est souvent indécidable pour les systèmes hybrides généraux, l'outil utilise une approche basée sur la simulation :
- Cellules Sûres Initiales ( $C^0_\phi$ ) : Au lieu d'un raisonnement symbolique, l'outil échantillonne systématiquement des points au sein de chaque cellule. Une cellule est jugée initialement sûre uniquement si tous les points échantillonnés satisfont la spécification de sécurité.
- Relation de Transition : Pour déterminer si une transition existe entre deux cellules ( $C \xrightarrow{a} C'$ ), l'outil simule les dynamiques du système à partir d'états échantillonnés dans $C$ en utilisant l'action $a$ . Si la simulation atteint un état où le contrôleur doit faire un nouveau choix, la cellule cible correspondante est ajoutée à la relation de transition.
- Stochasticité : Contraৰ aux travaux antérieurs qui nécessitaient une conception manuelle de l'échantillonnage pour les dimensions stochastiques, Uppaal Coshy permet au simulateur d'échantillonner directement à partir de distributions stochastiques, supportant ainsi des distributions générales à support non borné.

2.2 Gestion des Défis Pratiques

Espaces d'États Non Bornés : L'outil gère les systèmes dont les limites d'états ne sont pas immédiatement claires (par exemple, une balle rebondissante) en introduisant une cellule factice « hors limites » ( $C_{out}$ ). Les utilisateurs peuvent configurer si la sortie des limites est sûre, non sûre, ou déterminée via l'échantillonnage.
Omission de Variables : Pour réduire la dimensionnalité, les utilisateurs peuvent omettre des variables (par exemple, des compteurs de coût ou des horloges) du partitionnement de la grille. Ces variables sont fixées à leurs valeurs initiales lors de la synthèse, à condition qu'elles n'influencent pas la logique de sécurité.

2.3 Représentation Compacte : L'Algorithme Caap

Pour répondre à l'inefficacité de stockage des boucliers basés sur des grilles, les auteurs introduisent Caap (Coarsify Axis-Aligned Partitionings).

Objectif : Transformer un bouclier à grain fin basé sur une grille alignée sur les axes en un arbre de décision compact et équivalent.
Mécanisme : L'algorithme fusionne de manière itérative les cellules voisines qui partagent le même ensemble d'actions autorisées en de plus larges « régions » rectangulaires.
Contraintes : Les fusions sont soumises à trois règles d'expansion pour garantir que le partitionnement résultant reste valide :
1. Toutes les cellules de la nouvelle région doivent avoir le même ensemble d'actions.
2. La nouvelle région ne doit pas intercepter d'autres régions existantes dans le nouveau partitionnement.
3. L'expansion ne doit pas couper une région originale en fragments non rectangulaires.
Résultat : Cela produit un arbre de décision où les nœuds internes représentent des prédicats alignés sur les axes ( $s_i < c$ ) et les feuilles représentent des ensembles d'actions autorisées, réduisant considérablement la taille de la représentation.

3. Contributions Clés

Outil Uppaal Coshy : Un outil entièrement automatique pour la synthèse de boucliers dans Uppaal, supportant des formalismes expressifs incluant les automates hybrides stochastiques et les appels de bibliothèques C externes. Il s'intègre à Uppaal Stratego pour permettre l'apprentissage par renforcement sous un bouclier synthétisé.
Algorithme Caap : Un nouvel algorithme pour compresser les boucliers basés sur des grilles en arbres de décision, préservant la fonctionnalité tout en réduisant drastiquement la taille.
Approximation par Simulation : Une stratégie d'implémentation pratique qui contourne les problèmes de raggiungibilité indécidables en utilisant un échantillonnage et une simulation systématiques, supportant le contrôle non périodique et les distributions stochastiques générales.

4. Résultats et Évaluation

Les auteurs ont évalué l'outil sur quatre modèles : une balle rebondissante, un convertisseur boost, une marche aléatoire et un réservoir d'eau.

Synthèse et Réduction : Le Tableau 2 de l'article démontre des réductions significatives de la taille du bouclier. Pour le modèle de la balle rebondissante, le bouclier a été réduit de 1 430 000 cellules à 2 972 régions (un facteur de réduction d'environ 480x) en 53 secondes. Le convertisseur boost est passé de 136 800 à 571 régions.
Vérification de la Sécurité : Tous les boucliers synthétisés ont été évalués statistiquement avec des intervalles de confiance de 99 % sur 10 000 exécutions. Aucune exécution non sûre n'a été observée, confirmant que les boucliers maintenaient les propriétés de sécurité (par exemple, empêcher la balle de s'arrêter ou la tension de dépasser les limites).
Démonstration du Flux de Travail : Le cas d'étude de la balle rebondissante (Section 5.1) illustre un flux de travail complet : la synthèse d'une stratégie de base « efficace » (qui échoue à la sécurité), la génération d'un bouclier, sa compression via Caap, et enfin l'utilisation d'Uppaal Stratego pour apprendre une stratégie quasi-optimale sous le bouclier compact. La stratégie résultante était à la fois sûre et efficace.

5. Signification et Revendications

L'article positionne Uppaal Coshy comme un pont entre la synthèse de boucliers théorique et l'application pratique dans des systèmes hybrides complexes.

Expressivité : L'outil prétend gérer une classe de modèles plus riche que les outils existants (comme Tempest ou Uppaal Tiga), en supportant spécifiquement les systèmes hybrides stochastiques avec un contrôle non périodique et l'intégration de code externe.
Déployabilité : En introduisant l'algorithme Caap, les auteurs affirment résoudre le problème critique de la taille du bouclier, rendant le déploiement des stratégies synthétisées sur des dispositifs embarqués à ressources limitées réalisable.
Intégration : L'intégration transparente avec Uppaal Stratego permet un flux de travail où la sécurité est garantie par le bouclier, tandis que la performance est optimisée via l'apprentissage par renforcement, une capacité que les auteurs soulignent comme un avantage distinct par rapport aux travaux antérieurs.

Les auteurs restent modestes quant à la nature approximative de leur approche, notant que l'approche par sous-approximation par simulation repose sur le nombre d'échantillons ( $n$ ) et les exécutions de ré-échantillonnage ( $m$ ) pour approcher la solution réelle, et que l'algorithme Caap est actuellement un outil autonome qu'ils proposent d'intégrer directement dans l'interface utilisateur d'Uppaal dans des travaux futurs.