Signal Temporal Logic

Also known as STL

Ask about this topic

Overview

Signal Temporal Logic expresses requirements about how signals should behave over time, such as reaching a region within a deadline or avoiding hazards until a task is complete. Researchers use quantitative robustness scores, differentiable monitors, automata, and mixed-integer or reachability methods to learn specifications and synthesize or verify plans and controllers. Language models and vision systems are also being connected to STL so people can describe tasks in natural language or video and obtain inspectable formal requirements. A central challenge is balancing expressive specifications and reliable guarantees with computational cost, especially for continuous-time behavior, uncertainty, and imperfect translations.

Latest papers

CardsList

34 papers4 papers in the last four weeks, down 20% on the four weeks before. 0.0% of all new papers.

Nov 1, 2026

Beyond Ensemble Disagreement: Predictive STL Monitoring of RL Locomotion under Distribution Shift

RL locomotion policies trained under nominal simulation conditions may encounter distribution shifts that compromise safety. Predictive monitors could anticipate violations, but their world-model forecasts may become unreliable under shift, and ensemble disagreement is not calibrated. We evaluate predictive Signal Temporal Logic (STL) monitoring for frozen Ant-v5 and HalfCheetah-v5 policies using closed-loop world-model rollouts and a three-model ensemble. Across external-force, observation-noise, and mass shifts, predicted robustness ranks HalfCheetah's future STL violations strongly, whereas disagreement does not reliably track observation prediction error or violations. Under severe noise, violations remain common (64.2±24.4%64.2\pm24.4\% at K=20K{=}20 across three PPO seeds), yet current-state robustness without prediction comes within 0.030.03 AUROC of predictive robustness. Penalizing predicted robustness by disagreement does not consistently improve ranking. Ant provides complementary per-specification evidence, but its composite target has no positive violations and its any-violation target is single-class in most evaluated seed-condition slices. Overall, predictive robustness provides useful STL-specific ranking but little demonstrated additional ranking value over the current state; these findings caution against treating ensemble disagreement as a reliable indicator of safety uncertainty.

Qurban Ali, Badaruddin Chachar, Maqsood Ali +1

Sindh Madressatul Islam University, Karachi, Pakistan · Shah Abdul Latif University, Ghotki, Pakistan · University of Camerino, Camerino, Italy +2

Safe RLRobotic Policy EvaluationUncertainty Estimation in RLSignal Temporal LogicRobust RL
AskPDF
Oct 16, 2026

SparseMax-dSTL: Sound Robustness with Horizon-Independent Gradient Allocation for Temporal Logic Trajectory Optimization

A gradient-based solver that enforces a Signal Temporal Logic (STL) specification uses a smooth approximation of its quantitative semantics, the robustness. In safety-critical trajectory optimization, this approximation must have two properties. First, it must be sound, that is, nonnegative only on trajectories that satisfy the specification. Second, at each temporal operator, the weight of its gradient on the violating samples must stay bounded away from zero, however long the horizon. The approximations in use, including the log-sum-exp, its sound variant, and the generalized-mean robustness, do not have both. We introduce lower approximations of the minimum and the maximum whose gradients are sparsemax projections, and we prove that the robustness built from them has both. It lies below the exact robustness and is therefore sound, and its error has a bound that is independent of the number of samples and known before optimization. The gradient of each approximation is exactly zero on every sample beyond a data-dependent threshold, so the weight on violating samples a gap beyond the others has a positive lower bound at every horizon. On a planar unicycle and on a seven-joint manipulator beside a person in simulation, the log-sum-exp approximation is positive on a violating trajectory. As the horizon of the manipulator's task grows from 10 to 80 s, the gradient weight of the sound variant on the violating samples falls from 0.22 to 0.04, while that of sparsemax stays at 1. In a constrained trajectory optimization of the unicycle, the constraint on the log-sum-exp robustness returns a violating trajectory, whereas the constraint on the sparsemax robustness returns a trajectory that satisfies the specification with the required margin.

Sai Sandeep Damera, Ryan Matheu, John S. Baras +1

The authors are with the University of Maryland, College Park, USA.

STL Motion PlanningSignal Temporal LogicTrajectory Optimization
AskPDF
Oct 9, 2026

Class-Conditional Conformal Prediction for Signal Temporal Logic Inference with Many Classes

