STL Planning

STL: Signal Temporal Logic

Follow this topic Ask about this topic

Latest papers

17 papers3 papers in the last four weeks, level with the four weeks before. 0.0% of all new papers.

Oct 12, 2026

Belief Space Planning for Risk Signal Temporal Logic via Mixed-Integer Convex Programming

Signal Temporal Logic (STL) specifies robot tasks with spatio-temporal requirements, and its robustness semantics allow planning by trajectory optimization. In practice, robots estimate their state from noisy measurements, and when the information gained from a measurement depends on the state, the robot can actively reduce its uncertainty by planning in the belief space. The resulting problem is, however, generally non-convex, for which gradient-based methods are neither complete nor globally optimal. In this paper, we consider Risk STL (RiSTL) planning in Gaussian belief space and show that an information-form parameterization of the belief, together with a convex relaxation of the belief dynamics, yields a mixed-integer convex program (MICP). We prove that the MICP is sound and complete, and that the relaxation preserves the globally optimal input trajectories. We validate the effectiveness of our method in numerical simulations.

Shaohang Han, Joris Verhagen, Kaier Liang +1

Division of Robotics, Perception and Learning, School of Electrical Engineering and Computer Science, KTH Royal Institute of Technology, Stockholm, Sweden · Digital Futures

Belief-Space Planning STL Planning STL Motion Planning Robot Motion Planning

Oct 11, 2026

Efficient Hybrid Hard--Soft Signal Temporal Logic MPC for Driving under Multimodal Uncertainty

Motion planning for automated vehicles in interactive traffic has to simultaneously ensure safety, respect traffic rules, and maintain comfortable progress under multi-modal behavior uncertainty. Imposing all these requirements as hard constraints reduces feasibility, whereas treating them all as costs allows safety-critical requirements to be traded against progress. We propose a hybrid hard--soft Signal Temporal Logic (STL) MPC framework that optimizes a single shared ego trajectory against every retained behavior hypothesis: minimum-distance and speed predicates are imposed as explicit hard constraints, while soft STL robustness terms shape clearance, comfort, and interaction quality within the resulting feasible driving corridor. This retains robustness to discrete interaction modes without branch-specific contingent ego policies. We further identify substantial symbolic graph-construction overhead and introduce reachability-certified relevance screening and vectorized symbolic construction to reduce computational cost while preserving the feasible set and objective. Closed-loop Monte Carlo evaluation over six highway and intersection scenarios shows the highest strict success rate among the compared planners with no observed collisions or rule violations, at roughly a quarter of the planning latency of the unoptimized formulation. An ablation study separates the two layers: the hard constraints define the safety envelope, while the soft terms improve clearance and motion quality within it.

Kumar Manas, Adrian Paschke

Technical University Darmstadt, Germany · Freie Universität Berlin, Germany · Freie Universität Berlin and Fraunhofer FOKUS, Berlin, Germany

STL Planning Safe Motion Planning Autonomous Driving Planning STL Motion Planning Constrained Motion Planning Model Predictive Control+1

Oct 5, 2026

ScanSTL: Parallel Robustness Evaluation for Signal Temporal Logic

Repeated evaluation and differentiation of Signal Temporal Logic (STL) robustness can become a computational bottleneck in robot planning and control. Sequential temporal recurrences limit parallelism, while dense masking increases memory requirements. We propose ScanSTL, which combines associative temporal aggregation with parallel scans and ordered block reductions. Eventually and Always use range extrema, while inclusive strong Until composes compact segment representations. A common range engine handles bounded and shifted intervals, including the guards required before delayed Until witnesses. Each exact temporal operator computes complete robustness traces with linear work and storage and logarithmic parallel depth on uniformly sampled finite signals. An open source JAX implementation supports automatic differentiation, batching, and compilation. We compare ScanSTL with STLCG and STLCG++ using CPU and GPU operator benchmarks and nine composed specifications. Across these nine specifications at 512 samples, ScanSTL achieves geometric mean speedups of 243 times for forward evaluation and 104 times for gradient computation over STLCG++ in JAX on the CPU. On an RTX~5090 GPU, ScanSTL evaluates unbounded Until over more than two million samples with median times below 0.1 ms for forward evaluation and 0.25 ms for gradient computation. Simulated escort and patrol experiments with a robot dog further demonstrate faster repair of violating plans and greater solver capacity in model predictive control.

Gokhan Alcan

Automation Technology and Mechanical Engineering, Tampere University, 33100 Tampere, Finland

Signal Temporal Logic STL Planning

Sep 19, 2026

A Geometric Decision Procedure for STL Feasibility and Repair

