RecherchearXiv cs.RO7sem

Planification de trajectoire par retour d'état pour systèmes non linéaires stochastiques avec spécifications en logique temporelle de signal

1 source couvre ce sujet·Source originale ↗·

Résumé IASource uniqueImpact UE

Une équipe de chercheurs a déposé en mai 2026 sur arXiv (réf. 2605.02361) un cadre de planification de mouvement par retour d'état pour systèmes non linéaires stochastiques en temps continu, soumis à des spécifications formelles en Signal Temporal Logic (STL). La STL est un formalisme mathématique qui exprime des exigences comportementales temporelles précises - du type "éviter une zone pendant 3 secondes, puis atteindre la cible dans un rayon donné". L'objectif affiché est de garantir le respect de ces spécifications avec une probabilité de 99,99 % en boucle fermée. La méthode repose sur une stratégie dite d'"érosion de prédicats" : le problème stochastique, mathématiquement intractable, est transformé en optimisation déterministe avec des contraintes STL resserrées, dont l'amplitude est calibrée par un tube atteignable probabiliste (PRT, Probabilistic Reachable Tube) borné via la théorie de la contraction. Le pipeline complet a été validé en simulation sur plusieurs architectures robotiques, puis expérimentalement sur un robot quadrupède réel - dont la marque n'est pas précisée dans la prépublication, limite courante des dépôts arXiv. Les auteurs rapportent des résultats supérieurs aux approches de référence en termes de conservatisme réduit et de taux de satisfaction des spécifications.

Ce travail s'attaque à un verrou bien identifié en robotique formelle : la plupart des méthodes STL existantes supposent soit un système déterministe, soit un modèle linéaire, rendant les garanties probabilistes sur systèmes non linéaires bruités difficiles à obtenir sans explosion combinatoire. En reformulant le problème stochastique en optimisation déterministe compatible avec des solveurs numériques standards, l'approche ouvre une voie d'intégration industrielle sans exiger de matériel de calcul spécialisé. La validation sur quadrupède physique est un signal positif dans un domaine où le sim-to-real gap reste la principale objection aux méthodes formelles. Pour les intégrateurs et décideurs, une garantie probabiliste quantifiée et potentiellement auditable représente un argument concret dans des contextes de certification robotique - à condition que les résultats expérimentaux détaillés confirment la tenue des 99,99 % sur des scénarios variés, ce que le seul résumé ne permet pas de vérifier.

Ces travaux s'inscrivent dans un courant actif combinant planification temporelle et contrôle robuste, aux côtés des Control Barrier Functions (CBF) et des approches MPC-STL (Model Predictive Control avec spécifications temporelles). La théorie de la contraction mobilisée ici, développée notamment par Jean-Jacques Slotine au MIT et remise en avant ces dernières années dans la vérification formelle robotique, constitue l'un des apports méthodologiques distincts de l'article. Aucun acteur européen n'est impliqué dans ces travaux. Les extensions naturelles incluent des spécifications STL imbriquées ou multi-agents, des environnements dynamiques, et une comparaison étendue avec des architectures d'apprentissage par renforcement - domaine concurrent qui adresse des problèmes similaires avec des garanties formelles généralement plus faibles.

Dans nos dossiers

arXiv cs.RO

À lire aussi

1arXiv cs.RO

pdSTL : logique temporelle de signal probabiliste et différentiable pour les systèmes stochastiques