Signal Temporal Logic (STL) inference provides interpretable formulas for time series classification. For multiclass classification, however, accurate predictions do not necessarily ensure that the inferred formulas are satisfied consistently with the true class. We introduce the positive satisfaction rate and codeword satisfaction rate to quantify satisfaction of required formulas and consistency with the complete class codeword, respectively. We develop a two-stage procedure that first learns discriminative formulas using a margin-based objective and then refines predicate thresholds toward a small positive robustness target while fixing the formula structure and temporal intervals. Satisfaction and ranking penalties discourage violations of required formulas and loss of class separation. The decoding loss is used as a nonconformity score and calibrated separately for each class, providing finite-sample class-conditional coverage under intra-class exchangeability. Experiments on naval, synthetic, and robot manipulation trajectories demonstrate discrepancies between classification accuracy and formula satisfaction. The results further reveal a data-dependent tradeoff between robustness tightness and satisfaction, while class-conditional calibration mitigates undercoverage that can be hidden by pooled calibration.

Yixuan Wang, Danyang Li, Matthew Cleaveland +2

Mechanical Engineering, University of California, Riverside, CA 92521, USA · Mechanical Engineering, Boston University · MIT Lincoln Laboratory, Lexington, MA 02421, USA

Signal Temporal LogicMultivariate Time Series ClassificationGroup-Conditional Conformal Prediction
AskPDF
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 LogicSTL Planning
AskPDF
Sep 29, 2026

Video2STL: Grounding VLM-Generated Temporal Specifications for Robot Learning

Video-based policy learning is particularly promising, as it illustrates target behaviors without requiring action annotations or embodiment-matched demonstrations. A central challenge is deciding what information should be transferred from the video to the robot. Existing approaches commonly convert visual observations into scalar similarity or value signals, or ask foundation models to directly generate reward code. These approaches can make the temporal structure of a task difficult to inspect, ground, and reuse. We present Video2STL, a framework that converts observation-only videos into parametric Signal Temporal Logic (STL) specifications and uses the resulting formal representation for robot learning. A vision-language model extracts an embodiment-independent semantic event trace and constructs a bank of symbolic temporal specifications. The model determines the task structure, while numerical predicate thresholds and temporal bounds are grounded from successful robot trajectories. For policy learning, we separate short- and long-timescale temporal information: short-horizon specifications provide dense rewards through rolling-window quantitative robustness, while a causal monitor over a retained long-horizon specification provides one-time progress rewards for valid temporal prefixes. The same representation supports cross-embodiment transfer from human or animal videos to robot control. Across four manipulation tasks, Video2STL achieves 85.8%85.8\% average success-once and 67.0%67.0\% success-at-end, compared with 81.5%/59.5%81.5\%/59.5\% for native dense PPO and 65.0%/42.3%65.0\%/42.3\% for Text2Reward; in quadruped locomotion, Qwen-3.8 and GPT-5.6-based Video2STL policies achieve 100%100\% success across velocities from 0.30.3 to 2.1 m/s2.1\,\mathrm{m/s} while remaining competitive in high-speed energy efficiency. Project webpage: video2stl.

Merve Atasever, Keyan Azbijari, Cagan Bakirci +6

Department of Computer Science, University of Southern California Los Angeles, CA, USA · University of Florida Gainesville, FL, USA

VLMs for RoboticsSignal Temporal LogicCross-Embodiment Robot LearningRobot Policy LearningPolicy LearningRobot Learning+1
AskPDF
Sep 27, 2026

Feedback Makes Perfect: A Closed-Loop Framework for NL-to-STL Translation

Signal Temporal Logic (STL) enables rigorous verification and control of cyber-physical systems, but writing correct specifications requires expertise that most requirement holders lack. Large language models can translate natural-language (NL) requirements into STL, yet stronger translators alone approach an accuracy ceiling. We argue that this ceiling stems from how the task is posed: one-shot, open-loop translation is somewhat ill-defined. Natural language is ambiguous, and, more fundamentally, what a person writes may not always be what they intend, so the target specification is not fully contained in the input text. We therefore reformulate NL-to-STL translation as a closed-loop feedback process. Each generated formula is translated back into natural language for the user to check, and natural-language corrections drive revision until the user accepts the specification. Users never read or write formal syntax. This framework rests on an asymmetry familiar from feedback control theory. The forward path, from ambiguous language to formal logic, is hard and error-prone. The feedback path, from structured STL back to language, can be made highly precise, and a precise feedback path lets an imprecise forward path achieve precise closed-loop behavior. Experiments on 500 expert-authored requirements and seven LLMs support this view. Back-translated explanations agree with expert judgments in 99.5% of cases. Closed-loop refinement raises strong models from about 89% open-loop accuracy to 98.0--99.2%, and yields gains of over 30 percentage points for weaker models (e.g., 17.6%→\rightarrow48.0%). Ablations show these gains come from the semantic content of the feedback rather than from repeated attempts. An expert audit and a 280-session user study further confirm the reliability of the loop. We also identify a capability threshold above which feedback no longer helps.

Bowen Ye, Xiang Yin

Shanghai Jiao Tong University Shanghai, China