Feasibility of a Signal Temporal Logic (STL) specification asks whether, from a given initial state, an admissible control input can satisfy its continuous-time requirements under actuator limits. Establishing feasibility is essential for detecting unrealizable tasks and repairing specifications before execution. State-of-the-art Mixed-Integer Linear Programming (MILP) methods face growing model sizes as temporal horizons and formula complexity increase, and can accept control witnesses that violate continuous-time STL semantics between samples. We propose a geometric approach to STL feasibility and temporal repair that translates temporal requirements into spatial constraints evaluated at the initial state. Its compiled feasibility check is independent of horizon length for fixed compiled dimensions. We prove nonnegative continuous robustness under a joint controller assumption. On 6D UAV benchmarks, median geometric repair times are 0.265--1.510 ms; we show up to 1.68x10^4 speedup over MILP feasibility checker. All geometric runs pass continuous STL validation, whereas majority of completed MILP control witnesses violate continuous-time STL.

Avinash Malik

Department of Electrical, Computer, and Software Engineering, University of Auckland, Auckland, New Zealand

Reachability Analysis Signal Temporal Logic Formal Verification STL Planning Temporal Logic STL Motion Planning

Aug 30, 2026

Generalizable Multi-Agent Planning from Signal Temporal Logic Specifications via Diffusion

Multi-agent systems in the real-world (e.g., drone swarms, autonomous cars, warehouse robots) must satisfy rich, temporal tasks while avoiding collisions. Signal Temporal Logic (STL) elegantly encodes such objectives, but current STL planning methods face critical limitations. State-of-the-art optimization-based approaches can handle arbitrary STL specifications but struggle with scalability, becoming computationally impractical as the number of agents grows. Learning-based methods efficiently handle a large number of agents with rapid planning times but fare poorly when deployment-time objectives differ from those used during training, and do not support planning tasks that require different specifications to be ascribed to different agents (i.e., heterogeneity) or team-level specifications requiring coordination of multiple agents. This fundamental trade-off between generalizability and scalability presents a challenge for realizing multi-agent STL planning algorithms in practice. To overcome this challenge, we introduce a new diffusion method for multi-agent planning with STL specifications. Using a differentiable approximation of STL, we integrate the STL gradient in the denoising process, making our approach generalizable to novel formulas whose predicates are placed anywhere within the goal region covered during training, while achieving the same scalability as existing learning-based methods. Our method supports heterogeneous specifications, and by using diffusion models, naturally enhances plan diversity, thereby significantly reducing safety-related violations (e.g., collisions) among agents. A detailed evaluation study justifies the utility of STL-guided diffusion-based multi-agent planners for constructing generalizable, scalable, and diverse plans. Videos and code are available at https://www.jeappen.com/diff-ma-stl/ and https://github.com/jeappen/diff-ma-stl .

Joe Eappen, Zikang Xiong, Shreyash S. Iyengar +1

ECE and CS Departments of Purdue University

STL Planning Multi-Agent Planning Diffusion-Based Planning

Aug 25, 2026

Safety-aware Model Predictive Path Integral Control with Signal Temporal Logic

Safety-aware motion planning remains a challenge in robotics, especially when missions are time-critical and are under complex specifications. In this paper, we propose safety-aware-stl-mppi, a computationally efficient sampling-based receding-horizon planning framework designed to promote satisfaction of constraints expressed in Signal Temporal Logic (STL). Our approach encodes discrete-time STL formulas into candidate time-varying control barrier functions (CBF), which are integrated into a model predictive path integral (MPPI) controller. Our method inherits the benefits of low computational cost from an efficiently parallelizable sampling based planner and utilizes CBF for constraints expressed in STL. We compare against several MPPI baselines using four artificial Mars Rover planning case studies with a diverse environment and cost setups, where we show our method consistently achieving high safety and efficiency. We show a quadcopter planning experiment with NVIDIA Isaac Lab.

Yiqi Zhao, Taekyung Kim, Hideki Okamoto +4

Thomas Lord Department of Computer Science, University of Southern California, Los Angeles, CA 90089, USA · Department of Robotics, University of Michigan, Ann Arbor, MI 48109, USA · Toyota Motor North America R&D, Ann Arbor, MI 48105, USA +1

STL Motion Planning Safe Motion Planning Motion Planning Constrained Motion Planning STL Planning MPPI Control+1

Aug 20, 2026

Logic-VLA: A Temporal Logic Conditioned Vision-Language-Action Model

