Source-linked AI summary
Temporal Logic Specification-Conditioned Decision Transformer for Offline Safe Reinforcement Learning
Zijian Guo, Weichao Zhou, Wenchao Li
TL;DR
Offline safe RL must satisfy complex temporal constraints using fixed data, but conventional conditioned policies do not fully represent such structure. SDT conditions Decision Transformer sequence modeling on STL specifications and robustness information. It learns safe, high-reward policies, outperforms multiple baselines, and adapts to different satisfaction thresholds and suffix configurations without retraining.
Problem
Offline safe RL needs policies that achieve high reward under constraints from fixed data, while real-world tasks often require complex temporal and logical rules that standard cost functions do not capture well.
Method
SDT combines Decision Transformer sequence modeling with STL specifications and prefix and suffix robustness values as conditioning inputs.
Results
SDT outperforms multiple baselines in safety and task performance and generalizes to different robustness thresholds and configurations without retraining the policy.
Takeaways & Limitations
STL-conditioned sequence modeling can learn safe, high-reward policies for offline tasks with temporal and logical requirements.
Takeaways & Limitations
STL robustness targets cannot be updated autoregressively like additive rewards or costs, so target suffixes must be set in advance.
Abstract
from arXiv · showhide
Offline safe reinforcement learning (RL) aims to train a constraint satisfaction policy from a fixed dataset. Current state-of-the-art approaches are based on supervised learning with a conditioned policy. However, these approaches fall short in real-world applications that involve complex tasks with rich temporal and logical structures. In this paper, we propose temporal logic Specification-conditioned Decision Transformer (SDT), a novel framework that harnesses the expressive power of signal temporal logic (STL) to specify complex temporal rules that an agent should follow and the sequential modeling capability of Decision Transformer (DT). Empirical evaluations on the DSRL benchmarks demonstrate the better capacity of SDT in learning safe and high-reward policies compared with existing approaches. In addition, SDT shows good alignment with respect to different desired degrees of satisfaction of the STL specification that it is conditioned on.
1. Introduction
Offline safe RL must learn high-reward policies from fixed data while satisfying constraints that can involve complex temporal and logical behavior. SDT combines STL specifications with Decision Transformer sequence modeling, using robustness-conditioned inputs to improve safety, performance, and threshold generalization.
- Motivation: Complex real-world tasks require temporal and logical constraints that are difficult to capture with standard cost functions.Examples include stopping at an intersection, pausing, and proceeding only when no other cars are present.
- Motivation: STL expresses safety, liveness, sequentiality, and combinations of these behaviors over time, while its quantitative semantics measure satisfaction degree.This expressiveness makes STL suitable for specifying trajectory-level requirements.
- Method: SDT combines STL’s expressive temporal specifications with Decision Transformer sequence modeling to learn safe, high-performance policies from fixed offline data.The framework conditions DT on STL specifications rather than relying only on conventional reward or cost targets.
- Method: SDT introduces prefix and suffix robustness tokens that use complementary portions of trajectories to guide autoregressive learning.These inputs expose different temporal information to the sequence model.
- Results: SDT outperforms multiple baselines in safety and task performance by a large margin and generalizes across robustness thresholds and configurations without policy retraining.These findings are reported from comprehensive experiments.
2. Related Work
Prior offline safe RL work largely formulates safety as constrained optimization or conditions supervised policies on rewards and costs. This paper instead uses formal STL specifications to represent temporal properties that standard reward and cost functions may not capture.
- Constrained optimization for offline safe RL: Constrained-optimization methods for offline safe RL include distribution-correction and primal-dual approaches, but temporal constraints remain underexplored.These methods balance reward and cost using fixed trajectories, cost thresholds, distribution estimates, or Lagrangian penalties.
- Conditioned RL: Decision Transformer variants extend reward-conditioned supervised learning to offline RL by conditioning action prediction on return-to-go.Cost-conditioned extensions additionally target safety and generalization across cost thresholds.
- Conditioned RL: The paper adopts formal specifications as conditioning inputs to characterize temporal properties that standard reward or cost functions are difficult to capture.This distinguishes SDT from conventional reward- and cost-conditioned approaches.
- STL as reward or cost functions in RL: STL has been used to specify high-level goals and safety requirements and to evaluate agent behavior in reinforcement learning.Its rich syntax supports temporal requirements beyond ordinary scalar reward design.
3. Preliminaries
Offline safe RL learns reward-maximizing policies under cost constraints from fixed trajectories, while Decision Transformers model action sequences conditioned on return-to-go. STL supplies temporal formulas over sampled state signals, and robustness values quantify how strongly trajectories satisfy them.
- MDP Preliminaries: A trajectory consists of sequential state-action pairs over a finite horizon, and the policy seeks to maximize expected cumulative reward.These objects provide the sequential data modeled by offline RL and Decision Transformers.
- Offline Safe RL: Offline safe RL uses a fixed dataset of trajectories without environment interaction, aiming to maximize reward while keeping cumulative constraint cost below a threshold.The formulation is based on constrained Markov decision processes.
- Decision Transformers: Decision Transformer predicts actions from sequences of return-to-go, states, and actions using GPT-style causal self-attention.Its policy is trained by minimizing the difference between predicted and ground-truth actions.
- Signal Temporal Logic: STL specifies temporal properties of discretely sampled state signals using predicates and temporal operators such as Globally, Finally, and Until.The syntax supports Boolean combinations and sequential time intervals.
- STL Quantitative Semantics: STL robustness assigns a quantitative value to a trajectory’s satisfaction of a formula at each time step.A positive or negative sign indicates satisfaction or violation, while larger values indicate stronger satisfaction.
4. Method
SDT formulates offline safe RL as autoregressive supervised trajectory modeling conditioned on rewards, costs, and STL robustness values. It extends Decision Transformer with prefix and suffix robustness tokens to represent temporal constraints and guide Gaussian action prediction.
- 4.1. Offline RL via Supervised Learning: SDT models trajectories autoregressively from fixed offline data, conditioning action prediction on reward and cost functions rather than solving the constrained optimization problem directly.This formulation encompasses methods such as RvS, DT, ODT, QDT, CDT, and SaFormer, while SDT combines transformer policies with STL robustness values.
- 4.2. Specification-Conditioned Decision Transformers: SDT extends Decision Transformer with prefix and suffix robustness tokens alongside return-to-go, states, and actions, and predicts actions with a stochastic Gaussian policy.The framework retains reward conditioning for performance and uses entropy regularization during stochastic policy learning.
- 4.3. Suffix and Prefix Robustness Values: Prefix and suffix robustness address sparse suffix feedback, because STL satisfaction may depend on only a few critical states or intervals.When most suffix values are constant, the agent receives limited meaningful information; prefix values provide an additional trajectory segment for conditioning.
- 4.3. Suffix and Prefix Robustness Values: Suffix robustness summarizes desired future specification satisfaction, but its non-additive, specification-dependent recursion requires target suffixes to be specified in advance.Unlike return-to-go or cost-to-go, suffix robustness cannot be updated by simply subtracting the newly observed reward or cost.
- 4.3. Suffix and Prefix Robustness Values: Prefix robustness summarizes achieved past satisfaction and complements suffix robustness by comparing safety across past and future trajectory segments.Positive or negative prefix–suffix combinations distinguish safe and unsafe past and future behavior, helping provide information beyond the model's context length.
5. Experiment
SDT is evaluated on Bullet-Safety-Gym tasks with temporal specifications, relabeled offline costs, and comparisons against safe-RL and sequence-modeling baselines. It achieves stronger specification satisfaction and lower costs while retaining competitive rewards, aligns with target suffixes, and benefits from explicit prefix and suffix inputs.
- 5.1. Can SDT learn specification-satisfying policies?: SDT achieves the highest specification satisfaction and lowest costs while producing comparable or higher rewards than safe baselines.The evaluation averages 3 random seeds and 20 trajectories per seed; complete environment results are reported in the appendix.
- 5.1. Can SDT learn specification-satisfying policies?: Relabeling costs alone does not yield safe policies, while Markovian-cost baselines struggle with the non-Markovian temporal constraints.CDT and RvS-RC can retain high rewards despite low satisfaction, and Lagrangian and Q-learning baselines often fail to ensure safety.
- 5.2. Can SDT adapt to different target suffixes?: SDT aligns evaluated rewards and suffixes with varied target suffixes and remains safe when extrapolating to conflicting target combinations.RvS-Rρ struggles to meet target rewards at large or small suffixes, whereas SDT maintains safety across these settings.
- 5.3. Ablation studies: Removing either prefix or suffix inputs reduces safety and performance, with suffix removal having the larger effect on safety.The ablation normalizes cost against the highest cost among the corresponding experiments.
- 5.3. Ablation studies: An explicit reward prefix improves standard Decision Transformer rewards, while different suffix configurations still outperform baselines in satisfaction rate.The tested suffix configurations are linear, mean, and maximum, corresponding respectively to increasing, average-safe-trajectory, and conservative target behavior.
- 5.3. Ablation studies: Scaling individual predicates has negligible impact on task performance and specification satisfaction, indicating robustness to predicate rescaling.This conclusion is reported from the varying-scaling-factor evaluation in Table 3.
6. Conclusion
The paper frames SDT as a supervised-learning framework that uses STL robustness to guide Decision Transformer trajectory modeling for offline safe RL. Empirically, SDT learns safe, high-reward policies, adapts to target suffixes without retraining, and performs across suffix configurations.
- SDT uses STL robustness values to guide trajectory modeling in Decision Transformer for offline safe RL with temporal and logical requirements.
- SDT learns safe and high-reward policies in challenging offline tasks involving temporal and logical requirements.
- SDT adapts to different target suffixes without retraining and performs effectively across diverse target suffix configurations.
Impact Statement
The paper reports no ethical concerns from its methods, experiments, or results, while cautioning that misspecified specifications may cause serious and unforeseen consequences in real-world testing.
- The methods, experiments, and results are reported not to pose ethical concerns.
- Misspecified specifications may result in serious and unforeseen consequences when reinforcement learning is applied in real-world settings.
- The authors hope the findings provide insights for extending reinforcement learning to broader domains.
A. Environment Setting
The experiments use Bullet-safety-gym Run and Circle environments with reward and cost functions tied to movement objectives and safety boundaries. Costs are relabeled to represent temporal specification violations, and the offline datasets contain reward–cost and suffix–reward trade-offs.
- Environment Setting: Run agents are rewarded for high-speed movement between safety boundaries but penalized for boundary crossings or exceeding robot-specific velocity thresholds.
- Environment Setting: Circle agents are rewarded for clockwise circular motion while required to remain inside a designated safe area smaller than the intended circle.
- Environment Setting: Relabeled costs mark Circle violations after five consecutive prior cost violations and Run violations after five prior speeding violations or a boundary crossing.
- Offline Dataset: The offline datasets show an increasing reward trend as relabeled cost rises, indicating a reward–cost trade-off across training tasks.
- Offline Dataset: Figure 5 plots relabeled cost versus reward and suffix versus reward by environment, with each point representing a collected trajectory.
- Implementation: SDT is implemented with STL robustness prefix and suffix tokens added to Transformer inputs and trained for 200000 steps.
B. Complete Results of SDT
SDT achieves high satisfaction rates across environments and generally outperforms or provides more consistent performance than the evaluated baselines. Its target suffix is chosen as positive robustness, while different suffix configurations and evaluation protocols test alignment with specification satisfaction.
- Complete Results of SDT: SDT achieves high satisfaction rates across environments, consistently adhering to safety specifications while maintaining high reward.
- Complete Results of SDT: BC-Safe fails to learn zero-violation policies and shows conservative, low-reward performance, whereas RvS-Rρ is inconsistent across environments.
- Complete Results of SDT: RvS-Rρ performs worse in Ball-Run than expected because it lacks Transformer-based sequential modeling for temporal policies.
- Target Suffix Configurations: Figure 6 compares fixed, linearly increasing, mean-safe-trajectory, and maximum-safe-trajectory target suffix configurations.
- Target Suffix Configurations: Positive robustness values are used as target suffixes because they indicate specification satisfaction, with larger values indicating stronger satisfaction.
- Evaluation Protocol: Figure 7 reports normalized reward for DT and reward-prefix DT using means and mean ± standard deviation under the D4RL evaluation protocol.
C. Experiments of Decision Transformers
The experiment evaluates Decision Transformers with and without a reward prefix on D4RL to demonstrate the prefix’s role across multiple environments and dataset types.
- The study compares standard Decision Transformers with Decision Transformers augmented by a reward prefix on the D4RL benchmark.
- Experiments cover Halfcheetah, Walker2D, and Hopper using medium and medium-replay datasets.
- The evaluation uses the official Decision Transformer codebase and default hyperparameters.