Signal Temporal LogicLLM Reliability
AskPDF
Sep 23, 2026

Tractable Reinforcement Learning for Full Class of Signal Temporal Logic Specifications Using Spatiotemporal Tube Reward

This paper addresses the control problem for robotic systems, including non-holonomic and underactuated platforms operating under unknown dynamics and strict actuator limits to satisfy complex high-level specifications. We denote these high-level specifications using Signal Temporal Logic (STL) and propose a novel time-aware Reinforcement Learning (RL) framework that leverages the geometric properties of Spatiotemporal Tubes (STTs). While traditional analytical STT controllers often struggle to enforce input constraints, and existing RL approaches rely on memory-intensive state history, our method natively overcomes both limitations. By mapping the logical and temporal complexities of the full class of STL into time-varying geometric boundaries, we directly constrain the multidimensional system state without relying on scalar robustness metrics. Augmenting the state space with time, we train a time-aware Soft Actor-Critic (SAC) agent using a continuous, geometry-aware reward function that eliminates the need to explicitly evaluate complex logical semantics during execution. The proposed framework offers a history-free, computationally efficient approach to learn continuous control policies that ensure robust satisfaction of specifications while strictly adhering to system input constraints.

Vaishnavi Jagabathula, P Sangeerth, Pushpak Jagtap

Centre for Cyber-Physical Systems, IISc, Bangalore, India

Robotic RLReinforcement LearningConstrained RLSignal Temporal Logic
AskPDF
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 AnalysisSignal Temporal LogicFormal VerificationSTL PlanningTemporal LogicSTL Motion Planning
AskPDF
Sep 8, 2026

Fast Constraint Extraction for Corrective Control under STL Specifications via Logical Dependency Tracking

Ensuring the satisfaction of Signal Temporal Logic (STL) specifications under uncertainty is challenging, as reachability-based monitoring provides guarantees but does not indicate how to restore satisfaction when it becomes indeterminate. A key difficulty is identifying which uncertain components actually affect global satisfaction, especially for nested formulas. This paper introduces a logical dependency tracking framework that propagates uncertainty through the STL structure and captures the causal contribution of reachable sets to satisfaction. By associating markers to uncertain predicates and propagating them via three-valued semantics, we extract in milliseconds a compact Disjunctive Normal Form (DNF) of sufficient constraints, avoiding combinatorial enumeration. As an application, we formulate control correction as a minimum-effort optimization problem. Using zonotopic reachability, the derived constraints are enforced via linear programming, yielding corrections that guarantee STL satisfaction under bounded uncertainty and provide certified probabilistic bounds in the stochastic case. We demonstrate the approach on a nonlinear system with nested STL specifications, showing that dependency tracking enables efficient and formally guaranteed correction. The tracking implementation is available at https://github.com/Antoine-Bst/STL-Three-Valued-Clause-Filtering/.

Antoine Besset, Joris Tillet, Chuchu Fan +1

u2IS, ENSTA, Institut Polytechnique de Paris, France · Univ. Grenoble Alpes, CNRS, Grenoble INP, VERIMAG, France · REALM, AeroAstro, Massachusetts Institute of Technology, Cambridge, USA

Signal Temporal LogicRobust ControlFormal Verification
AskPDF
Aug 13, 2026

Reward Machines for Signal Temporal Logic

Signal temporal logic (STL) provides a formal language for specifying real-time properties of real-valued observations, along with a quantitative robustness score for monitoring satisfaction. Control synthesis from STL specifications is of interest since manual controller design becomes infeasible as real-world systems grow in complexity. Moreover, many modern autonomous and AI-enabled systems lack accurate and complete system models, which makes optimization-based synthesis approaches unsuitable and motivates learning-based control. Prior work uses STL robustness scores as rewards in reinforcement learning (RL) to obtain control policies satisfying given specifications; however, robustness depends on execution history, leading to intractable state space expansion for general long-horizon specifications with arbitrarily nested temporal operators. This work introduces a novel automata-based approach that provides an efficient memory mechanism and associated Markovian rewards suitable for RL frameworks. Our approach constructs a timed alternating automaton from the given STL specifications, augments the state space with automaton locations and clock valuations, and derives rewards from the automaton acceptance condition. We empirically demonstrate that our approach learns policies that achieve higher robustness scores and satisfaction rates than those learned by existing approaches using robustness-based rewards.

Alper Kamil Bozkurt, Shangtong Zhang, Yuichi Motai

Department of Computer Science, University of Virginia, Charlottesville, VA, USA

Reward MachinesReward Design for RLRL ControlSignal Temporal LogicReinforcement Learning
AskPDF
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 TrackingConstrained Motion PlanningSignal Temporal LogicSTL PlanningRobot Motion PlanningSTL Motion Planning
AskPDF
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 LogicRobot Task PlanningBehavior TreesSTL Planning
AskPDF
Jul 9, 2026

