Correct-by-Construction Behavior Tree Synthesis from Signal Temporal Logic Specifications with Application to Robotic Missions
For roboticists needing formal guarantees for complex tasks with timing constraints, this provides a correct-by-construction synthesis method for Behavior Trees, addressing a gap in existing LTL-based approaches.
This work synthesizes correct-by-construction Behavior Trees from Signal Temporal Logic specifications, enabling formal guarantees for quantitative timing constraints in robotic missions. Simulations and a physical quadrotor experiment with six STL specifications demonstrate satisfaction with strictly positive robustness.
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.