Thèse Planification de Mouvements Sûre et Vérifiable dans des Systèmes Robotiques Hétérogènes une Approche Formelle et Hiérarchique H/F - Université Paris-Saclay GS Sciences de l'ingénierie et des systèmes

Établissement : Université Paris-Saclay GS Sciences de l'ingénierie et des systèmes
École doctorale : Sciences et Technologies de l'Information et de la Communication
Laboratoire de recherche : Laboratoire Universitaire de Recherche en Production Automatisée
Direction de la thèse : Grégory FARAUT ORCID 000000030388932X
Début de la thèse : 2026-09-01
Date limite de candidature : 2026-03-20T23:59:59

Ce projet de thèse porte sur le développement d'un cadre formel, guidé par la vérification, pour la planification de mouvements au sein de systèmes robotiques hétérogènes, où des robots aux capacités différentes doivent se coordonner de manière sûre et efficace afin d'accomplir des missions complexes.
Les systèmes multi-robots hétérogènes sont de plus en plus déployés dans des domaines critiques pour la sécurité, tels que la réponse aux catastrophes, la santé, l'agriculture et l'automatisation industrielle. Dans ces contextes, la planification de mouvements doit dépasser la seule faisabilité et les performances : elle doit garantir une coordination correcte, le respect de contraintes temporelles et des garanties de sûreté. Or, de nombreuses approches existantes considèrent la vérification et la sûreté comme des étapes de validation a posteriori, ce qui limite leur applicabilité dans des scénarios complexes ou critiques.
L'objectif de cette thèse est d'intégrer la vérification directement au coeur du processus de planification, en adoptant l'idée que la planification de mouvements doit être traitée comme un problème de prise de décision formellement vérifiable, plutôt que comme une simple tâche d'optimisation algorithmique. L'approche proposée s'appuie sur un cadre de modélisation formelle hiérarchique basé sur des réseaux de Petri de haut niveau, permettant une représentation scalable de la concurrence, de la synchronisation et de la coordination dans des équipes robotiques hétérogènes.
Le cadre permet de spécifier et d'imposer formellement des contraintes temporelles, de sûreté et de coordination, exprimées à l'aide de la logique temporelle linéaire (LTL) et de formalismes apparentés. En particulier, la thèse traite de l'imposition de contraintes bornées en temps, ouvrant la voie à des extensions vers des fragments d'intérêt pratique de la logique temporelle à intervalles métriques (MITL) et de la logique temporelle sur signaux (STL) pour des applications robotiques. Le travail ne vise pas à résoudre le problème général de synthèse en MITL ou en STL, mais plutôt à supporter une prise en compte structurée et vérifiable d'exigences temporelles quantitatives.
Les problèmes de planification de mouvements sont reformulés comme des problèmes d'atteignabilité et de supervision, de manière à obtenir des garanties de correction « par construction ». La structure hiérarchique du cadre favorise un raisonnement modulaire et compositionnel, atténuant l'explosion combinatoire des états tout en conservant les capacités de vérification formelle.
Le travail doctoral impliquera des activités de modélisation formelle, d'analyse et d'implémentation, avec une validation au moyen de simulations numériques et d'études de cas multi-robots représentatives, réalisées avec des outils dédiés. Le résultat attendu est un cadre de planification robuste et solidement fondé sur des bases formelles, qui comble l'écart entre la spécification de mission de haut niveau et l'exécution correcte, et qui permette un déploiement fiable de systèmes robotiques hétérogènes dans des environnements complexes.

The context involves the growing complexity of tasks and environments for robotic systems, necessitating advanced motion planning techniques. Traditional methods face limitations in scalability and flexibility, particularly in heterogeneous teams, prompting the need for innovative approaches like the HLrtPN system.

This thesis contributes to the field of robotic motion planning by proposing a formal, verification-driven framework for the coordination and execution of missions in heterogeneous robotic systems. The contributions go beyond algorithmic planning by integrating formal modeling, temporal reasoning, and correctness guarantees into a unified verification-driven approach. This includes both qualitative temporal reasoning and quantitative time-bounded constraints, which are essential for real-world robotic applications.

Les candidats pour ce projet doivent posséder des compétences en systèmes robotiques, planification de mouvements, réseaux de Petri, méthodes formelles (telles que la logique temporelle linéaire) et programmation, en particulier dans des environnements simulant ou contrôlant des opérations robotiques. Une expérience avec la modélisation hiérarchique et la compréhension des comportements des systèmes complexes dans des environnements dynamiques serait également très bénéfique.