用信号时序逻辑生成带时间约束的机器人行为树，确保任务正确性。
Correct-by-Construction Behavior Tree Synthesis from Signal Temporal Logic Specifications with Application to Robotic Missions
- 基于信号时序逻辑构建带时间约束的行为树，实现从规格到控制的正确性构造。
- 在仿真和六条规格下验证，无人机实验满足严格正鲁棒性要求。
- 适合需要形式化保障的复杂机器人任务部署，如无人系统自主决策。
行为树（BTs）广泛用于机器人复杂任务执行，具备模块化、响应式控制优势，但缺乏形式化保证。现有基于线性时序逻辑（LTL）的正确性构造方法无法表达定量时间约束。本文提出从信号时序逻辑（STL）规格中合成正确性保证的行为树。将工作空间建模为时序转移系统，并抽象为区域图；引入扩展状态空间以同时追踪逻辑进展与时间约束。采用分层不动点算法计算包含安全、可达、响应、重复与持续性等特性的STL片段的获胜集，生成带运行时约束函数的子树。证明了正确性并给出了复杂度界。仿真显示规格满足且具有严格正鲁棒性；六条STL规格下的物理四旋翼实验验证了实际可部署性。
原文摘要 · Abstract (English)
Behavior Trees (BTs) are widely adopted for complex task execution in robotics, providing modular, reactive control but lacking formal guarantees. However, existing correct-by-construction synthesis from Linear Temporal Logic (LTL) cannot express quantitative timing constraints. This letter synthesizes correct-by-construction BTs from Signal Temporal Logic (STL) specifications. The workspace is modeled as a timed transition system and abstracted into a zone graph, and an augmented state space tracking both logical progress and timing constraints is introduced. A hierarchical fixed-point algorithm computes winning sets for an STL fragment encompassing safety, reachability, response, recurrence, and persistence, yielding BT subtrees with a runtime constraint function. Correctness guarantees are proven and complexity bounds are derived. Simulations demonstrate specification satisfaction with strictly positive robustness, and a physical quadrotor experiment with six STL specifications validates practical deployability.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。