Vision-language-action (VLA) models can follow natural-language (NL) task instructions, but such instructions may not precisely specify safety-critical or spatiotemporal requirements on the resulting behavior. We introduce Logic-VLA, a formal-requirement-aware VLA that conditions on Signal Temporal Logic (STL) specifications supplied at inference time. Logic-VLA uses a syntax-graph-based STL encoder pre-trained to capture temporal logic semantics. Policy adaptation proceeds in two stages: STL-conditioned supervised fine-tuning on satisfying demonstrations is followed by trajectory-level preference optimization over matched satisfying-violating rollout pairs using a flow-matching surrogate for Identity Preference Optimization. This formulation improves formal requirement satisfaction while preserving the nominal NL task. We evaluate Logic-VLA in closed-loop quadcopter navigation simulation across randomized photorealistic environments and test generalization to STL formulas unseen during training. Across the evaluation benchmarks, Logic-VLA improves STL satisfaction rate over an STL-blind base policy by 24.8 to 40.7 percentage points (pp) while reducing nominal NL task success by at most 1.8 pp, showing that a single VLA can adapt its behavior to varying formal requirements without requiring a separate policy for each specification.

Celina Shiyu Wang, Yiqi Zhao, Junjie Ye +2

Thomas Lord Department of Computer Science, University of Southern California

Vision-Language-Action Models Reasoning for VLA Models STL Planning Aerial VLN

Jul 21, 2026

STL-GCS: A Planner-Controller Framework for Signal Temporal Logic via Graphs of Time-varying Convex Sets

We present a unified trajectory planning and control framework for the satisfaction of Signal Temporal Logic (STL) specifications defined over convex predicates. At the planning layer, STL tasks are encoded as time-varying convex sets in configuration space, specifically designed so that forward invariance of the system with respect to these sets implies satisfaction of the specification with a prescribed robustness margin. This representation is then lifted to the joint time--configuration space and combined with the Graphs of Convex Sets (GCS) framework, yielding a shortest-path formulation of the planning problem over convex spatio-temporal sets. Trajectories are parameterized by B-splines, which enable continuous-time enforcement of STL satisfaction, collision avoidance, and smoothness constraints. At the control layer, the same time-varying sets used for planning are exploited to design a feedback controller that tracks the planned trajectory while prioritizing satisfaction of the STL specification during execution in the presence of tracking errors and model mismatch. We validate the proposed approach in simulation and in real-world experiments on space robotic platforms.

Nicola De Carli, Gregorio Marchesini, Dimos V. Dimarogonas

Robot Trajectory Tracking Constrained Motion Planning Signal Temporal Logic STL Planning Robot Motion Planning STL Motion Planning

Jul 21, 2026

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

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.

Jiaheng Dong, Jingyi Huang, Liang Han

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

Signal Temporal Logic Robot Task Planning Behavior Trees STL Planning

Jun 19, 2026

Temporal logics and formal synthesis for robot planning and control

As robots move from controlled environments into real-world settings, it becomes increasingly crucial to ensure that they perform as expected. A key step toward that goal is a rigorous specification of the desired robot behavior, capturing intricate temporal, spatial, and logical requirements. Complementing this, plan and control synthesis methods are needed to fulfill these specifications with provable guarantees. This manuscript presents temporal logics - particularly linear and signal temporal logic - as expressive specification languages for robot behavior over time. We then discuss principles of formal synthesis, from discrete graph- and game-based approaches to sampling-based motion planning, trajectory optimization, and control-certificate-based synthesis. Finally, we outline challenges in deploying formal synthesis in real-world robotics, emphasizing the interplay between modeling fidelity, computational tractability, and the types of rigorous guarantees that can be achieved.

Jana Tumova, Joris Verhagen, Matti Vahs

KTH Royal Institute of Technology

Robotics Signal Temporal Logic Linear Temporal Logic Robotic Control Formal Verification Robot Motion Planning+1

May 22, 2026

Signal Temporal Logic Motion Planning via Graphs of Convex Sets

This paper investigates continuous-time motion planning under Signal Temporal Logic (STL) specifications. The goal is to generate smooth robot trajectories that satisfy high-level logical and timing requirements while respecting low-level motion constraints. To this end, we propose an efficient framework that combines timed-automata reasoning with graphs of convex sets (GCS). An STL specification is first represented by a timed automaton, which is then coupled with a convex decomposition of the configuration space to form a joint transition system encoding both task progress and region occupancy. Based on this joint transition system, the STL motion-planning problem is reformulated as a shortest-path problem over a GCS, whose solution induces a smooth Bézier-spline trajectory satisfying the STL specification, smoothness requirements, and velocity bounds. We establish the soundness of the proposed formulation and analyze its computational complexity, showing that, once the timed automaton and convex decomposition are fixed, the convex relaxation scales polynomially with the configuration-space dimension and the Bézier degree. We further develop a compact timed-automaton construction for an expressive STL fragment using dedicated templates and Boolean composition. Numerical experiments on low-dimensional benchmarks, a