Des chercheurs ont déposé en juin 2026 sur arXiv pdSTL (probabilistic differentiable Signal Temporal Logic), un cadre formel pour robots autonomes opérant dans des environnements stochastiques. Le système étend la Signal Temporal Logic (STL), formalisme standard pour spécifier des propriétés de sécurité et temporelles dans les systèmes dynamiques, en combinant deux capacités jusqu'ici dissociées : la différentiabilité permettant l'optimisation de trajectoires par gradient, et la sémantique probabiliste appliquée aux trajectoires de croyances (belief trajectories), c'est-à-dire la distribution d'états estimée à partir de capteurs bruités. pdSTL calcule des bornes de satisfaction conservatrices via des sémantiques à intervalles propagées compositionnellement, et formule l'évaluation de la robustesse temporelle comme un dépliage récurrent de style LSTM pour une surveillance en temps linéaire. Les expériences couvrent des scénarios simulés d'évitement d'obstacles et de changement de voie, ainsi que des vols réels avec le nano-drone Crazyflie de Bitcraze soumis à des perturbations aérodynamiques. L'apport central est de résoudre simultanément deux lacunes concurrentes des approches existantes. La STL différentiable déterministe (dSTL) permettait l'optimisation par gradient mais supposait des états connus avec certitude, ignorant le bruit de capteur et la dynamique stochastique. Les extensions probabilistes de la STL existantes offraient des garanties formelles mais sacrifiaient la différentiabilité, les rendant incompatibles avec les pipelines d'apprentissage modernes. pdSTL unifie les deux, et les auteurs rapportent qu'il surpasse significativement dSTL pour le maintien des marges de sécurité sous incertitude réelle. Pour un ingénieur robotique ou un intégrateur travaillant sur la navigation autonome, cette combinaison de garanties probabilistes formelles et d'optimisabilité par gradient constitue une brique potentielle pour des spécifications de sécurité certifiables en conditions opérationnelles. La STL est un outil standard de la vérification formelle de systèmes cyber-physiques depuis les années 2010, et ses extensions différentiables avaient déjà intéressé la communauté robotique pour l'optimisation de trajectoires. Le Crazyflie, drone open-source de la société suédoise Bitcraze, est une plateforme académique de référence appréciée pour sa dynamique instable, qui en fait un test exigeant pour toute approche de contrôle robuste. Ce travail est pour l'instant un preprint non relu par les pairs, sans code public annoncé et sans métriques quantitatives précises dans le résumé, ce qui invite à la prudence face aux affirmations de surperformance. Les équipes de motion planning sous incertitude dans les secteurs drones, véhicule autonome et manipulation industrielle sont les premières concernées par une éventuelle implémentation.

UEBitcraze (Suède, UE) fournit la plateforme drone de validation matérielle, ce qui ancre marginalement ce travail académique dans l'écosystème européen, mais sans impact opérationnel direct à ce stade de preprint non relu.

RecherchePaper

1 source

2arXiv cs.RO

DAG-STL : un cadre hiérarchique pour la planification de trajectoires zéro-shot sous contraintes de logique temporelle signalée

Des chercheurs ont publié DAG-STL, un cadre hiérarchique de planification de trajectoires pour robots opérant sous contraintes de Signal Temporal Logic (STL), une logique formelle permettant de spécifier des tâches robotiques structurées dans le temps. Le pipeline decompose-allocate-generate fonctionne en trois étapes : il décompose d'abord une formule STL en conditions de progression d'accessibilité et d'invariance, liées par des contraintes de synchronisation partagées ; il alloue ensuite des waypoints temporels via des estimations d'accessibilité apprises ; enfin, il synthétise les trajectoires entre ces waypoints à l'aide d'un générateur basé sur la diffusion. Les expériences ont été conduites sur trois benchmarks standards : Maze2D, OGBench AntMaze, et le domaine Cube, avec un environnement personnalisé incluant une référence par optimisation. DAG-STL surpasse significativement l'approche concurrente de diffusion guidée par robustesse directe sur des tâches STL à long horizon, et récupère la majorité des tâches solubles par optimisation classique tout en conservant un avantage computationnel notable. L'apport principal de ce travail est de résoudre la planification STL en contexte zero-shot, c'est-à-dire sans avoir jamais vu la tâche cible lors de l'entraînement, et sans modèle analytique de la dynamique du système. Pour les intégrateurs et décideurs en robotique, cela signifie qu'un robot équipé de DAG-STL pourrait recevoir une spécification temporelle formelle inédite et en dériver un plan exécutable uniquement depuis des données de trajectoires génériques préenregistrées. La séparation explicite entre raisonnement logique et réalisation physique de la trajectoire est une décision architecturale structurante : elle réduit les problèmes de planification globale long-horizon à une série de sous-problèmes plus courts et mieux couverts par les données. Le cadre introduit également une métrique de cohérence dynamique sans rollout et un mécanisme de replanification hiérarchique en ligne, deux mécanismes qui adressent directement le gap simulation-réel, sujet central des débats sur le sim-to-real dans les VLA (Vision-Language-Action models). DAG-STL s'inscrit dans un courant de recherche actif qui cherche à doter les robots d'une capacité de généralisation formellement vérifiable, à la croisée de la planification sous contraintes logiques temporelles et des modèles génératifs de trajectoires. La STL est un langage étudié depuis les années 2000 en vérification formelle, mais son application à la planification robotique offline reste difficile faute de modèles dynamiques disponibles dans des environnements réels. Les approches concurrentes incluent les méthodes d'imitation learning task-spécifiques et les planificateurs à base de modèle explicite, que DAG-STL vise à dépasser sur le critère de généralisation. Le preprint est disponible sur arXiv (2604.18343) et les prochaines étapes naturelles seraient une validation sur des plateformes physiques, notamment en manipulation et navigation réelle, pour confirmer les gains observés en simulation.