Learning-enabled Parameter Synthesis for Nonlinear Systems from Signal Temporal Logic

Signal Temporal Logic (STL) is increasingly used to describe interpretable objectives and constraints for optimal control and learning methods, especially when no target time series data is available. In this work, we propose to synthesize parameters for nonlinear systems that robustly satisfy continuous-time STL specifications for uncertain initial conditions. To this end, we use gradient-based optimization along with set-based reachability verification to efficiently learn in high-dimensional parameter spaces while providing provable satisfaction guarantees for the optimized parameters. We demonstrate the effectiveness and scalability of our method on three systems with up to 18 parameter dimensions.

Alex Beaudin, Hanna Krasowski, Eric Palanques-Tost +2

University of California, Berkeley · Boston University · University of Maryland, College Park

Signal Temporal LogicRobust Control
AskPDF
Jul 8, 2026

Learning Spatiotemporal Tubes for Full Class of Signal Temporal Logic Tasks for Control of Unknown Systems under Input Constraints

This paper presents a Spatiotemporal Tube (STT)-based control framework for general unknown nonlinear Euler-Lagrange (EL) systems subject to input constraints, with the objective of satisfying Signal Temporal Logic (STL) specifications, where confinement of the system trajectory within the STT guarantees the satisfaction of the corresponding STL task. For both single and multi-agent scenarios, the STT corresponding to each agent is modeled as a time-varying ball, whose center and radius are jointly parameterized using a physics-informed neural network (PINN). The robustness metric associated with the STL specification corresponding to the agents is incorporated into the training process as a loss function, enabling the learned tube to encode task-level temporal requirements. For a multi-agent scenario, we introduce an additional robustness metric corresponding to the global task, which, when satisfied, ensures the tubes do not collide with each other. To ensure that the system trajectory remains within the learned STT and thereby satisfies the local and global STL specifications, we propose a control strategy that explicitly accounts for input constraints. In particular, a closed-form control law is developed to keep the trajectory inside the tube while regulating the motion of the tube by enforcing bounds on its evolution depending on the input constraints of the system. The proposed approach has been validated over several case studies.

Ahan Basu, Ratnangshu Das, Soumyodipta Nath +2

Centre for Cyber-Physical Systems Indian Institute of Science, Bengaluru, India · Electrical Engineering Department, Eindhoven Institute of Technology, Netherlands

Signal Temporal LogicMulti-Agent ControlFeedback Control
AskPDF
Jul 7, 2026

EvoPlan: Evolutionary Neuro-Symbolic Robot Planning with Spatio-Temporal Guarantees

LLM-based robot planners are fluent but cannot guarantee that their plans are executable or safe. Classical PDDL planners can guarantee symbolic validity, but only once the problem is fully specified, and they make poor use of an LLM's ability to read context and repair plans. We present EvoPlan, a neuro-symbolic framework whose guarantees are symbolic validity and satisfaction of a constraint learned from data. The planner works with locally-hosted open-weight models, so it does not require a cloud service. EvoPlan has three parts. First, an offline procedure that mines a single global Signal Temporal Logic (STL) mobility constraint from demonstrations. Perturbed demonstrations supply the missing negatives without encoding any rule, and evolutionary search fits the constraint, which captures driving rules or social-navigation preferences within a modelled taxonomy of norms. We use the mined constraint to shield driving and navigation policies on Bench2Drive and HA-VLN-CE. Second, an evolutionary PDDL planner: an LLM proposes and repairs plans, programmatic validators decide which ones survive, and the validated portion of the plan grows over iterations. On open-world ALFWorld and NL-PDDL Blocksworld, it approaches classical planning when the goal vocabulary agrees with the action model, and it stays robust when the two disagree and classical planning fails. Third, a constrained execution loop: Nav2 uses the costmap to ground the plan into waypoints, which are checked against the mined constraint. Violations and execution failures update the PDDL problem for re-planning. We demonstrate the full pipeline in Gazebo and on a Clearpath Jackal robot. More details and videos are on the project page: https://nbhavyasai.github.io/evoplan/

Bhavya Sai Nukapotula, Samin Moosavi, Haoze Wang +4

Texas A&M University · Student at Westwood High School; work done as an intern at Texas A&M University.

Neuro-Symbolic ReasoningLarge Language Model-Based Robot PlanningConstrained Motion PlanningSignal Temporal LogicRobot SafetyRobot Task Planning+2
AskPDF
Jun 25, 2026

An Algebraic Framework for Quantitative Semantics of Spatio-Temporal Logic with Graph Operators

