Preuves assistées par ordinateur pour l’atteignabilité en théorie du contrôle linéaire avec contraintes
Petit séjour d’étude organisé par Camille Pouchol, du 11 au 16 mars 2023.
Participants
Ivan HASENOHR (Université 1 Paris Cité, France), Camille POUCHOL (Université Paris Cité, France), Yannick PRIVAT (MSHS Poitiers – Université de Poitiers, France), Christophe ZHANG (INRIA Nancy, France)
Résumé

Notre méthode repose sur une idée géométrique simple : pour montrer qu’un point (ici en rouge) ne peut être atteint par le système contrôlé, il suffit de trouver un hyperplan (ici en rouge pâle) qui le sépare de l’ensemble de tous les points atteignables (ici en bleu).
Notre séjour du 11 au 16 mars 2024 a été consacré à la rédaction et à la finalisation d’un article de mathématiques sur les preuves assistées par ordinateur appliquées à la contrôlabilité et à l’atteignabilité des systèmes. Ce travail a réuni les mathématiciens Ivan Hasenohr, Camille Pouchol, Yannick Privat, et Christophe Zhang (3/4 de participants juniors), dans le cadre de la thèse d’Ivan Hasenohr sur la contrôlabilité sous contraintes géométriques et topologiques. L’article explore comment certifier que certains états indésirables ne peuvent être atteints par un système linéaire contrôlé. Nous avons développé des méthodes numériques robustes pour la certification de la non-atteignabilité, en tenant compte des erreurs et des contraintes pratiques. Cette recherche, désormais en prépublication, a été rendue possible grâce à l’environnement de travail exceptionnel offert par la Fondation des Treilles.
Summary
Our stay from March 11 to 16, 2024, was dedicated to writing and finalising a mathematics article on computer-assisted proofs applied to the controllability and attainability of systems. This work brought together mathematicians Ivan Hasenohr, Camille Pouchol, Yannick Privat, and Christophe Zhang (3 out of 4 are “junior participants”), within the framework of Ivan Hasenohr’s thesis on controllability under geometric and topological constraints. The article explores how to certify that given unwanted states will not be reached by a controlled linear system. We developed robust numerical methods for certifying non-attainability, taking into account errors and practical constraints. This research, now in preprint, was made possible thanks to the exceptional working environment provided by the Fondation des Treilles.
Compte rendu
Notre séjour s’est déroulé du 11/03/2024 au 16/03/2024. Il a été consacré à l’écriture et la finalisation d’un article de mathématiques désormais en prépublication [1], sur la notion de preuves assistées par ordinateur appliquées à la notion de contrôle et d’atteignabilité.
Ce séjour, réunissant Ivan Hasenohr, Camille Pouchol, Yannick Privat et Christophe Zhang, a été organisé dans le contexte de la thèse d’Ivan Hasenohr, débutée le 1er octobre 2022 au sein du laboratoire MAP5 de l’Université Paris Cité. Sa thèse, intitulée Contrôlabilité sous contraintes géométriques et topologiques est encadrée par Yannick Privat de l’Université de Lorraine, Christophe Zhang de l’INRIA Grand Est, et Camille Pouchol de l’Université Paris Cité.
La théorie mathématique du contrôle et de l’atteignabilité porte sur l’étude de modèles physiques ou biologiques, sur lesquels on agit pour atteindre – ou au contraire éviter – certaines cibles. Elle examine la possibilité de guider un système depuis une configuration initiale vers une configuration finale souhaitée à l’aide de contrôles, i.e. des actions sur le système par un utilisateur extérieur. On peut par exemple considérer des barrages routiers comme des contrôles visant à libérer un axe pour permettre à des secours de l’emprunter. L’objectif est alors l’évacuation d’un axe routier en un temps donné.
Afin de traduire convenablement les contingences pratiques permettant de réaliser une telle opération, on doit considérer des contraintes sur ces contrôles. Il est possible qu’on ne puisse pas atteindre certaines positions ou configurations en raison de telles contraintes. Une autre conséquence des contraintes est l’émergence de temps minimaux pour atteindre l’objectif visé. On parle alors d’obstructions à la contrôlabilité. À l’inverse, il se peut que l’on veuille à tout prix éviter certaines cibles indésirables.
Dans l’article rédigé au cours de cette semaine, nous nous sommes concentrés sur ce phénomène : nous avons cherché à déterminer si un contrôle (satisfaisant les contraintes physiques du problème) peut conduire le système vers une configuration indésirable. L’approche implique la résolution d’un problème dit de “contrôle optimal”, qui est en général complexe à analyser, car non-linéaire. Nous nous nous sommes concentrés sur la propagation d’erreurs et avons proposé des méthodes robustes de certification puis d’implémentation numérique.
Il existe des applications pratiques dans de nombreux domaines, de la navigation des véhicules autonomes à la régulation des processus industriels, en passant par la modélisation des phénomènes naturels.
Détails du projet de recherche et de l’article : contrôlabilité et obstructions
Notre objectif principal était d’explorer la question de la contrôlabilité dans ce contexte où des contraintes doivent être prises en compte. Plus précisément, il s’agissait de déterminer s’il existe un contrôle conduisant la solution d’un système (physique, biologique ou technologique) vers une zone indésirable en un temps donné.
Dans notre recherche, nous avons pris en considération des contraintes sur la commande traduisant des réalités physiques. Cette situation diffère des problèmes de contrôlabilité classiques pour les systèmes linéaires, où de telles contraintes ne sont généralement pas présentes.
Bien évidemment, dans la plupart des applications visées, il est absolument essentiel de connaître ces informations et d’être capable de les obtenir rapidement, à l’aide d’un ordinateur. Cela justifie le développement d’algorithmes efficaces adaptés à ces problèmes.
Pour les applications qui ne peuvent souffrir de telles incertitudes, il s’agit d’une restriction importante. Pour y remédier, nous proposons une méthode à l’aide de preuves assistées par ordinateur. Il s’agit dans ce cadre de contrôler les erreurs d’arrondi commises à chaque étape, grâce à l’arithmétique d’intervalles via le logiciel Intlab [3]. Celle-ci permet in fine de garantir de manière rigoureuse qu’un état donné est atteignable, ou ne l’est pas : on parle alors de certification.
Nous avons adopté une approche basée sur l’analyse convexe, inspirée de [2] qui s’appuie notamment sur le théorème de Fenchel-Rockafellar. Le coeur de notre méthode repose sur la formulation d’un problème de “contrôle optimal” où nous minimisons une fonction de coût sous contraintes. Cette approche nous a conduits à développer des méthodes numériques robustes pour certifier que les zones indésirables ne peuvent être atteintes par le système. Elles nécessitent l’utilisation d’algorithmes d’optimisation adaptés, notamment pour les cas où les coûts ne sont pas nécessairement différentiables.
Les résultats théoriques et numériques, obtenus en dimension finie, sont concluants jusqu’à des dimensions de l’ordre de 50.
Conclusion
Ce séjour nous a ainsi permis de complètement finaliser la rédaction de l’article Computer-assisted proof of non-reachability for linear systems in finite dimension, Ivan Hasenohr, Camille Pouchol, Yannick Privat and Christophe Zhang. Prépublication HAL (2024). Nous remercions chaleureusement la fondation des Treilles pour le cadre exceptionnel qu’elle nous a fourni, ainsi que l’accueil très chaleureux du personnel sur place.
Références
[1] Ivan Hasenohr, Camille Pouchol, Yannick Privat, and Christophe Zhang. Computer-assisted
proofs of non-reachability for linear finite-dimensional control systems. hal-04523794.
[2] Camille Pouchol, Emmanuel Trélat, and Christophe Zhang. Approximate control of parabolic
equations with on-off shape controls by Fenchel duality. Annales de l’Institut Henri Poincaré
C, pages 1–43, 2024.
[3] S.M. Rump. INTLAB – INTerval LABoratory. In Tibor Csendes, editor, Developments in Re-
liable Computing, pages 77–104. Kluwer Academic Publishers, Dordrecht, 1999.
OpenEdition vous propose de citer ce billet de la manière suivante :
ldiebold (13 juin 2024). Preuves assistées par ordinateur pour l’atteignabilité en théorie du contrôle linéaire avec contraintes. Les carnets de la Fondation des Treilles. Consulté le 19 mars 2025 à l’adresse https://doi.org/10.58079/11ti7