让机器人在不确定环境中安全运行，用概率化可微时序逻辑精准优化轨迹。
pdSTL: Probabilistic Differentiable Signal Temporal Logic for Stochastic Systems
- 引入概率可微时序逻辑，统一信念轨迹的不确定性与可微鲁棒性评估
- 通过递归展开实现线性时间可微监控，在模拟与真实飞行中提升安全边际
- 适合需形式化概率保障的自主系统优化，如无人机避障与变道控制
在不确定环境中运行的自主机器人必须满足复杂的时序与安全规范，即使面对随机动力学和传感噪声。信号时序逻辑（STL）虽提供梯度优化的鲁棒性度量，但现有扩展或缺乏可微性，或忽略信念空间不确定性。本文提出概率可微信号时序逻辑（pdSTL），将概率语义与信念轨迹上的可微鲁棒性统一。pdSTL采用区间值概率语义计算保守满足边界，并通过STL语法树逐层传播。我们将时序鲁棒性评估建模为类似LSTM的递归展开，实现线性时间、可微监控，适用于端到端轨迹优化。在障碍物避让、车道变换的仿真以及受气动干扰的真实Crazyflie四轴飞行器实验中验证，pdSTL在保持形式化概率保证的前提下实现了高效优化，显著优于确定性可微STL在真实不确定性下的安全边距表现。
原文摘要 · Abstract (English)
Autonomous robots operating in uncertain environments must satisfy complex temporal and safety specifications despite stochastic dynamics and sensing noise. While Signal Temporal Logic (STL) offers robustness measures for gradient-based optimization, existing extensions either lack differentiability or ignore belief-space uncertainty. We introduce pdSTL (probabilistic differentiable Signal Temporal Logic), a framework that unifies probabilistic semantics with differentiable robustness over belief trajectories. pdSTL employs interval-valued probabilistic semantics to compute conservative satisfaction bounds, propagated compositionally through the STL syntax tree. We formulate the temporal robustness evaluation as a recurrent, LSTM-style unfolding of STL operators, enabling linear-time, differentiable monitoring suitable for end-to-end trajectory optimization. We validate pdSTL on simulated obstacle avoidance, lane-change maneuvers, and real-world Crazyflie quadcopter flight experiments under aerodynamic disturbances. Results demonstrate that pdSTL achieves efficient optimization with formal probabilistic guarantees, significantly outperforming deterministic differentiable STL in maintaining safety margins under real-world uncertainty.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。