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

• URL: http://arxiv.org/abs/2607.18731v1
• Date: Tue, 21 Jul 2026 05:43:19 GMT
• Title: Correct-by-Construction Behavior Tree Synthesis from Signal Temporal Logic Specifications with Application to Robotic Missions
• Abstract summary: Behavior Trees (BTs) are widely adopted for complex task execution in robotics.<n>This letter synthesizes correct-by-construction BTs from Signal Temporal Logic (STL) specifications.
• Score: 5.524204636266904
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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.

Related papers

• An Operator-Based Approach to STL [10.103844123344057]
  We propose a novel approach to Signal Temporal Logic (STL) based on an operator acting on reachability value functions.<n>This constitutes a new theoretical framework for handling complex multi-nested formulae.<n>In contrast to focusing on the design of STL-based reachability functions, we develop operator-based nesting rules.
  arXiv  Detail & Related papers  (2026-05-27T07:47:45Z)
• Signal Temporal Logic Motion Planning via Graphs of Convex Sets [8.443328067924298]
  This paper investigates continuous-time motion planning under Signal Temporal Logic (STL) specifications.<n>We propose a framework that combines timed-automata reasoning with graphs of convex sets.<n> Numerical experiments on low-dimensional benchmarks, a $3$-Drotor, a $30$-DoF humanoid, and a hardware experiment on a UR-3 robot arm demonstrate that the proposed method efficiently solves complex STL motion-planning problems.
  arXiv  Detail & Related papers  (2026-05-22T05:19:43Z)
• How LLMs Fail and Generalize in RTL Coding for Hardware Design? [56.361436215029045]
  We introduce a new error taxonomy grounded in problem solvability, inspired by cognitive theory.<n>Our taxonomy categorizes failures into syntactic, semantic, solvable functional, and unsolvable functional types.
  arXiv  Detail & Related papers  (2026-04-26T14:34:49Z)
• Ternary Logic Encodings of Temporal Behavior Trees with Application to Control Synthesis [5.99447754429793]
  Temporal BTs offer a promising approach by leveraging existing temporal logic formalisms to specify and verify executions of BTs.<n>We reformulate TBTs using a ternary-valued Signal Temporal Logic (STL) amenable for control.<n>We propose mixed-integer linear encodings for partial trajectory STL and TBTs over ternary logic allowing for correct-by-construction control strategies.
  arXiv  Detail & Related papers  (2026-04-13T22:07:05Z)
• Do It for HER: First-Order Temporal Logic Reward Specification in Reinforcement Learning (Extended Version) [49.462399222747024]
  We propose a novel framework for the logical specification of non-Markovian rewards in Decision Processes (MDPs) with large state spaces.<n>Our approach leverages Linear Temporal Logic Modulo Theories over finite traces (LTLfMT)<n>We introduce a method based on reward machines and Hindsight Experience Replay (HER) to translate first-order logic specifications and address reward sparsity.
  arXiv  Detail & Related papers  (2026-02-05T22:11:28Z)
• Zero-Shot Instruction Following in RL via Structured LTL Representations [54.08661695738909]
  Linear temporal logic (LTL) is a compelling framework for specifying complex, structured tasks for reinforcement learning (RL) agents.<n>Recent work has shown that interpreting instructions as finite automata, which can be seen as high-level programs monitoring task progress, enables learning a single generalist policy capable of executing arbitrary instructions at test time.<n>We propose a novel approach to learning a multi-task policy for following arbitrary instructions that addresses this shortcoming.
  arXiv  Detail & Related papers  (2025-12-02T10:44:51Z)
• Unlocking Symbol-Level Precoding Efficiency Through Tensor Equivariant Neural Network [84.22115118596741]
  We propose an end-to-end deep learning (DL) framework with low inference complexity for symbol-level precoding.<n>We show that the proposed framework captures substantial performance gains of optimal SLP, while achieving an approximately 80-times speedup over conventional methods.
  arXiv  Detail & Related papers  (2025-10-02T15:15:50Z)
• AutoLayout: Closed-Loop Layout Synthesis via Slow-Fast Collaborative Reasoning [102.71841660031065]
  Auto is a fully automated method that integrates a closed-loop self-validation process within a dual-system framework.<n>The effectiveness of Auto was validated across 8 distinct scenarios, where it demonstrated a significant 10.1% improvement over SOTA methods.
  arXiv  Detail & Related papers  (2025-07-06T08:35:22Z)
• STLCG++: A Masking Approach for Differentiable Signal Temporal Logic Specification [9.039665244779185]
  We present STLCG++, a masking-based approach that parallelizes STL computation and backpropagation across timesteps.<n>We also introduce a smoothing technique to enable the differentiation of time interval bounds, thereby expanding STL's applicability in gradient-based optimization tasks.
  arXiv  Detail & Related papers  (2025-01-08T00:06:43Z)
• DeepLTL: Learning to Efficiently Satisfy Complex LTL Specifications for Multi-Task RL [59.01527054553122]
  Linear temporal logic (LTL) has recently been adopted as a powerful formalism for specifying complex, temporally extended tasks.<n>Existing approaches suffer from several shortcomings.<n>We propose a novel learning approach to address these concerns.
  arXiv  Detail & Related papers  (2024-10-06T21:30:38Z)
• LTLDoG: Satisfying Temporally-Extended Symbolic Constraints for Safe Diffusion-based Planning [12.839846486863308]
  In this work, we focus on generating long-horizon trajectories that adhere to novel static and temporally-extended constraints/instructions at test time. We propose a data-driven diffusion-based framework, finiteDoG, that modifies the inference steps of the reverse process given an instruction specified using linear temporal logic. Experiments in robot navigation and manipulation illustrate that the method is able to generate trajectories that satisfy formulae that specify obstacle avoidance and visitation sequences.
  arXiv  Detail & Related papers  (2024-05-07T11:54:22Z)
• Certified Reinforcement Learning with Logic Guidance [78.2286146954051]
  We propose a model-free RL algorithm that enables the use of Linear Temporal Logic (LTL) to formulate a goal for unknown continuous-state/action Markov Decision Processes (MDPs) The algorithm is guaranteed to synthesise a control policy whose traces satisfy the specification with maximal probability.
  arXiv  Detail & Related papers  (2019-02-02T20:09:32Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.