Planification de mouvements sûre et vérifiable dans des systèmes robotiques hétérogènes : une approche formelle et hiérarchique // Secure and Verifiable Motion Planning in Heterogeneous Robotic Systems: A Formal and Hierarchical Approach

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 cœur 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.
------------------------------------------------------------------------------------------------------------------------------------------------------------------------
------------------------------------------------------------------------------------------------------------------------------------------------------------------------

This PhD project focuses on the development of a formal and verification-driven framework for motion planning in heterogeneous robotic systems, where robots with different capabilities must coordinate safely and efficiently to accomplish complex missions.
Heterogeneous multi-robot systems are increasingly deployed in safety-critical domains such as disaster response, healthcare, agriculture, and industrial automation. In these contexts, motion planning must go beyond feasibility and performance, ensuring correct coordination, temporal compliance, and safety guarantees. However, many existing approaches treat verification and safety as post-hoc validation steps, which limits their applicability in complex or safety-critical scenarios.
The objective of this thesis is to embed verification directly into the motion planning process, adopting the perspective that motion planning should be treated as a formally verifiable decision-making problem rather than a purely algorithmic optimization task. The proposed approach relies on a hierarchical formal modeling framework based on high-level Petri nets, enabling scalable representation of concurrency, synchronization, and coordination in heterogeneous robotic teams.
The framework supports the formal specification and enforcement of temporal, safety, and coordination constraints, expressed using Linear Temporal Logic (LTL) and related formalisms. In particular, the thesis addresses the enforcement of time-bounded constraints, enabling extensions toward practically relevant fragments of Metric Interval Temporal Logic (MITL) and Signal Temporal Logic (STL) for robotic applications. The work does not aim at solving the general MITL or STL synthesis problem, but rather at supporting structured and verifiable enforcement of quantitative temporal requirements.
Motion planning problems are reformulated as reachability and supervision problems, allowing correctness guarantees to be obtained by construction. The hierarchical structure of the framework supports modular and compositional reasoning, mitigating state explosion while preserving formal verification capabilities.
The doctoral research will involve formal modeling, analysis, and implementation, with validation through numerical simulations and representative multi-robot case studies using dedicated tools. The expected outcome is a robust and formally grounded planning framework that bridges the gap between high-level mission specification and correct execution, enabling reliable deployment of heterogeneous robotic systems in complex environments.
------------------------------------------------------------------------------------------------------------------------------------------------------------------------
------------------------------------------------------------------------------------------------------------------------------------------------------------------------

Début de la thèse : 01/09/2026

Programme doctoral pour les cotutelles internationales de thèse (ADI)

Université Paris-Saclay GS Sciences de l'ingénierie et des systèmes

580 Sciences et Technologies de l'Information et de la Communication

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.
Candidates for this project should possess skills in robotic systems, motion planning, Petri Nets, formal methods (such as Linear Temporal Logic), and programming, particularly in environments simulating or controlling robotic operations. Experience with hierarchical modeling and understanding complex system behaviors in dynamic environments would also be highly beneficial.