3

-D quadrotor, 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 and produces smooth executable trajectories.

Yu Chen, Ancheng Hou, Mingyang Feng +2

School of Automation & Intelligent Sensing, Shanghai Jiao Tong University, Shanghai 200240, China · Institute of Artificial Intelligence, Xiamen University, Xiamen, China

Constrained Motion Planning Trajectory Generation STL Motion Planning Motion Planning Robot Motion Planning STL Planning

May 5, 2026

Feasibility-aware Hybrid Control for Motion Planning under Signal Temporal Logics

In this work, a novel method for planar task and motion planning based on hybrid modeling is proposed. By virtue of a discrete variable which models local constraint satisfaction and enables local feasibility analysis, the proposed control architecture unifies planning with control design. Concurrently, control barrier functions are designed on a transformed disk version of the original nonconvex and geometrically complex robotic workspace, thus amending the issue of deadlocks. Simulations of the proposed method indicate effective handling of multiple overlapping spatio-temporal tasks even in the face of input saturation.

Panagiotis Rousseas, Dimos V. Dimarogonas

∗KTH Royal Institute of Technology, School of Electrical Engineering and Computer Science, Division of Decision and Control Systems

Constrained Motion Planning Signal Temporal Logic STL Planning Feedback Control Robot Motion Planning Safe Motion Planning+2

May 4, 2026

Feedback Motion Planning for Stochastic Nonlinear Systems with Signal Temporal Logic Specifications

We study feedback motion planning for continuous-time stochastic nonlinear systems under signal temporal logic (STL) specifications. We propose a framework that synthesizes control policies for chance-constrained STL trajectory optimization problems, with the goal of ensuring that the closed-loop stochastic system satisfies a given STL formula with high probability (e.g., 99.99%). Our approach is based on a predicate erosion strategy that transforms the intractable stochastic problem into a deterministic STL trajectory optimization problem with tightened STL formula constraints. The amount of erosion is determined by a probabilistic reachable tube (PRT) that bounds the deviation between the stochastic trajectory and an associated nominal trajectory. To compute such bounds, we leverage contraction theory and feedback design, and develop several tracking controllers. This yields a complete feedback motion planning pipeline which can be implemented by numerical optimizations. We demonstrate the efficacy and versatility of the proposed framework through simulations on several robotic systems and through experiments on a real-world quadrupedal robot, and show that it is less conservative and achieves higher specification satisfaction probability than representative baselines.

Liqian Ma, Zishun Liu, Glen Chou +1

Georgia Institute of Technology, Atlanta, GA 30332

Constrained Motion Planning Trajectory Optimization Contraction Theory Stochastic Optimal Control Robot Motion Planning STL Motion Planning+2

May 2, 2026

Zero-Shot Signal Temporal Logic Planning with Disjunctive Branch Selection in Dynamic Semantic Maps

Signal Temporal Logic (STL) offers verifiable task specifications and is crucial for safety-critical control. Yet STL planning remains challenging: exact optimization-based methods are often too slow, and learning-based methods struggle to generalize across varying environments. We propose a zero-shot STL planning solver for variable-map environments that generates feasible trajectories without retraining. By integrating a map-conditioned Transformer architecture with a lightweight heuristic, our approach effectively handles complex disjunctive (OR) subformulas. Furthermore, we leverage Transitive Reinforcement Learning (TRL) to ensure consistent temporal grounding and logical coherence across decomposed sub-tasks. Experiments on dynamic semantic maps with diverse obstacle layouts demonstrate consistent gains, highlighting the framework's superior zero-shot generalization to changing environments and broad STL coverage.

Bowen Ye, Ancheng Hou, Junyue Huang +2

School of Automation and Intelligent Sensing, Shanghai Jiao Tong University, and the Key Laboratory of System Control and Information Processing, the Ministry of Education of China, Shanghai 200240, China

STL Planning Robot Task Planning

Apr 20, 2026

DAG-STL: A Hierarchical Framework for Zero-Shot Trajectory Planning under Signal Temporal Logic Specifications

