Track papers across labs, topics, and trends.
Search papers, labs, and topics across Lattice.
This paper synthesizes Behavior Trees (BTs) from Signal Temporal Logic (STL) specifications, addressing the limitations of existing methods that rely on Linear Temporal Logic (LTL) and cannot handle quantitative timing constraints. By modeling the workspace as a timed transition system and employing a hierarchical fixed-point algorithm, the authors derive BT subtrees that ensure correctness and meet specified timing requirements. The approach is validated through simulations and a physical quadrotor experiment, demonstrating robust performance across multiple STL specifications.
Correctly synthesizing Behavior Trees from Signal Temporal Logic allows for precise timing guarantees in robotic missions, a significant leap beyond traditional methods.
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.