cs.ROJul 21, 2026

Correct-by-Construction Behavior Tree Synthesis from Signal Temporal Logic Specifications with Application to Robotic Missions

Authors: Jiaheng DongJingyi HuangLiang Han

Organizations: Sino-French Engineer School,Beihang University, Beijing 100191, China

Abstract

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.

Explore similar work

CardsList
  1. Contract-Grounded Behavior Tree Synthesis via Coding Agents

    Jul 13, 2026Jonathan Salfity, Robert Blake Anderson, Mitch PryorExecutable Robot BehaviorCoding Agents