Planification de mouvements par logique temporelle de signaux via des graphes d'ensembles convexes

Une équipe de chercheurs a publié sur arXiv (arXiv:2605.23240) un cadre de planification de trajectoires en temps continu combinant la logique temporelle de signaux (STL, Signal Temporal Logic) et les graphes d'ensembles convexes (GCS, Graphs of Convex Sets). L'objectif est de générer des trajectoires lisses satisfaisant à la fois des contraintes logico-temporelles de haut niveau, par exemple "atteindre la zone A entre t=2 s et t=5 s tout en évitant B", et des limites cinématiques de bas niveau comme les bornes de vitesse. La méthode encode d'abord la spécification STL sous forme d'automate temporisé, le couple à une décomposition convexe de l'espace de configuration, puis reformule l'ensemble comme un problème de plus court chemin sur un GCS. La solution produit des trajectoires en B-splines de Bézier, validées expérimentalement sur un quadrirotor 3D, un humanoïde à 30 degrés de liberté (DoF) et un bras industriel UR-3 testé en conditions matérielles réelles.

La contribution principale est de rendre tractable un problème historiquement difficile. Les approches classiques de planification sous STL s'appuient sur la programmation mixte entière (MILP), dont la complexité est exponentielle avec la dimension de l'espace ou la longueur de l'horizon temporel. Ce travail démontre qu'une fois l'automate temporisé et la décomposition convexe fixés, la relaxation convexe évolue polynomialement avec la dimension de l'espace de configuration et le degré des splines de Bézier, ce qui constitue une garantie de passage à l'échelle concrète. Le test sur un humanoïde à 30 DoF est significatif : c'est précisément la gamme de systèmes où les planificateurs STL classiques échouent. La validation hardware sur UR-3 confirme que les trajectoires produites sont directement exécutables, sans post-traitement supplémentaire.

Le cadre GCS a été introduit vers 2022 par Marcucci, Tedrake et leurs collaborateurs au MIT comme outil d'optimisation de trajectoires dans des espaces fragmentés en régions convexes. Ce papier étend l'approche aux spécifications temporelles contraintes, une jonction entre vérification formelle et robotique opérationnelle. Les approches concurrentes incluent la MPC non linéaire sous STL et les planificateurs par échantillonnage avec satisfaction de contraintes temporelles. L'article reste un preprint non relu par les pairs ; les benchmarks présentés couvrent essentiellement des espaces de basse à moyenne dimension, et l'extension aux environnements dynamiques ou à la replanification en temps réel n'est pas encore abordée.