Spatio-Temporal Logic with Graph Operators (STL-GO) extends Signal Temporal Logic (STL) to multi-agent systems via graph operators that count neighboring agents satisfying a property, together with multi-agent quantifiers. While Boolean semantics for STL-GO are well-defined, quantitative semantics have not yet been developed and existing quantitative semantics for spatio-temporal logics such as STREL cannot capture the counting constraints in STL-GO's graph operators. We develop quantitative semantics for STL-GO as a layered algebraic construction that separates temporal aggregation from graph-operator aggregation (governed by an abstract accumulator with a monotone fold and readout). We prove that soundness and completeness reduce to monotonicity conditions on these components. We implement the framework and evaluate it on two multi-agent environments: a 2D bounded region with stochastic Dubins-car dynamics and a 3D Earth-satellite system, under four semantic instantiations (Boolean, min-max, signed-deficit, and a hybrid), demonstrating the tradeoffs between accumulator choices and reporting scalability in the number of agents and time horizon.

Sheryl Paul, Vidisha Kudalkar, Anand Balakrishnan +3

University of Southern California, Los Angeles, CA, USA · University of Texas at Austin, Austin, TX, USA · ETH Zürich, Zürich, Switzerland

Signal Temporal LogicMulti-Agent SystemsTemporal Logic
AskPDF
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

RoboticsSignal Temporal LogicLinear Temporal LogicRobotic ControlFormal VerificationRobot Motion Planning+1
AskPDF
Jun 17, 2026

pdSTL: Probabilistic Differentiable Signal Temporal Logic for Stochastic Systems

Autonomous robots operating in uncertain environments must satisfy complex temporal and safety specifications despite stochastic dynamics and sensing noise. While Signal Temporal Logic (STL) offers robustness measures for gradient-based optimization, existing extensions either lack differentiability or ignore belief-space uncertainty. We introduce pdSTL (probabilistic differentiable Signal Temporal Logic), a framework that unifies probabilistic semantics with differentiable robustness over belief trajectories. pdSTL employs interval-valued probabilistic semantics to compute conservative satisfaction bounds, propagated compositionally through the STL syntax tree. We formulate the temporal robustness evaluation as a recurrent, LSTM-style unfolding of STL operators, enabling linear-time, differentiable monitoring suitable for end-to-end trajectory optimization. We validate pdSTL on simulated obstacle avoidance, lane-change maneuvers, and real-world Crazyflie quadcopter flight experiments under aerodynamic disturbances. Results demonstrate that pdSTL achieves efficient optimization with formal probabilistic guarantees, significantly outperforming deterministic differentiable STL in maintaining safety margins under real-world uncertainty.

Bennett Dogbey, Hemanth Manjunatha

Dept. of Mechanical and Aerospace Engineering, Oklahoma State University, Stillwater, OK USA

Signal Temporal LogicSafe Robot Navigation
AskPDF
May 27, 2026

An Operator-Based Approach to STL

Signal Temporal Logic (STL), has recently seen extensive development, owing to its rich expressivenes for autonomous planning and control. Nevertheless, existing verification and control synthesis methods are limited with respect to the complexity and degree of nesting of the formulae. In this work, we propose a novel approach to STL based on an operator acting on reachability value functions. This constitutes a new theoretical framework for handling complex multi-nested formulae while at the same time providing tools for on-line control synthesis. In contrast to focusing on the design of STL-based reachability (or control barrier) functions, we develop operator-based nesting rules directly. Our method's expressiveness is demonstrated both theoretically, where necessary and sufficient conditions for STL formula satisfaction are extracted, as well as in simulations with complex fragments.

Panagiotis Rousseas, Dimos V. Dimarogonas

Department of Decision and Control Systems, School of Electrical Engineering and Computer Science, Royal Institute of Technology KTH, Sweden.

Signal Temporal LogicFormal Verification
AskPDF
May 23, 2026

On the Stability and Realizability of Recurrent Polynomial Surrogate Ternary Logic Gate Networks

Recurrent Neural Networks (RNNs) can learn to predict Signal Temporal Logic (STL) verdicts online from partial trajectories, but deploying them as runtime monitors in safety-critical systems demands more than predictive accuracy. Standard RNN architectures offer no structural guarantee that outputs degrade gracefully under sensor degradation; a dropped input can silently flip a verdict from safe to unsafe. We introduce the Recurrent Differentiable Ternary Logic Gate Network (R-DTLGN), a recurrent architecture that operates over Kleene's three-valued logic {−1,0,+1}\{-1, 0, +1\}, where 00 explicitly represents unknown. The R-DTLGN trains through continuous polynomial surrogates and hardens to a discrete ternary logic circuit at inference. We analyze the hardened circuit through two gate vocabularies derived from two orderings on the ternary domain: numerically monotone gates ensure stable recurrent dynamics, while information-monotone gates, when present, guarantee principled abstention (unknown inputs never produce wrong outputs) and monotonicity in input certainty (more information can only improve the verdict). We show that the recurrent connections required by bounded STL operators use exclusively AND and OR, which belong to both vocabularies, linking the monitoring task to the architecture's guarantees. A realizability bound derived from the STL formula's temporal operators directly sizes the network's hidden state, replacing hyperparameter search with a formula-driven specification. We evaluate on STL specifications over D4RL PointMaze navigation data, testing prediction accuracy, degradation under predicate dropout, and the accuracy-versus-safety tradeoff between two label construction pipelines. The R-DTLGN is, to our knowledge, the first recurrent architecture that couples learned temporal prediction with formal degradation guarantees rooted in three-valued logic.

