Exemple numérique : contrôle d’un robot mobile
Approches symboliques pour le contrôle des systèmes non linéaires

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.