RecherchePaper

1 source

3arXiv cs.RO

SAGAS : assemblage par graphe sémantique pour la planification hors ligne en logique temporelle

Des chercheurs ont déposé sur arXiv (référence 2512.00775, version 2, 2025) un cadre baptisé SAGAS (Semantic-Aware Graph-Assisted Stitching) pour la planification robotique à long horizon à partir de données hors-ligne uniquement. Le problème ciblé : piloter un agent pour exécuter des tâches complexes décrites en logique temporelle linéaire (LTL), un formalisme mathématique exprimant des séquences de conditions du type "atteindre A, puis B, tout en évitant C", sans modèle de dynamique, sans démonstrations spécifiques à la tâche, et sans interaction en ligne avec l'environnement. SAGAS apprend deux composants offline à partir de fragments de trajectoires hétérogènes : un graphe latent d'atteignabilité réutilisable, et un exécuteur conditionné sur des objectifs figé après l'entraînement. Pour chaque nouvelle formule LTL au moment du test, le système augmente ce graphe avec des propositions sémantiques, puis applique une recherche en produit de Büchi pour synthétiser un plan de waypoints "prefix-suffix" à coût minimisé, exécuté par l'exécuteur figé. Les expériences portent sur les domaines de locomotion d'OGBench, une suite de benchmarks offline standard dans la communauté. La contribution centrale revendiquée est la généralisation zero-shot à des spécifications LTL non vues à l'entraînement, sans récompense tâche-spécifique ni réentraînement de politique. C'est une distinction structurelle face aux deux familles dominantes : la synthèse symbolique model-based exige un système de transitions étiqueté précis, difficile à construire sur du matériel réel, tandis que les méthodes d'apprentissage par renforcement supposent généralement une interaction en ligne ou des démonstrations dédiées. SAGAS déplace le raisonnement propre à chaque formule vers une augmentation de graphe et une recherche symbolique au temps d'inférence, découplant ainsi la capacité de généralisation du processus d'entraînement. À noter : les validations sont entièrement simulées sur OGBench ; le gap sim-to-real n'est pas adressé, ce qui limite la portée industrielle immédiate. La planification LTL en robotique mobilise un nombre croissant d'équipes, portée par le besoin de comportements vérifiables formellement sur des robots industriels et de service. Les approches concurrentes couvrent un spectre large : planification par diffusion (Diffuser, Decision Diffuser), politiques conditionnées par langage naturel via des VLA (vision-language-action models), et combinaisons de model checking avec du renforcement offline sur D4RL (IQL, CQL). SAGAS occupe la niche "offline + symbolique + zero-shot LTL", encore peu exploitée. Aucun déploiement matériel ni partenariat industriel n'est annoncé ; les suites logiques seraient une validation sur plateforme physique et une extension à des environnements à espace d'état plus riche.

RecherchePaper

1 source

4arXiv cs.RO

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.

UELa validation matérielle sur bras UR-3 (Universal Robots, Danemark/UE) offre une pertinence indirecte pour les équipes R&D européennes en planification de trajectoires, mais la recherche est conduite au MIT sans implication directe d'acteurs français ou européens.

RecherchePaper

1 source