En poursuivant votre navigation sur ce site, vous acceptez le dépôt de cookies dans votre navigateur. (En savoir plus)

Thèse (H/F): Synthèse de contrôleurs robustes par approches symboliques

Cette offre est disponible dans les langues suivantes :
Français - Anglais

Assurez-vous que votre profil candidat soit correctement renseigné avant de postuler. Les informations de votre profil complètent celles associées à chaque candidature. Afin d’augmenter votre visibilité sur notre Portail Emploi et ainsi permettre aux recruteurs de consulter votre profil candidat, vous avez la possibilité de déposer votre CV dans notre CVThèque en un clic !

Faites connaître cette offre !

Informations générales

Référence : UMR8506-ANTGIR-002
Lieu de travail : GIF SUR YVETTE
Date de publication : lundi 25 novembre 2019
Nom du responsable scientifique : Antoine Girard
Type de contrat : CDD Doctorant/Contrat doctoral
Durée du contrat : 36 mois
Date de début de la thèse : 1 mars 2020
Quotité de travail : Temps complet
Rémunération : 2 135,00 € brut mensuel

Description du sujet de thèse

Problématique:

Véhicules autonomes, bâtiments intelligents ou robots promettent de transformer le quotidien de notre société dans toutes ses dimensions (transport, logement, industrie, santé, assistance aux personnes âgées ...). Ces systèmes sont des exemples de systèmes cyber-physiques résultant de l'intégration de composants informatiques et de processus physiques. Le principal objectif du projet PROCSYS est de fournir un cadre de programmation pour les CPS permettant un développement rapide et sûr de leurs fonctionnalités grâce à un langage de haut niveau. Des algorithmes de synthèse génèrent alors automatiquement des contrôleurs de bas niveau qui exécutent le comportement spécifié. La correction des contrôleurs est garantie en suivant le paradigme de la synthèse correcte par construction grâce à des techniques de contrôle symbolique: la dynamique physique continue est abstraite par un modèle symbolique, qui est un système dynamique purement discret; une interface composée de contrôleurs de bas niveau est conçue pour que le système physique et le modèle symbolique se comportent de manière identique; un contrôleur symbolique de haut niveau est ensuite synthétisé automatiquement à partir du programme de haut niveau et du modèle symbolique.

========================
Objectifs et description du travail:

L'objectif principal de la thèse est de développer des algorithmes pour la synthèse de contrôleurs symboliques robustes. Nous nous appuierons sur nos travaux préliminaires sur la synthèse quantitative de contrôleurs symboliques [4,5]. En utilisant une formulation de commande optimale, on peut synthétiser un contrôleur maximisant une marge de robustesse pour les spécifications de sûreté et d'atteignabilité. Cependant, cette approche ne garantit pas nécessairement la robustesse vis-à-vis des perturbations non modélisées. Dans ce cas, la robustesse peut être obtenue par la satisfaction de deux conditions principales formulées dans [3]. Premièrement, en présence de perturbations, la robustesse doit se dégrader progressivement par rapport à l'amplitude de la perturbation. Cette condition est généralement satisfaite si la fonction de robustesse satisfait à certaines conditions de Lipschitz. Deuxièmement, en l'absence de perturbation, le comportement correct du système doit être rétabli. Cette condition sera satisfaite si la fonction de robustesse satisfait certaines conditions de croissance par rapport aux transitions du modèle symbolique. Pour synthétiser des contrôleurs robustes vis-à-vis des perturbations, il est donc nécessaire d'inclure les deux types de contraintes (Lipschitz et conditions de croissance) dans le problème de contrôle optimal à résoudre. Il sera alors nécessaire de développer des algorithmes pour résoudre ces problèmes de contrôle optimal sous contraintes.

Le travail de doctorat commencera par de simples propriétés de sûreté et d'atteignabilité, puis sera étendu à des spécifications plus complexes définies dans le langage de haut niveau développé dans le cadre du projet PROCSYS. Une évaluation des algorithmes proposés sera effectuée à l'aide d'études de cas numériques, par exemple dans le domaine de la conduite autonome.

============
Profil recherché:

La personne recrutée doit avoir un Master en automatique ou en informatique avec une solide formation en mathématiques. Une expérience préalable dans le domaine des systèmes hybrides est recommandée. Des compétences en programmation sont également nécessaires.

=========
Références:

[1] Belta, C., Yordanov, B., & Gol, E. A. (2017). Formal Methods for Discrete-Time Dynamical Systems (Vol. 89). Springer.
[2] Tabuada, P. (2009). Verification and control of hybrid systems: a symbolic approach. Springer Science & Business Media.
[3] Rungger, M., & Tabuada, P. (2016). A notion of robustness for cyber-physical systems. IEEE Transactions on Automatic Control, 61(8), 2108-2123.
[4] Eqtami A. and Girard A., Safety control, a quantitative approach. IFAC Conference on Analysis and Design of Hybrid Systems, 2018.
[5] Eqtami A. and Girard A., A quantitative framework for transition systems under reachability specifications. Preprint, 2019.

Contexte de travail

Le L2S - Laboratoire des Signaux et Systèmes (UMR8506) est une unité mixte de recherche CNRS, CentraleSupélec et Université Paris Sud, située à Gif-sur-Yvette. Le L2S compte environ 260 personnes dont 108 permanents, 118 doctorants et 33 post-doctorants. Il est organisé en 3 pôles de recherche (Pôle Signaux et Statistiques, Pôle Automatique et Systèmes et Pôle Télécoms et réseaux). Les 3 pôles scientifiques s'appuient sur 3 pôles support à la Recherche : un pôle Gestion des Ressources Humaines et Communication, un pôle Gestion Financière, placés sous la responsabilité de l'administrateur (trice) et un pôle informatique. La structure de l'unité est complétée par un pôle de Calcul scientifique. Le budget exécuté du laboratoire est d'environ 3 M€ par an.

Informations complémentaires

Projet ERC PROCSYS

On en parle sur Twitter !