Sai Sandeep Damera, Ryan Matheu, Aniruddh G. Puranic +2

University of Maryland, College Park, USA

Logical ReasoningSignal Temporal LogicRecurrent Neural NetworksRuntime VerificationDifferentiable Logic Gate Networks
AskPDF
May 13, 2026

Vision-Based Runtime Monitoring under Varying Specifications using Semantic Latent Representations

We study certified runtime monitoring of past-time signal temporal logic (ptSTL) from visual observations under partial observability. The monitor must infer safety-relevant quantities from images and provide finite-sample guarantees, while being reusable: once trained and calibrated, it should certify any formula in a target fragment without per-formula retraining. For fragments induced by a finite dictionary of temporal atoms, we prove that the semantic basis, the vector of atom robustness scores, is the minimum prediction target within the class of monotone, 1-Lipschitz reusable interfaces: any formula is evaluated by a deterministic decoder derived from the parse tree, and a single conformal calibration pass certifies the entire fragment with no union bound. We also introduce a rolling prediction monitor that predicts only current predicate values and reconstructs temporal history online; this is easier to learn but grows conservative at long horizons. On a pedestrian-crossroad benchmark, rolling achieves tighter certified bounds at short horizons while the semantic-basis monitor is up to 4-times tighter at long horizons. We validate the presented monitors on real-world Waymo driving data, where both monitors satisfy the conformal coverage guarantee empirically.

Bardh Hoxha, Oliver Schön, Hideki Okamoto +2

Toyota NA R&D · ETH Zürich

Signal Temporal LogicConformal Prediction
AskPDF
May 12, 2026

Runtime Monitoring of Perception-Based Autonomous Systems via Embedding Temporal Logic

Runtime monitoring of autonomous systems traditionally relies on mapping continuous sensor observations to discrete logical propositions defined over low-dimensional state variables. This abstraction breaks down in perception-driven settings, where such mappings require additional learned modules that are often computationally expensive, brittle, and semantically misaligned. In this work, we propose Embedding Temporal Logic (ETL), a temporal logic that performs monitoring directly in learned embedding spaces. ETL defines predicates through distances between observed embeddings and target embeddings derived from reference observations. This formulation allows specifications to capture high-level perceptual concepts, such as similarity to visual goals or avoidance of semantic regions, that are difficult or impossible to express using traditional predicates. By composing these predicates with temporal operators, ETL naturally expresses temporally extended and sequential perceptual behaviors. We introduce ETL monitors for evaluating specifications over bounded embedding traces, along with a conformal calibration procedure that provides reliable and safety-oriented predicate evaluation. We evaluate our approach across multiple manipulation environments to show that ETL achieves strong empirical agreement with ground-truth semantics, including accurate monitoring of temporally composed behaviors.

Parv Kapoor, Abigail Hammer, Ashish Kapoor +2

Software and Societal Systems Department Carnegie Mellon University · General Robotics · Aeronautics and Astronautics Department University of Washington

Signal Temporal LogicAI Agent Monitoring
AskPDF
May 7, 2026

ReasonSTL: Bridging Natural Language and Signal Temporal Logic via Tool-Augmented Process-Rewarded Learning

Signal Temporal Logic (STL) is an expressive formal language for specifying spatio-temporal requirements over real-valued, real-time signals. It has been widely used for the verification and synthesis of autonomous systems and cyber-physical systems. In practice, however, users often express their requirements in natural language rather than in structured STL formulas, making natural-language-to-STL translation a critical yet challenging task. Manual specification requires temporal-logic expertise and cannot scale, while prompting commercial LLM APIs incurs substantial token costs and may expose sensitive system requirements to third-party services, raising privacy concerns for industrial deployment. To address these challenges, we present ReasonSTL, a tool-augmented framework that adapts local open-source language models for natural-language-to-STL generation. ReasonSTL decomposes the translation process into explicit reasoning, deterministic tool calls, and structured formula construction. We further introduce process-rewarded training to supervise both tool-use trajectories and final formulas, together with STL-Bench, a bilingual, computation-aware benchmark grounded in real-world signals. Experiments show that a 4B model trained with ReasonSTL achieves state-of-the-art performance in both automatic metrics and human evaluations, demonstrating that ReasonSTL provides a transparent, low-cost, and privacy-preserving alternative for formal specification drafting.

