Présentation

Article

1 - ABSTRACTION SYMBOLIQUE D’UN SYSTÈME COMPLEXE

2 - SYNTHÈSE D’UN CONTRÔLEUR SYMBOLIQUE

3 - EXEMPLE NUMÉRIQUE : CONTRÔLE D’UN ROBOT MOBILE

4 - THÈMES AVANCÉS EN COMMANDE SYMBOLIQUE

5 - CONCLUSION

6 - GLOSSAIRE

7 - SIGLES, NOTATIONS ET SYMBOLES

Article de référence | Réf : S7467 v1

Thèmes avancés en commande symbolique
Approches symboliques pour le contrôle des systèmes non linéaires

Auteur(s) : Antoine GIRARD, Pierre-Jean MEYER, Adnane SAOUD

Date de publication : 10 sept. 2024

Pour explorer cet article
Télécharger l'extrait gratuit

Vous êtes déjà abonné ?Connectez-vous !

Sommaire

Présentation

Version en anglais En anglais

RÉ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’article

ABSTRACT

Symbolic approaches for the control of non linear systems

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.

Cet article est réservé aux abonnés.
Il vous reste 95% à découvrir.

Pour explorer cet article
Téléchargez l'extrait gratuit

Vous êtes déjà abonné ?Connectez-vous !


L'expertise technique et scientifique de référence

La plus importante ressource documentaire technique et scientifique en langue française, avec + de 1 200 auteurs et 100 conseillers scientifiques.
+ de 10 000 articles et 1 000 fiches pratiques opérationnelles, + de 800 articles nouveaux ou mis à jours chaque année.
De la conception au prototypage, jusqu'à l'industrialisation, la référence pour sécuriser le développement de vos projets industriels.

KEYWORDS

Control of nonlinear systems   |   formal methods   |   symbolic model   |   discrete synthesis

DOI (Digital Object Identifier)

https://doi.org/10.51257/a-v1-s7467


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

ABONNEZ-VOUS

Lecture en cours
Présentation
Version en anglais En anglais

4. Thèmes avancés en commande symbolique

Les approches de contrôle symbolique sont aujourd’hui considérées comme un outil puissant pour le contrôle des systèmes dynamiques. Elles présentent plusieurs avantages par rapport aux approches classiques de l’automatique :

  • traitement d’une large classe de systèmes (non linéaires, hybrides, incertains…) sous contraintes ;

  • traitement de spécifications complexes comme celles évoquées dans la section 2. Ces spécifications sont très représentatives des systèmes dynamiques modernes tels que les robots ou les véhicules autonomes ;

  • prise en compte de l’interaction entre le logiciel de contrôle et les processus physiques : le modèle symbolique et le logiciel de contrôle implémenté dans la plateforme de calcul numérique sont décrits dans un cadre unifié (par exemple, en tant que dynamiques symboliques). Cela permet de tenir compte des contraintes sur la partie logiciel lors de la synthèse du contrôleur ;

  • l’approche est automatique et formelle : la synthèse du contrôleur est effectuée de manière automatique, sans recourir à des techniques heuristiques (contrairement à des contrôleurs PID, qui nécessitent des réglages et des tests). De plus, les garanties sont formelles, au sens où le système en boucle fermée satisfait la spécification. Ce type de garantie est obtenu en combinant deux types de preuves : des preuves mathématiques dans la phase d’abstraction, en se basant par exemple sur des outils d’analyse d’atteignabilité ; et des preuves algorithmiques, durant la phase de synthèse de contrôleur en se basant sur des outils de la communauté des méthodes formelles tels que les algorithmes de vérification de modèles ...

Cet article est réservé aux abonnés.
Il vous reste 94% à découvrir.

Pour explorer cet article
Téléchargez l'extrait gratuit

Vous êtes déjà abonné ?Connectez-vous !


L'expertise technique et scientifique de référence

La plus importante ressource documentaire technique et scientifique en langue française, avec + de 1 200 auteurs et 100 conseillers scientifiques.
+ de 10 000 articles et 1 000 fiches pratiques opérationnelles, + de 800 articles nouveaux ou mis à jours chaque année.
De la conception au prototypage, jusqu'à l'industrialisation, la référence pour sécuriser le développement de vos projets industriels.

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

ABONNEZ-VOUS

Lecture en cours
Thèmes avancés en commande symbolique
Sommaire
Sommaire

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).

  • ...

1 Outils logiciels

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 est réservé aux abonnés.
Il vous reste 92% à découvrir.

Pour explorer cet article
Téléchargez l'extrait gratuit

Vous êtes déjà abonné ?Connectez-vous !


L'expertise technique et scientifique de référence

La plus importante ressource documentaire technique et scientifique en langue française, avec + de 1 200 auteurs et 100 conseillers scientifiques.
+ de 10 000 articles et 1 000 fiches pratiques opérationnelles, + de 800 articles nouveaux ou mis à jours chaque année.
De la conception au prototypage, jusqu'à l'industrialisation, la référence pour sécuriser le développement de vos projets industriels.

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

ABONNEZ-VOUS