Research map / Reinforcement learning / Visual and representation RL
DeepLTL: Learning to Efficiently Satisfy Complex LTL Specifications for Multi-Task RL
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Proposes DeepLTL, which zero-shot satisfies arbitrary (finite and infinite-horizon) LTL specifications by extracting reach-avoid sequences from LDBAs and following a DeepSets+GRU sequence-conditioned PPO policy selected via a learned value function.
Problem
Learning multi-task RL policies that zero-shot satisfy arbitrary LTL specifications, including omega-regular ones, efficiently, non-myopically and with safety constraints.
Approach
Represent the current LDBA state by a set of reach-avoid sequences of truth assignments extracted from accepting cycles; train a goal-conditioned policy on such sequences with DeepSets encodings and a backward GRU; at test time pick the sequence with highest learned value and execute it.
Key results
- On complex LetterWorld specs, DeepLTL reaches success rate 1.00 on phi_1 with 9.66 mean steps vs GCRL-LTL 0.94 / 15.29 steps.
- On FlatWorld phi_15, DeepLTL achieves 0.86 success rate while LTL2Action gets 0.07 and GCRL-LTL 0.73.
- DeepLTL outperforms GCRL-LTL on most ZoneEnv complex tasks in both success rate and steps (e.g., phi_8 0.96 SR, 259.75 steps vs 0.89 SR, 449.70 steps).
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Use reach-avoid sequence representation and sequence-conditioned policy instead of the baseline methods | DeepLTL · Complex finite-horizon specifications in LetterWorld, ZoneEnv, and FlatWorld | success rate (SR) | Helped |
| Use reach-avoid sequence representation and sequence-conditioned policy instead of the baseline methods | DeepLTL · Complex finite-horizon specifications in LetterWorld, ZoneEnv, and FlatWorld | average steps to satisfy (μ) | Helped |
| Reason over temporally extended reach-avoid sequences rather than composing subtask policies | GCRL-LTL · Complex finite-horizon specifications | efficiency | Helped |
| Use DeepLTL for infinite-horizon specifications rather than GCRL-LTL | DeepLTL · Infinite-horizon recurrence tasks | visits to accepting states per episode | Helped |
Limitations
- Only the eventual-discounting extension is left as untested future work
- GCRL-LTL remains competitive on some tasks (e.g., FlatWorld phi_12 steps and phi_16 steps are better for baselines)
- Relies on a finite prefix approximation of infinite sequences with a fixed number of loop repetitions
Experimental setup
Datasets: LetterWorld ZoneEnv FlatWorld
Benchmarks: LetterWorld complex finite-horizon specs ZoneEnv complex specs FlatWorld complex specs infinite-horizon recurrence specs
Metrics: discounted return success rate average steps to completion average accepting-state visits
Baselines: LTL2Action GCRL-LTL RAD-embeddings
Builds on: LTL2Action GCRL-LTL eventual discounting DeepSets PPO
Closest papers by meaning
- One Subgoal at a Time: Zero-Shot Generalization to Arbitrary Linear Temporal Logic Requirements in Multi-Task Reinforcement Learning (NeurIPS 2025 · similarity 0.93)
- Zero-Shot Instruction Following in RL via Structured LTL Representations (NeurIPS 2026 · similarity 0.92)
- Reinforcement Learning with LTL and $\omega$-Regular Objectives via Optimality-Preserving Translation to Average Rewards (NeurIPS 2024 · similarity 0.88)
- Automaton Constrained Q-Learning (NeurIPS 2025 · similarity 0.88)
- Regret-Free Reinforcement Learning for Temporal Logic Specifications (ICML 2025 · similarity 0.88)
- Temporal Logic Specification-Conditioned Decision Transformer for Offline Safe Reinforcement Learning (ICML 2024 · similarity 0.87)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.