Présentation
En anglaisRÉSUMÉ
Cet article traite de la synthèse de contrôleurs pour des systèmes non linéaires soumis à des contraintes sur les états et la commande et à des perturbations bornées, et pour des spécifications telles que la sûreté, l’atteignabilité ou des propriétés plus complexes formulées à l’aide d’automates ou de logiques temporelles. Dans ce contexte, les approches symboliques, qui reposent sur l’abstraction du système par un modèle symbolique (avec un nombre fini d’états et de commandes), permettent la synthèse automatique de contrôleurs certifiés « corrects par construction ». Cet article expose de manière didactique les éléments clés de ces approches (abstraction, synthèse et concrétisation des contrôleurs) et présente une synthèse des thématiques avancées de ce domaine de recherche dynamique.
Lire cet article issu d'une ressource documentaire complète, actualisée et validée par des comités scientifiques.
Lire l’articleABSTRACT
This article deals with controller synthesis for nonlinear systems subject to constraints on states and control, as well as bounded disturbances, and for specifications such as safety, reachability, or more complex properties formulated using automata or temporal logics. In this context, symbolic approaches, based on the abstraction of the system through a symbolic model (with a finite number of states and controls), enable the automatic synthesis of controllers certified as “correct by construction.” This article presents in a didactic manner the key elements of these approaches (abstraction, synthesis, and concretization of controllers) and provides an overview of advanced themes in this dynamically evolving research field.
Auteur(s)
-
Antoine GIRARD : Directeur de recherche CNRS - Université Paris-Saclay, CNRS, CentraleSupélec, Laboratoire des signaux et systèmes, 91190, Gif-sur-Yvette, France
-
Pierre-Jean MEYER : Chargé de recherche du développement durable - Univ Gustave Eiffel, COSYS-ESTAS, F-59666 Villeneuve d’Ascq, France
-
Adnane SAOUD : Professeur Assistant - College of Computing, Mohammed VI Polytechnic University (UM6P), Benguerir, Maroc
INTRODUCTION
Dans le domaine de l’automatique, l’utilisation de modèles mathématiques les plus fidèles possibles (non linéaires, avec contraintes sur les états et commandes, avec perturbations, etc.) permet généralement d’augmenter la fiabilité et la confiance en les résultats obtenus suite à l’analyse de ces modèles. Malheureusement, cette complexité des modèles rend l’étape de synthèse de contrôleurs d’autant plus difficile, voire parfois impossible. D’autre part, bien qu’il existe une importante bibliographie considérant des objectifs de contrôle classiques de l’automatique continue tels que la stabilité, ces méthodes ne sont pas les plus adaptées pour traiter d’autres types de spécifications telles que la sûreté, l’atteignabilité, ou la riche gamme de propriétés pouvant être décrites par des automates ou des formules de logique temporelle que l’on retrouve dans les domaines de l’informatique et de la robotique.
Les approches symboliques présentées dans cet article ont pour but de s’attaquer à l’intersection de ces deux points. Ces approches s’appuient sur trois étapes successives :
-
l’abstraction du système dynamique continu en un modèle symbolique discret décrit par un système dynamique avec un nombre fini d’états et de commandes ;
-
la synthèse d’un contrôleur dans le domaine discret ;
-
la concrétisation du contrôleur symbolique pour son application sur le système continu de départ.
Contrairement aux méthodes de commande prédictive, l’intégralité de ces trois étapes est réalisée hors ligne, et l’application en ligne du contrôleur concrétisé se fait par le biais d’un simple tableau de correspondance.
Ces approches à base d’abstraction symbolique ont de nombreux avantages. Le premier est qu’elles peuvent traiter une très large gamme de systèmes dynamiques non linéaires complexes (avec perturbations, incertitudes, contraintes d’état ou de commande) d’une manière complètement automatique puisque la synthèse de contrôleur dans le domaine discret est indépendante de la forme et de la complexité des dynamiques continues. Elles permettent également de s’intéresser à une nouvelle gamme de spécifications plus variées et plus complexes que celles traditionnellement considérées en automatique continue, telles que des formules de logique temporelle. D’autre part, les algorithmes utilisés pour la synthèse dans le domaine discret sont issus des domaines des méthodes formelles et du model checking, et permettent d’obtenir des garanties formelles de la satisfaction des spécifications même après la concrétisation du contrôleur vers le domaine continu ; le contrôleur est ainsi certifié « correct par construction ». Enfin, puisque la première étape d’abstraction symbolique s’appuie sur des méthodes à base de surapproximations de l’ensemble des comportements réels du système, l’approche globale se retrouve dotée d’une certaine robustesse intrinsèque en supplément de la prise en compte des perturbations et incertitudes du modèle. En revanche, la principale limitation des approches symboliques est leur complexité exponentielle en la dimension de l’espace d’état, ce qui les rend difficiles à appliquer sur des systèmes de grande dimension. Mais de nombreux travaux, présentés dans la section 4 de cet article, ont déjà été réalisés pour réduire cette complexité et permettre un meilleur passage à l’échelle des méthodes symboliques.
Bien qu’il existe de nombreuses variations et améliorations possibles sur la manière de mettre en œuvre les trois étapes constituant les approches symboliques, l’objectif de cet article est de fournir une présentation synthétique et pédagogique de la méthode au cœur de toutes ces approches, afin d’être facilement utilisable. Nous commençons par l’introduction des définitions nécessaires à la description des étapes 1 et 3 de l’approche symbolique, c’est-à-dire l’abstraction du problème du domaine continu vers le domaine discret, et la concrétisation du contrôleur discret vers le domaine continu. Nous présentons ensuite l’étape 2 pour la synthèse d’un contrôleur symbolique dans le domaine discret, pour plusieurs types d’objectifs de contrôle, en mettant l’accent sur les spécifications de sûreté. L’approche complète est alors illustrée par un exemple numérique sur un véhicule modélisé comme un monocycle devant visiter plusieurs régions (avec contraintes sur leur ordre) et en éviter d’autres. La présentation de cet article se focalisant sur la méthode de base des approches symboliques, dans la section 4 nous proposons une ouverture sur les nombreuses variations et améliorations des méthodes symboliques ayant été récemment publiées dans la littérature scientifique, en donnant une attention particulière aux méthodes permettant de réduire ou de s’abstraire des problèmes de complexités.
MOTS-CLÉS
Contrôle des systèmes non linéaires méthodes formelles modèle symbolique synthèse discrète
KEYWORDS
Control of nonlinear systems | formal methods | symbolic model | discrete synthesis
DOI (Digital Object Identifier)
Cet article fait partie de l’offre
Automatique et ingénierie système
(138 articles en ce moment)
Cette offre vous donne accès à :
Une base complète d’articles
Actualisée et enrichie d’articles validés par nos comités scientifiques
Des services
Un ensemble d'outils exclusifs en complément des ressources
Un Parcours Pratique
Opérationnel et didactique, pour garantir l'acquisition des compétences transverses
Doc & Quiz
Des articles interactifs avec des quiz, pour une lecture constructive
Présentation
Cet article fait partie de l’offre
Automatique et ingénierie système
(138 articles en ce moment)
Cette offre vous donne accès à :
Une base complète d’articles
Actualisée et enrichie d’articles validés par nos comités scientifiques
Des services
Un ensemble d'outils exclusifs en complément des ressources
Un Parcours Pratique
Opérationnel et didactique, pour garantir l'acquisition des compétences transverses
Doc & Quiz
Des articles interactifs avec des quiz, pour une lecture constructive
BIBLIOGRAPHIE
-
(1) - TABUADA (P.) - Verification and control of hybrid systems : a symbolic approach. - Springer Science & Business Media (2009).
-
(2) - REISSIG (G.), WEBER (A.), RUNGGER (M.) - Feedback refinement relations for the synthesis of symbolic controllers. - IEEE Transactions on Automatic Control, 62(4) :1781–1796 (2016).
-
(3) - ALTHOFF (M.), FREHSE (G.), GIRARD (A.) - Set propagation techniques for reachability analysis. - Annual Review of Control, Robotics, and Autonomous Systems, 4 :369–395 (2021).
-
(4) - ANGELI (D.), SONTAG (E.D.) - Monotone control systems. - IEEE Transactions on Automatic Control, 48(10) :1684–1698 (2003).
-
(5) - MEYER (P.-J.), DEVONPORT (A.), ARCAK (M.) - Interval Reachability Analysis: Bounding Trajectories of Uncertain Systems with Boxes for Control and Verification. - Springer (2021).
-
...
DANS NOS BASES DOCUMENTAIRES
SCOTS : A Tool for the Synthesis of Symbolic Controllers
https://gitlab.lrz.de/hcs/scots
pFaces : An Acceleration Ecosystem for Formal Methods in Control
https://github.com/parallall/pFaces
Co4Pro : Correct by Construction Controllers from Control Programs
https://github.com/girardan/Co4Pro
RObustly Complete control Synthesis (ROCS)
https://git.uwaterloo.ca/hybrid-systems-lab/rocs
QUEST : A Tool for State-Space Quantization-Free Synthesis of Symbolic Controllers
https://gitlab.lrz.de/hcs/QUEST
CoSyMA : A Tool for Controller Synthesis Using Multi-scale Abstractions
https://github.com/mouelhis/cosymast
TIRA : Toolbox for Interval Reachability Analysis
https://gitlab.com/pj_meyer/TIRA
COntinuous Reachability Analyzer (CORA)
https://github.com/TUMcps/CORA
...Cet article fait partie de l’offre
Automatique et ingénierie système
(138 articles en ce moment)
Cette offre vous donne accès à :
Une base complète d’articles
Actualisée et enrichie d’articles validés par nos comités scientifiques
Des services
Un ensemble d'outils exclusifs en complément des ressources
Un Parcours Pratique
Opérationnel et didactique, pour garantir l'acquisition des compétences transverses
Doc & Quiz
Des articles interactifs avec des quiz, pour une lecture constructive