Signal Temporal Logic (STL) is a powerful language for specifying temporally structured robotic tasks. Planning executable trajectories under STL constraints remains difficult when system dynamics and environment structure are not analytically available. Existing methods typically either assume explicit models or learn task-specific behaviors, limiting zero-shot generalization to unseen STL tasks. In this work, we study offline STL planning under unknown dynamics using only task-agnostic trajectory data. Our central design philosophy is to separate logical reasoning from trajectory realization. We instantiate this idea in DAG-STL, a hierarchical framework that converts long-horizon STL planning into three stages. It first decomposes an STL formula into reachability and invariance progress conditions linked by shared timing constraints. It then allocates timed waypoints using learned reachability-time estimates. Finally, it synthesizes trajectories between these waypoints with a diffusion-based generator. This decomposition--allocation--generation pipeline reduces global planning to shorter, better-supported subproblems. To bridge the gap between planning-level correctness and execution-level feasibility, we further introduce a rollout-free dynamic consistency metric, an anytime refinement search procedure for improving multiple allocation hypotheses under finite budgets, and a hierarchical online replanning mechanism for execution-time recovery. Experiments in Maze2D, OGBench AntMaze, and the Cube domain show that DAG-STL substantially outperforms direct robustness-guided diffusion on complex long-horizon STL tasks and generalizes across navigation and manipulation settings. In a custom environment with an optimization-based reference, DAG-STL recovers most model-solvable tasks while retaining a clear computational advantage over direct optimization based on the explicit system model.

Ruijia Liu, Ancheng Hou, Xiao Yu +1

School of Automation and Intelligent Sensing, Shanghai Jiao Tong University, Shanghai, China. · Institute of Artificial Intelligence, Xiamen University, Xiamen, China.

Constrained Motion Planning Trajectory Generation STL Planning Robot Motion Planning STL Motion Planning

Mar 31, 2026

GraSP-STL: A Graph-Based Framework for Zero-Shot Signal Temporal Logic Planning via Offline Goal-Conditioned Reinforcement Learning

This paper studies offline, zero-shot planning under Signal Temporal Logic (STL) specifications. We assume access only to an offline dataset of state-action-state transitions collected by a task-agnostic behavior policy, with no analytical dynamics model, no further environment interaction, and no task-specific retraining. The objective is to synthesize a control strategy whose resulting trajectory satisfies an arbitrary unseen STL specification. To this end, we propose GraSP-STL, a graph-search-based framework for zero-shot STL planning from offline trajectories. The method learns a goal-conditioned value function from offline data and uses it to induce a finite-horizon reachability metric over the state space. Based on this metric, it constructs a directed graph abstraction whose nodes represent representative states and whose edges encode feasible short-horizon transitions. Planning is then formulated as a graph search over waypoint sequences, evaluated using arithmetic-geometric mean robustness and its interval semantics, and executed by a learned goal-conditioned policy. The proposed framework separates reusable reachability learning from task-conditioned planning, enabling zero-shot generalization to unseen STL tasks and long-horizon planning through the composition of short-horizon behaviors from offline data. Experimental results demonstrate its effectiveness on a range of offline STL planning tasks.

Ancheng Hou, Ruijia Liu, Xiang Yin

School of Automation & Intelligent Sensing, Shanghai Jiao Tong University, Shanghai 200240, China.

STL Planning Graph-Based Planning Offline RL

Feb 19, 2026

Multi-Agent Temporal Logic Planning via Penalty Functions and Block-Coordinate Optimization

Multi-agent planning under Signal Temporal Logic (STL) is often hindered by collaborative tasks that lead to computational challenges due to the inherent high dimensionality of the problem, preventing scalable synthesis with satisfaction guarantees. To address this, we formulate STL planning as an optimization program under multi-agent STL constraints and introduce a penalty-based unconstrained relaxation that can be efficiently solved via a Block-Coordinate Gradient Descent (BCGD) method, where each block corresponds to a single agent's decision variables, thereby mitigating complexity. By utilizing a quadratic penalty function defined via smooth STL semantics, we show that BCGD iterations converge to a stationary point of the penalized problem under standard regularity assumptions. To enforce feasibility, the BCGD solver is embedded within a two-layer optimization scheme: inner BCGD updates are performed for a fixed penalty parameter, which is then increased in an outer loop to progressively improve multi-agent STL robustness. The proposed framework enables scalable computations and is validated through various complex multi-robot planning scenarios.

Eleftherios E. Vlahakis, Arash Bahari Kordabad, Lars Lindemann +3

the Division of Computer Engineering and Computer Science, University West, 46132, Trollhättan, Sweden · the Max Planck Institute for Software Systems, Kaiserslautern, Germany · the Automatic Control Laboratory, ETH Zürich, 8092, Zürich, Switzerland +2

STL Planning Multi-Agent Planning Multi-Robot Motion Planning Constrained Optimization