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