Bowen Ye, Zhijian Li, Junyue Huang +2

Shanghai Jiao Tong University · Alibaba Group, Hangzhou, China

Signal Temporal LogicLLM Tool Use
AskPDF
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 PlanningSignal Temporal LogicSTL PlanningFeedback ControlRobot Motion PlanningSafe Motion Planning+2
AskPDF
Apr 27, 2026

Logic of Fuzzy Paths

We introduce a new family of temporal logics intended for specifications in motion planning (MP). It builds upon the signal temporal logic (STL), which is a linear-time logic over real-valued signals that possess quantitative semantics and thus became popular in the areas of cyber-physical systems, robotics, and specifically robot MP. However, in contrast to STL, the proposed logic works with paths as first-class citizens, separating the concerns of geometry and of logic. This in turn leads to simpler and more understandable formulae, and a more refined notion of satisfaction being able to reflect also preferences over behaviours. Technically, the logic is built on fuzzy, time-varying signal constraints. As a consequence of this expressivity, it is (i) more usable for human-given specifications in MP and (ii) more amenable to learning specifications from demonstrations than other logics. The former is important for the traditional style of verification in robot MP; the latter is becoming recognized as crucial for mining data-given tasks and controller synthesis in human-aware MP. We expose the advantages of our proposed logic on examples and show the versatility and flexibility of the framework on a number of scenarios. Finally, we give a learning algorithm with a prototype implementation and discuss the possibilities of model checking and monitoring.

Kush Grover, Pratham Gupta, Jan Křetínský

Fondazione Bruno Kessler · Indian Institute of Science · Masaryk University

Temporal ReasoningSignal Temporal LogicRobot Motion PlanningTemporal LogicSTL Motion Planning
AskPDF
Apr 13, 2026

Ternary Logic Encodings of Temporal Behavior Trees with Application to Control Synthesis

Behavior Trees (BTs) provide designers with an intuitive graphical interface to construct long-horizon plans for autonomous systems. To ensure their correctness and safety, rigorous formal models and verification techniques are essential. Temporal BTs (TBTs) offer a promising approach by leveraging existing temporal logic formalisms to specify and verify the executions of BTs. However, this analysis is currently limited to offline post hoc analysis and trace repair. In this paper, we reformulate TBTs using a ternary-valued Signal Temporal Logic (STL) amenable to control synthesis. Ternary logic introduces a third truth value Unknown, formally capturing cases where a trajectory has neither fully satisfied nor violated a specification. We propose mixed-integer linear encodings for partial trajectory STL and TBTs over ternary logic, allowing for correct-by-construction control strategies for linear dynamical systems via mixed-integer optimization. We demonstrate the utility of our framework by solving optimal control problems.

Ryan Matheu, John S. Baras, Calin Belta

Institute for Systems Research, University of Maryland, College Park, USA.

Behavior TreesSignal Temporal Logic
AskPDF
Apr 6, 2026

Stratifying Reinforcement Learning with Signal Temporal Logic

In this paper, we develop a stratification-based semantics for Signal Temporal Logic (STL) in which each atomic predicate is interpreted as a membership test in a stratified space. This perspective reveals a novel correspondence principle between stratification theory and STL, showing that most STL formulas can be viewed as inducing a stratification of space-time. The significance of this interpretation is twofold. First, it offers a fresh theoretical framework for analyzing the structure of the embedding space generated by deep reinforcement learning (DRL) and relates it to the geometry of the ambient decision space. Second, it provides a principled framework that both enables the reuse of existing high-dimensional analysis tools and motivates the creation of novel computational techniques. To ground the theory, we (1) illustrate the role of stratification theory in Minigrid games and (2) apply numerical techniques to the latent embeddings of a DRL agent playing such a game where the robustness of STL formulas is used as the reward. In the process, we propose computationally efficient signatures that, based on preliminary evidence, appear promising for uncovering the stratification structure of such embedding spaces.

Justin Curry, Alberto Speranzon

University at Albany, State University of New York, Department of Mathematics and Statistics, 1400 Washington Ave., Albany, NY 12202 USA · Lockheed Martin, Advanced Technology Labs, 1303 Corporate Center Dr, Eagan, MN 55121 USA

Signal Temporal LogicReinforcement LearningRepresentation Learning for RL
AskPDF
Mar 30, 2026

Structural-Ambiguity-Aware Translation from Natural Language to Signal Temporal Logic

