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

Conclusion
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 English

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

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

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

(139 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 English

5. Conclusion

Les approches de contrôle symbolique présentent de nombreux avantages :

  • une grande généralité sur les systèmes et objectifs de contrôle complexes pouvant être traités ;

  • une structure de synthèse de contrôleur complètement automatique et indépendante de la complexité, des incertitudes et des contraintes du système considéré ;

  • une robustesse intrinsèque du fait de l’abstraction du système par une surapproximation de l’ensemble de ses comportements ;

  • et des garanties formelles de la satisfaction des spécifications par le système original bien que le contrôleur ait été synthétisé sur son modèle symbolique.

La combinaison de tous ces éléments rend les approches à base d’abstraction symbolique très intéressantes dans de nombreux domaines, et la généralisation de leur utilisation va très vraisemblablement se poursuivre dans les années à venir. Bien que cet article se soit focalisé sur le cas de systèmes à dynamiques déterministes, il est à noter qu’il existe également de nombreux travaux sur les abstractions symboliques de systèmes stochastiques .

Bien que le passage à l’échelle pour le traitement de systèmes de grande dimension soit l’un des principaux défis des méthodes symboliques, la constante amélioration des puissances de calcul atténue progressivement cette limitation. En particulier, l’introduction d’outils d’accélération se basant sur la parallélisation des calculs réalisés sur des cartes graphiques a le potentiel de grandement faciliter l’application...

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.

Cet article fait partie de l’offre

Automatique et ingénierie système

(139 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
Conclusion
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 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

(139 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