RecherchearXiv cs.RO 19 juin 2026

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

1 source couvre ce sujet·Source originale ↗·

Résumé IASource uniqueImpact UE

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.

Impact France/UE

Bitcraze (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.

Dans nos dossiers

arXiv cs.RO

À lire aussi

1arXiv cs.RO

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

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.

RecherchePaper

1 source

2arXiv cs.RO

Apprentissage de tubes spatiotemporels pour toutes les tâches de logique temporelle de signal, pour le contrôle de systèmes inconnus sous contraintes d'entrée

Le 9 juillet 2026 (arXiv:2607.07136v1), une équipe de chercheurs a publié un nouveau cadre de contrôle basé sur les "spatiotemporal tubes" (STT) destiné aux systèmes non linéaires inconnus de type Euler-Lagrange, sous contraintes d'entrée, pour satisfaire des spécifications de logique temporelle de signal (STL). L'idée centrale : au lieu de calculer une trajectoire optimale classique, la méthode apprend un tube englobant variable dans le temps, modélisé comme une boule dont le centre et le rayon évoluent, dont le confinement de la trajectoire garantit automatiquement le respect de la tâche STL. Ce tube est paramétré conjointement par un réseau de neurones informé par la physique (PINN), entraîné en intégrant directement la métrique de robustesse de la spécification STL comme fonction de perte. Pour les scénarios multi-agents, une métrique de robustesse globale supplémentaire est ajoutée afin que les tubes individuels ne se chevauchent jamais, évitant ainsi les collisions. Une loi de contrôle en forme close est ensuite dérivée pour maintenir la trajectoire dans le tube tout en respectant les bornes du système. L'approche a été validée sur plusieurs études de cas simulées, pas sur du matériel réel. L'intérêt pratique tient au fait que la méthode ne suppose aucune connaissance du modèle dynamique du système, un point de friction majeur pour appliquer des spécifications formelles (STL) à des robots ou véhicules réels dont la dynamique exacte est rarement connue avec précision. En couplant apprentissage par PINN et garanties de robustesse formelle, le travail tente de combler l'écart entre contrôle par apprentissage, souvent sans garantie, et contrôle formel, souvent limité à des modèles simplifiés. La prise en compte explicite des contraintes d'entrée (actionneurs limités) rapproche aussi la méthode de cas d'usage industriels concrets, comme la coordination de flottes de robots mobiles ou de bras manipulateurs. Ce travail s'inscrit dans la lignée des recherches sur les tubes de contrôle (funnel control, control barrier functions) et sur l'usage croissant des PINN pour encoder des contraintes physiques dans l'apprentissage. Les prochaines étapes attendues concernent la validation sur des plateformes matérielles réelles et l'extension à des dynamiques plus complexes que le formalisme Euler-Lagrange.

RecherchePaper

1 source

3arXiv cs.RO

PISTO : inférence proximale pour l'optimisation stochastique de trajectoires

Des chercheurs ont publié sur arXiv (arXiv:2605.07215) un algorithme de planification de trajectoires robotiques appelé PISTO (Proximal Inference for Stochastic Trajectory Optimization). Leur contribution centrale est de démontrer que STOMP, méthode stochastique classique, minimise implicitement une divergence KL par rapport à une distribution de trajectoires de Boltzmann, révélant une structure d'inférence variationnelle (VI) sous-jacente. PISTO exploite cette observation en ajoutant une régularisation KL entre propositions gaussiennes successives, ce qui stabilise les mises à jour et produit une interprétation de type trust-region. L'algorithme reste entièrement sans dérivées et s'appuie sur un échantillonnage Monte Carlo à pondération d'importance. Sur les benchmarks de planification de bras robotiques, PISTO atteint 89 % de taux de succès contre 63 % pour CHOMP et 68 % pour STOMP, tout en générant des trajectoires plus courtes et plus lisses, à deux fois la vitesse des méthodes stochastiques concurrentes. Des validations complémentaires sur des tâches de locomotion et manipulation contact-rich en simulation MuJoCo montrent des performances supérieures aux baselines CEM et MPPI en termes de récompense cumulée. Pour les intégrateurs et ingénieurs en planification de mouvement, l'absence totale de dérivées est une caractéristique décisive : elle permet de traiter des fonctions de coût non-différentiables ou discontinues, fréquentes dans les environnements industriels réels (détection de collisions, zones interdites, contraintes non paramétriques). Le gain de vitesse d'un facteur deux par rapport aux méthodes stochastiques existantes réduit directement les temps de cycle dans les applications de planification en ligne, point critique pour la robotique collaborative et les systèmes pick-and-place haute cadence. La validation sur MuJoCo avec contacts ouvre des perspectives vers la locomotion humanoïde et la manipulation dextre, bien que ces résultats restent pour l'instant entièrement simulés, sans validation sur matériel physique. PISTO s'inscrit dans la lignée de STOMP (développé chez Willow Garage et présenté à l'ICRA 2011) et de ses concurrents gradient-based tels que CHOMP, ainsi que des méthodes stochastiques modernes MPPI (popularisé par NVIDIA en 2017) et CEM. Soumis comme preprint arXiv sans révision par les pairs à ce stade, l'article n'annonce ni déploiement industriel ni partenariat commercial. Son impact pratique dépendra de la mise à disposition du code source et de validations expérimentales sur robot réel, étapes absentes de la publication actuelle.

RecherchePaper

1 source

4arXiv cs.RO

Estimation de pose 6D temporellement cohérente des objets pour le contrôle robotique

Des chercheurs publient sur arXiv (2605.02708v1) une méthode d'estimation de pose 6D d'objets temporellement cohérente pour la commande de robots manipulateurs. L'approche repose sur un graphe de facteurs qui filtre et lisse en ligne les estimations produites par des estimateurs RGB monoculaires standard, sans recours à un capteur de profondeur. Le système combine trois composantes : un modèle de mouvement de l'objet, une estimation explicite de l'incertitude de mesure de pose, et un optimiseur en ligne intégrant les deux. Les auteurs rapportent une amélioration significative sur des benchmarks standardisés d'estimation de pose avec rejet des valeurs aberrantes, sans toutefois chiffrer précisément les gains. La validation expérimentale porte sur une tâche de suivi d'objet par une caméra embarquée sur un manipulateur à commande en couple (torque-controlled). L'estimation de pose 6D (trois degrés de translation, trois de rotation) est un prérequis pour toute manipulation robotique précise : saisie, assemblage, tri industriel. Les estimateurs RGB monoculaires récents atteignent des performances compétitives sur benchmarks, mais présentent des discontinuités temporelles, des sauts brusques d'une image à l'autre, incompatibles avec la stabilité d'une boucle de contrôle en temps réel. Ce travail s'attaque précisément à ce fossé entre performance sur benchmark et déploiement réel : non pas améliorer la précision frame par frame, mais garantir la cohérence temporelle nécessaire à un retour visuel stable. Pour un intégrateur de cellules robotisées, cela réduit la dépendance aux capteurs ToF ou RGBD, plus coûteux et plus sensibles aux conditions d'éclairage industriel. Les graphes de facteurs sont un outil classique du SLAM robotique (localisation et cartographie simultanées), utilisés depuis longtemps dans les estimateurs de navigation, mais leur application à l'estimation de pose d'objet reste moins répandue. Le champ concurrentiel inclut des approches par filtre de Kalman étendu, des méthodes de lissage sur SE(3), ainsi que des systèmes temps réel comme FoundationPose de NVIDIA ou HappyPose, solution open-source portée par des acteurs européens. L'article est pour l'heure un preprint sans validation industrielle publiée ni annonce de déploiement. Les étapes logiques suivantes incluent une comparaison directe avec les méthodes filtrées existantes sur des jeux de données de référence comme YCB-Video ou LINEMOD, et une extension aux scènes multi-objets.

UELa méthode se positionne en concurrent direct de HappyPose, solution open-source portée par des acteurs européens, sans impact opérationnel identifiable à ce stade de preprint non validé industriellement.

RecherchePaper

1 source