Signal Temporal Logic (STL) is widely used to specify timed and safety-critical tasks for cyber-physical systems, but writing STL formulas directly is difficult for non-expert users. Natural language (NL) provides a convenient interface, yet its inherent structural ambiguity makes one-to-one translation into STL unreliable. In this paper, we propose an ambiguity-preserving method for translating NL task descriptions into STL candidate formulas. The key idea is to retain multiple plausible syntactic analyses instead of forcing a single interpretation at the parsing stage. To this end, we develop a three-stage pipeline based on Combinatory Categorial Grammar (CCG): ambiguity-preserving nn-best parsing, STL-oriented template-based semantic composition, and canonicalization with score aggregation. The proposed method outputs a deduplicated set of STL candidates with plausibility scores, thereby explicitly representing multiple possible formal interpretations of an ambiguous instruction. In contrast to existing one-best NL-to-logic translation methods, the proposed approach is designed to preserve attachment and scope ambiguity. Case studies on representative task descriptions demonstrate that the method generates multiple STL candidates for genuinely ambiguous inputs while collapsing unambiguous or canonically equivalent derivations to a single STL formula.

Kosei Fushimi, Kazunobu Serizawa, Junya Ikemoto +1

The authors are with the Graduate School of Engineering, The University of Osaka, Suita, Japan

Semantic ParsingSignal Temporal Logic
AskPDF
Mar 29, 2026

LLM-Enabled Low-Altitude UAV Natural Language Navigation via Signal Temporal Logic Specification Translation and Repair

Natural language (NL) navigation for low-altitude unmanned aerial vehicles (UAVs) offers an intelligent and convenient solution for low-altitude aerial services by enabling an intuitive interface for non-expert operators. However, deploying this capability in urban environments necessitates the precise grounding of underspecified instructions into safety-critical, dynamically feasible motion plans subject to spatiotemporal constraints. To address this challenge, we propose a unified framework that translates NL instructions into Signal Temporal Logic (STL) specifications and subsequently synthesizes trajectories via mixed-integer linear programming (MILP). Specifically, to generate executable STL formulas from free-form NL, we develop a reasoning-enhanced large language model (LLM) leveraging chain-of-thought (CoT) supervision and group-relative policy optimization (GRPO), which ensures high syntactic validity and semantic consistency. Furthermore, to resolve infeasibilities induced by stringent logical or spatial requirements, we introduce a specification repair mechanism. This module combines MILP-based diagnosis with LLM-guided semantic reasoning to selectively relax task constraints while strictly enforcing safety guarantees. Extensive simulations and real-world flight experiments demonstrate that the proposed closed-loop framework significantly improves NL-to-STL translation robustness, enabling safe, interpretable, and adaptable UAV navigation in complex scenarios.

Yuqi Ping, Huahao Ding, Tianhao Liang +6

Guangdong Provincial Key Laboratory of Space-Aerial Networking and Intelligent Sensing, Harbin Institute of Technology, Shenzhen, China · Information Systems Technology and Design, Singapore University of Technology and Design, Singapore 487372 · School of Computer Science and Engineering, Central South University, Changsha, China +1

UAV NavigationRobot NavigationLarge Language Model-Based Robot PlanningSignal Temporal Logic
AskPDF
Mar 28, 2026

Conformalized Signal Temporal Logic Inference under Covariate Shift

Signal Temporal Logic (STL) inference learns interpretable logical rules for temporal behaviors in dynamical systems. To ensure the correctness of learned STL formulas, recent approaches have incorporated conformal prediction as a statistical tool for uncertainty quantification. However, most existing methods rely on the assumption that calibration and testing data are identically distributed and exchangeable, an assumption that is frequently violated in real-world settings. This paper proposes a conformalized STL inference framework that explicitly addresses covariate shift between training and deployment trajectories dataset. From a technical standpoint, the approach first employs a template-free, differentiable STL inference method to learn an initial model, and subsequently refines it using a limited deployment side dataset to promote distribution alignment. To provide validity guarantees under distribution shift, the framework estimates the likelihood ratio between training and deployment distributions and integrates it into an STL-robustness-based weighted conformal prediction scheme. Experimental results on trajectory datasets demonstrate that the proposed framework preserves the interpretability of STL formulas while significantly improving symbolic learning reliability at deployment time.

Yixuan Wang, Danyang Li, Matthew Cleaveland +2

Mingyu Cai and Yixuan Wang are with Mechanical Engineering, University of California, Riverside, CA, 92521, USA. · Danyang Li and Roberto Tron are with Mechanical Engineering, Boston University. · Matthew Cleaveland is with MIT Lincoln Laboratory, Lexington, MA, 02421, USA

Signal Temporal LogicConformal PredictionCovariate ShiftWeighted Conformal Prediction
AskPDF