AI 中文总结
研究从信号时序逻辑规范合成构建正确的行为树，通过将工作空间建模为定时转换系统并抽象为区域图，引入增强状态空间，利用分层定点算法计算获胜集，证明正确性并推导复杂度界限，经仿真和实验验证了方法的有效性和可部署性。
AI 中文摘要
行为树广泛用于机器人复杂任务执行，提供模块化、反应式控制，但缺乏形式保证。现有从线性时序逻辑的构建正确的合成无法表达定量时序约束。本文从信号时序逻辑规范合成构建正确的行为树。将工作空间建模为定时转换系统并抽象为区域图，引入跟踪逻辑进展和时序约束的增强状态空间。通过分层定点算法计算包含安全、可达性、响应、递归和持久性的信号时序逻辑片段的获胜集，产生具有运行时约束函数的行为树子树。证明了正确性保证并推导了复杂度界限。仿真表明满足规范且具有严格正鲁棒性，物理四旋翼实验验证了实际可部署性。
英文摘要
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.
Comments8 pages, 9 figures. This work has been submitted to the IEEE for possible publication
