Paper deep dive
Jaxolotl: A Unified High-Performance Benchmark Suite for LTL-Based Multi-Task RL
Mathias Jackermeier, Jacques Cloete, Alessandro Abate
Intelligence
Status: not_run | Model: - | Prompt: - | Confidence: 0%
Entities (0)
Relation Signals (0)
No relation signals yet.
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:Training agents to follow arbitrary instructions is an important goal of multi-task reinforcement learning (RL). Linear temporal logic (LTL) provides a precise and structured formalism for specifying instructions to agents, and has been successfully adopted for training generalist multi-task policies. However, differences in implementations, task distributions, and evaluation protocols make existing methods difficult to compare, while high computational costs limit the scale and statistical reliability of experiments. We introduce Jaxolotl, a unified high-performance benchmark suite for multi-task LTL-RL to address these concerns. Jaxolotl provides a modular, end-to-end JAX implementation of six representative algorithms and four environments, together with newly curated task suites and a standardised, statistically robust evaluation protocol. By precompiling symbolic task representations into static arrays, Jaxolotl enables fully JIT-compiled training and evaluation, achieving end-to-end speedups of up to $220\times$ and supporting controlled comparisons at substantially greater experimental scale. We use this framework to systematically evaluate existing approaches, revealing complementary strengths and limitations: general methods capable of non-myopic reasoning struggle as the number of propositions grows, while methods with stronger scaling rely on environment-specific assumptions and suffer from myopia.
Tags
Links
- Source: https://arxiv.org/abs/2609.38065v1
- Canonical: https://arxiv.org/abs/2609.38065v1
PDF not stored locally. Use the link above to view on the source site.
Full Text
146,417 characters extracted from source content.
Expand or collapse full text
Jaxolotl: A Unified High-Performance Benchmark Suite for LTL-Based Multi-Task RL Mathias Jackermeier Jacques Cloete Alessandro Abate Affiliation: Department of Computer Science, University of Oxford Affiliation: Oxford Robotics Institute, University of Oxford Abstract Training agents to follow arbitrary instructions is an important goal of multi-task reinforcement learning (RL). Linear temporal logic (LTL) provides a precise and structured formalism for specifying instructions to agents, and has been successfully adopted for training generalist multi-task policies. However, differences in implementations, task distributions, and evaluation protocols make existing methods difficult to compare, while high computational costs limit the scale and statistical reliability of experiments. We introduce Jaxolotl, a unified high-performance benchmark suite for multi-task LTL-RL to address these concerns.11footnotemark: 1 Jaxolotl provides a modular, end-to-end JAX implementation of six representative algorithms and four environments, together with newly curated task suites and a standardised, statistically robust evaluation protocol. By precompiling symbolic task representations into static arrays, Jaxolotl enables fully JIT-compiled training and evaluation, achieving end-to-end speedups of up to 220×220× and supporting controlled comparisons at substantially greater experimental scale. We use this framework to systematically evaluate existing approaches, revealing complementary strengths and limitations: general methods capable of non-myopic reasoning struggle as the number of propositions grows, while methods with stronger scaling rely on environment-specific assumptions and suffer from myopia. **footnotetext: Equal contribution 1Code is available at: https://github.com/mathiasj33/jaxolotl 1 Introduction Multi-task reinforcement learning (RL) is a promising approach towards training generalist agents that can complete diverse objectives. A central question in this setting is how to specify tasks (or instructions) to the agent. While many works have explored natural language as an intuitive interface (e.g. Hill et al., 2020; Carta et al., 2023), there has been increasing interest in formal specification languages such as linear temporal logic (LTL; Pnueli, 1977). LTL specifies temporally extended tasks over atomic propositions, i.e. high-level Boolean features of the environment state, and is especially appealing due to its unambiguous semantics and compositional task structure. Despite recent progress in multi-task LTL-conditioned RL (Vaezipoor et al., 2021; Qiu et al., 2023; Liu et al., 2024; Jackermeier and Abate, 2025; Guo et al., 2025; Jackermeier et al., 2026), it remains challenging to understand how different methods actually compare: existing evaluations rely on different environments, evaluation protocols, and low-level implementation details, making it difficult to draw general conclusions. As a result, it is unclear whether reported differences arise from algorithmic choices or from experimental setup. Systematic comparison is further hindered by the computational cost of experiments, which typically involve training RL agents for millions of steps in CPU-based environments, restricting evaluations to a few random seeds and limiting broad analyses. We introduce Jaxolotl (JAX-Optimised Learning for Objectives in Temporal Logic) as a unified benchmark suite to address these shortcomings. Jaxolotl provides a modular, end-to-end JAX (Bradbury et al., 2018) implementation of six representative algorithms and four environments, spanning high-dimensional navigation, continuous control, and object interaction. We precompile inherently symbolic task structures, such as finite automata and syntax trees, into static tensor representations to meet JAX’s strict requirements on static array shapes and functional control flow. This allows us to fully just-in-time (JIT) compile the entire training and evaluation loop, leading to end-to-end speedups of up to 220×220× over reference implementations on hardware accelerators. These efficiency improvements enable controlled benchmarking at substantially greater experimental scale, such as training 10 independent seeds in under four minutes rather than 13.4 hours. We use Jaxolotl to conduct an extensive controlled benchmark of existing methods, isolating aspects such as general task satisfaction, non-myopic reasoning, and scaling with the number of atomic propositions. Our experiments reveal complementary limitations in current approaches: general methods capable of non-myopic reasoning (i.e. reasoning about the entire task rather than individual subgoals) struggle to scale to environments with large numbers of propositions. Conversely, methods exhibiting stronger proposition scaling rely on environment-specific observation-reduction functions and suffer from myopia, preventing them from planning multiple steps ahead. Our main contributions are as follows: • we introduce Jaxolotl, an open-source JAX benchmark suite for multi-task LTL-RL, unifying six representative algorithms and four environments under shared abstractions; • we design a precompilation strategy for dynamic symbolic task representations that enables end-to-end JIT compilation, yielding training speedups of up to 220×220×; • we establish a standardised evaluation protocol and curated task suites for controlled comparison across methods, including uncertainty estimates over independently trained policies; • lastly, we conduct an extensive benchmark evaluating existing methods across general task completion, non-myopic reasoning, and proposition scaling, uncovering complementary strengths and limitations of current approaches. 2 Related Work Figure 1: Overview of Jaxolotl’s design and implementation. We provide a modular implementation of representative multi-task LTL-RL algorithms in terms of a generic task representation, policy architecture, and shared common modules. Precompilation of dynamic structures and environment resets enables end-to-end JIT compilation of the entire training and evaluation loop. LTL-Based Multi-Task RL. LTL and related formalisms such as reward machines are widely used to specify single, fixed tasks for RL agents (Hahn et al., 2019; Camacho et al., 2019; Toro Icarte et al., 2022; Voloshin et al., 2023; Hasanbeig et al., 2023). We instead consider the multi-task setting, where a single policy is required to zero-shot execute arbitrary LTL instructions. Many approaches have been developed for this setting, which can be broadly categorised into decomposition-based and holistic methods. Decomposition-based methods break down LTL specifications into subgoals that can be completed one at a time by a goal-conditioned policy (Araki et al., 2021; León et al., 2022; Qiu et al., 2023; Liu et al., 2024; Guo et al., 2025). While this simplifies learning, it limits the agent’s ability to reason about the entire task and may lead to myopic behaviour. Holistic approaches instead condition the policy on broader task structure, for example by encoding the formula syntax tree (Vaezipoor et al., 2021) or Büchi automaton sequences (Jackermeier and Abate, 2025). Recent work targets scaling to large proposition sets, via proposition-specific observation reduction (Guo et al., 2025) or parameterised predicates (Cloete et al., 2026). While the field has seen rapid progress in recent years, it remains difficult to compare methods due to differences in environments, task distributions, and evaluation protocols. Our work builds on these existing LTL-based multi-task RL methods and unifies them within a single JAX framework. Existing LTL-Based Benchmarks. Closest to our work, Guo et al. (2026) introduce SpecRLBench, a suite of environments and tasks for generalisation in multi-task LTL-RL. While SpecRLBench standardises several experimental settings, it relies on the methods’ original codebases, retaining differences in their training and evaluation pipelines. In contrast, Jaxolotl provides a unified implementation of six representative algorithms, together with a standardised evaluation protocol and curated task suites for controlled comparison. Furthermore, while SpecRLBench relies on CPU-based environments, Jaxolotl enables end-to-end training and evaluation on hardware accelerators, yielding orders-of-magnitude speedups over the reference algorithm implementations. These speedups make larger-scale, statistically robust benchmarking practical. Concurrent work (Peng et al., 2026) evaluates VLA policies using LTLf monitors, but does not address multi-task LTL-RL methods. Hardware-Accelerated RL. The speedups enabled by end-to-end JIT-compiled training in JAX (Lu et al., 2022) have spurred a broad ecosystem of accelerated environments (Freeman et al., 2021; Lange, 2022; Bonnet et al., 2024; Matthews et al., 2024; Pignatelli et al., 2025; Zakka et al., 2025) and algorithm libraries (Liesen et al., 2024; Rutherford et al., 2024). Closest to our design, XLand-MiniGrid (Nikulin et al., 2024) encodes procedurally generated symbolic rules and goals as fixed-size arrays to enable compiled multi-task training. However, these accelerated frameworks do not support LTL-specified tasks, whose inherently dynamic structure in the form of finite automata or syntax trees poses a significant challenge for JIT compilation. See Appendix A for extended related work. 3 Background Reinforcement Learning. We consider a standard reinforcement learning (RL) setting, where an agent interacts with an environment modelled as a Markov decision process (MDP). An MDP is a tuple ℳ=(,,P,R,γ,ρ0)M=(S,A,P,R,γ, _0), where S is the state space, A is the action space, P:×→[0,1]P:S×A×S→[0,1] is the transition kernel, R:×→R:S×A×S is the reward function, γ∈[0,1)γ∈[0,1) is the discount factor, and ρ0∈Δ() _0∈ (S) is the initial state distribution. The agent’s objective is to learn a (stationary) policy π:→Δ()π:S→ (A) that maximises the expected cumulative discounted reward Eτ∼π[∑t=0∞γtR(st,at,st+1)],E_τ π [ _t=0^∞γ^tR(s_t,a_t,s_t+1) ], where τ∈(×)∞τ∈(S×A)^∞ is a trajectory generated by π in ℳM. Linear Temporal Logic. Linear temporal logic (LTL; Pnueli, 1977) is a formal language for specifying temporal properties of systems, which is being increasingly adopted as a task specification language in multi-task RL. The basic unit of LTL formulae are atomic propositions APAP, which represent Boolean properties of the environment (e.g. “the agent is at the goal”). The syntax of LTL formulae is defined recursively as follows: φ::=⊤||¬φ|φ1∧φ2|φ|φ1φ2 ::= \;|\; p\;|\; \;|\; _1 _2\;|\; X\, \;|\; _1\; U\; _2 where ⊤ is the Boolean constant true, ∈AP p∈ AP is an atomic proposition, ¬ is negation, ∧ is conjunction, X\, is the next operator, and \; U\; is the until operator. Standard Boolean connectives (e.g. ∨ , →) and temporal operators (e.g. F\,, G\,) can be derived from the above syntax. Intuitively, φ X\, means that φ is true in the next step, φ1φ2 _1\; U\; _2 means that φ1 _1 holds until φ2 _2 is true, φ F\, means that φ eventually holds at some future time step, and φ G\, means that φ is true always (at all time steps). These operators allow for the specification of complex compositional and temporally extended tasks, such as “eventually reach the goal while avoiding obstacles” or “visit all rooms in a specific order”. To interpret LTL formulae in an MDP, we assume a labelling function L:→2APL → 2^AP that returns the set of true atomic propositions for a given state. An MDP trajectory τ satisfies an LTL formula φ , denoted by τ⊧φτ , if the sequence of labels L(s0),L(s1),…L(s_0),L(s_1),… satisfies the formula according to the standard semantics of LTL (see Appendix B). Multi-task RL with LTL specifications aims to train generalist LTL policies by solving the following optimisation problem: π∗(⋅|φ)∈argmaxπEφ∼,τ∼π|φ[1[τ⊧φ]],π^*(·\,|\, )∈ _π _ subarrayc ,\\ τ π\,|\, subarray [1[τ ] ], where D is an arbitrary distribution over LTL tasks, and π|φπ\,|\, is a policy conditioned on the task φ . 4 Jaxolotl We present Jaxolotl (JAX-Optimised Learning for Objectives in Temporal Logic), a unified high-performance benchmark suite for multi-task RL with LTL specifications. Jaxolotl provides a modular end-to-end JAX implementation of representative multi-task LTL-RL environments and algorithms, enabling controlled benchmarking at substantially greater experimental scale. 4.1 Design Principles See Figure 1 for an illustration of Jaxolotl’s design and implementation principles. The framework is designed to be modular via common abstractions, leverages flexible configuration management, and achieves highly efficient training and evaluation via end-to-end JIT compilation. Modular Abstractions. Jaxolotl defines modular abstractions that allow implementing LTL-RL methods in terms of a generic task representation and policy architecture. Here, a task representation is the algorithm-specific data structure used to encode the current LTL instruction, such as a formula syntax tree (Vaezipoor et al., 2021), reach–avoid sequence (Jackermeier and Abate, 2025), or reach–avoid subgoal (Guo et al., 2025). As the agent interacts with the environment and completes parts of the task, this representation is generally updated online. A task encoder maps this representation to an embedding for the policy. The policy architecture further consists of an observation encoder to process environment observations, and a shared actor–critic module that outputs actions and value estimates based on the combined observation and task embeddings. Actions and value estimates are used for policy optimisation using goal-conditioned RL (Liu et al., 2022), where goals are task representations sampled at the beginning of each episode. A reusable curriculum learning implementation lets users gradually increase task complexity during training. Curricula consist of a sequence of stages with different task distributions, and the agent progresses to the next stage once it achieves a specified performance threshold. Jaxolotl currently supports on-policy optimisation with PPO (Schulman et al., 2017), but the abstractions are agnostic to the underlying RL algorithm and can be extended to support off-policy methods. By providing reusable implementations of common modules, Jaxolotl enables controlled comparisons between different algorithms, while keeping shared components such as observation encoders fixed. The modular design further makes it easy to combine components from different methods, and to extend the framework with new approaches in the future. Flexible Configuration. Experiments are configured using Hydra (Yadan, 2019), a flexible configuration management system. We provide pre-defined configurations for the entire benchmark suite, and individual hyperparameters or components can be overridden directly from the command line. To illustrate, training DeepLTL (Jackermeier and Abate, 2025) on ZoneEnv is as simple as running: $ python scripts/train.py alg=deep_ltl env=zone_env End-to-End JIT Compilation. JAX’s just-in-time (JIT) compilation achieves significant speedups by compiling Python code into XLA-optimised kernels for accelerators such as GPUs or TPUs. Jaxolotl follows the recent trend of JIT-compiling the entire training and evaluation loop (Lu et al., 2022; Liesen et al., 2024), rather than only the environment step function or policy network. However, end-to-end compilation is considerably more challenging for LTL-RL than for standard RL workloads. The algorithms considered in this work manipulate symbolic objects whose structure depends on the sampled task, including formula syntax trees, automata with variable topology, and reach--avoid sequences with variable numbers of steps. These task representations are inherently dynamic and may change during environment interaction, directly conflicting with JAX’s strict requirements for static tensor shapes and control flow during JIT compilation.22 2 See https://docs.jax.dev/en/latest/notebooks/Common_Gotchas_in_JAX.html for an overview. Jaxolotl addresses this mismatch by extensively precompiling dynamic structures into static array representations, such as padded adjacency lists for formula graphs or padded transition tables for Büchi automata. Before training, we sample tasks for each curriculum stage, convert them into method-specific array representations, and pad all variable-sized components to fixed shapes. Task sampling and updating then reduce to simple array indexing operations, which are fully compatible with JIT compilation. We similarly precompute compact environment-reset descriptors to efficiently handle control flow under JIT, and compile evaluation formulae into static representations. The entire training and evaluation loops are therefore pure JIT-compiled functions, which further enables straightforward parallelisation across independent seeds via vmap. 4.2 Evaluation Infrastructure Deep RL algorithms are well-known to be sensitive to hyperparameter choices and random initialisation (Henderson et al., 2018; Chan et al., 2019), making meaningful comparisons between different methods challenging. Jaxolotl’s computational efficiency allows increasing the number of independent training runs and evaluation episodes at marginal cost (see § 5.1), thereby improving estimates of expected performance and its uncertainty due to training randomness. We leverage this to provide a standardised evaluation protocol that adapts the general evaluation principles of Agarwal et al. (2021) to the generalist-policy setting. In particular, Jaxolotl reports estimates of expected performance on a fixed set of benchmark tasks, together with 95% confidence intervals (CIs) over independent training runs. In contrast to conventional evaluation settings in which separate policies are trained for each task, each training run in our setting produces a single generalist policy that is evaluated on multiple tasks. This results in correlated scores across tasks, and we hence treat independently trained policies, rather than task-policy pairs, as the statistical units. Moreover, we deliberately use the arithmetic mean to aggregate performance across tasks, rather than a robust statistic such as the median or IQM (Agarwal et al., 2021). This ensures that potentially poor performance on difficult tasks is not discarded as outliers. Additionally, we provide per-task performance scores for fine-grained comparisons. We report two-sided 95% Student-t CIs (Student, 1908) over the resulting policy-level estimates. A full description of our evaluation protocol is provided in Appendix C. 4.3 Environments and Evaluation Tasks (a) LetterWorld (b) ZoneEnv (c) FrankaZoneEnv (d) Warehouse Figure 2: Visualisations of the main environments included in Jaxolotl. Jaxolotl includes JAX implementations of four main environments spanning discrete navigation, continuous control, and object interaction, visualised in Figure 2. These are summarised below: Environment Observation Space Action Space Reference LetterWorld Grid (7×7×137× 7× 13) Discrete (4 directions) Vaezipoor et al. (2021) ZoneEnv Proprioception + LiDAR (69D) Continuous (2D) Vaezipoor et al. (2021) FrankaZoneEnv Proprioception + range–bearing (72D) Continuous (6D) Guo et al. (2026) Warehouse Proprio. + LiDAR + inventory (47D) Hybrid (2D + 5D) Jackermeier et al. (2026) LetterWorld, ZoneEnv, and Warehouse are implemented directly in JAX, whereas our FrankaZoneEnv implementation is based on MuJoCo XLA (MJX; Todorov et al., 2012). Each environment comes with curated finite- and infinite-horizon specification suites derived from tasks in the literature. We provide further details on the environments and task suites in Appendix D. 4.4 Algorithms We provide unified implementations of six state-of-the-art multi-task LTL-RL methods: Algorithm Task representation Full obs. Infinite Curriculum Reference LTL2Action Formula syntax tree Vaezipoor et al. (2021) GCRL-LTL Proposition subgoal Qiu et al. (2023) DeepLTL Reach–avoid sequence Jackermeier and Abate (2025) GenZ-LTL Reach–avoid subgoal Guo et al. (2025) SemLTL Semantic LDBA Abate et al. (2026) StructLTL Boolean formula sequence Jackermeier et al. (2026) In contrast to the other methods, GenZ-LTL relies on domain-specific observation reduction functions (see § 5.2) and LTL2Action does not support infinite-horizon tasks. Our reusable curriculum learning implementation can be applied to any method, but the subgoal-based representations of GCRL-LTL and GenZ-LTL do not naturally allow for gradual increases in task complexity, and we hence do not apply curriculum learning (following the original works). See Appendix E for details on methods. 5 Experimental Evaluation Our experimental evaluation is split into two parts. We first demonstrate the efficiency and correctness of Jaxolotl with respect to reference implementations (§ 5.1). We then systematically evaluate existing methods on our benchmark suites to answer three research questions (§ 5.2): (Q1) How do existing approaches compare in terms of general task satisfaction on the curated finite- and infinite-horizon LTL suites? (Q2) What are the capabilities of existing approaches for non-myopic reasoning? (Q3) How do existing algorithms scale with the number of atomic propositions? 5.1 Efficiency and Correctness Computational Efficiency. Figure 3: End-to-end training and evaluation times of Jaxolotl compared to original reference implementations on ZoneEnv. We achieve speedups of up to 220×220× for training and 79×79× for evaluation. We investigate the speed improvements enabled by Jaxolotl by comparing end-to-end training and evaluation times on ZoneEnv with original reference implementations. We focus on DeepLTL and GenZ-LTL, two representative methods with distinct task representations. All timings are measured on standard consumer hardware and include compilation overhead for the JAX implementations. See Section G.1 for full experimental details. As shown in Figure 3, our implementation yields speedups of 34×34× and 47×47× for training a single seed of DeepLTL and GenZ-LTL, respectively. This difference becomes even more pronounced as we increase the number of independent runs, achieving efficiency improvements of 102×102× and 220×220× for 10 seeds. This allows us to train 10 seeds of DeepLTL in 8.2 minutes and GenZ-LTL in 3.7 minutes, compared to 14.0 and 13.4 hours for the original implementations. We further observe significant speedups for evaluation, with 79×79× and 34×34× improvements for DeepLTL and GenZ-LTL, respectively. Section G.1 provides additional comparisons on raw environment throughput. Implementation Validation. Figure 4: Validation of Jaxolotl. (Left) Final ZoneEnv success rates are within ±1.1%± 1.1\% of the reference implementations for all methods. (Right) Overall training dynamics of DeepLTL and GenZ-LTL closely follow the references. To validate the correctness of our implementations, we compare the performance of Jaxolotl against original reference implementations on ZoneEnv. Figure 4 compares final success rates across all methods (left), and training curves for DeepLTL and GenZ-LTL (right). The results demonstrate that our implementations closely match the references. While there are small differences in the training curves, these can be explained by minor low-level implementation details. Crucially, both overall learning behaviour and final success rates accurately reproduce the reference results. Further experimental details are provided in Section G.2. 5.2 Benchmarking Existing Methods We proceed to systematically evaluate existing methods with Jaxolotl. Detailed training parameters are described in Appendix F. The evaluation tasks in our general benchmark suite are drawn from the literature and enriched with curated specifications that cover a wide range of environment-specific behaviour and LTL objectives; see Section D.2 for details. Unless stated otherwise, we train each method using 10 independent random seeds, compute individual policy–task results over 512 episodes, and report 95%95\% Student-t CIs over independent policies (see § 4.2). GenZ-LTL Observation Interfaces. Standard GenZ-LTL uses domain-specific observation-reduction functions that map the current observation sts_t into a task-relative representation, containing only features relevant for the current reach–avoid subgoal (see Appendix E). We denote this configuration by GenZ-LTL† throughout figures and tables, and additionally evaluate GenZ-LTL (unreduced obs.), which conditions on the full observation together with a one-hot encoding of the current subgoal, following Guo et al. (2025). The standard reduction assumes that observations decompose into proposition-specific components and relies on a hand-designed fusion operator to produce fixed reach and avoid features. The unreduced variant removes these assumptions while retaining the rest of the method’s design, and is used when the assumptions do not hold, such as in Warehouse. 5.2.1 General LTL Task Satisfaction (Q1) Figure 5: Aggregate finite-horizon success rates over training. Lines show means across 10 independently trained policies, with shaded 95%95\% Student-t confidence intervals. Table 1: Aggregated benchmark results over the Jaxolotl task suites, averaged over 512 episodes per formula, with 95%95\% CIs over 10 training seeds. Fin.: finite-horizon success rate (0–1); Inf.: completed accepting cycles with fixed episode length. R-S: completed accepting cycles on the reach-stay task suite. Best results are bold, second best underlined, — denotes unsupported configurations. See Section H.1 for per-specification results. LetterWorld ZoneEnv FrankaZoneEnv Warehouse Method Fin. ↑ Inf. ↑ Fin. ↑ Inf. ↑ R-S ↑ Fin. ↑ Inf. ↑ Fin. ↑ Inf. ↑ R-S ↑ LTL2Action 0.42±0.03 — 0.43±0.03 — — 0.04±0.01 — 0.34±0.09 — — GCRL-LTL 0.94±0.00 8.0±0.1 0.93±0.00 5.7±0.1 30.2±3.3 0.55±0.27 8.1±5.9 — — — DeepLTL 0.87±0.01 5.3±0.2 0.92±0.02 3.0±0.3 540.1±48.0 0.51±0.17 4.8±3.3 0.80±0.09 2.6±0.3 618.1±118.7 GenZ-LTL† 0.99±0.00 8.2±0.0 1.00±0.00 6.5±0.2 492.0±50.6 1.00±0.00 35.0±0.6 — — — ↪\; unreduced obs. 0.93±0.00 5.6±0.0 0.96±0.01 5.0±0.1 321.6±59.2 0.45±0.22 5.1±3.6 0.84±0.12 2.2±0.7 102.6±24.8 SemLTL 0.79±0.01 4.2±0.1 0.83±0.02 2.6±0.1 532.9±36.6 0.51±0.05 13.6±1.0 0.83±0.04 0.2±0.1 673.5±30.9 StructLTL 0.90±0.01 5.5±0.2 0.95±0.01 3.7±0.3 572.7±47.7 0.94±0.00 15.3±0.4 0.96±0.01 3.1±0.2 809.9±30.4 Table 1 lists final aggregate results across all task suites, and Figure 5 shows training dynamics on finite-horizon tasks, which we focus on first. We observe that GenZ-LTL performs exceptionally well when provided with a suitable observation reduction function, achieving near perfect success rates. While its unreduced variant obtains high performance on LetterWorld and ZoneEnv, it struggles in more complex environments, where StructLTL dominates among the general methods. GCRL-LTL, DeepLTL, and SemLTL overall perform similarly, but GCRL-LTL is not applicable to Warehouse due to its limited avoidance heuristic (see Appendix E). The early method LTL2Action is consistently outperformed by more modern approaches, showing a distinct gap in success rates. For infinite-horizon tasks, we report the established metric of average completed accepting cycles in the Büchi automaton constructed from the task (Jackermeier and Abate, 2025; Guo et al., 2026). Performance on recurrence tasks (Inf. suite) follows the same general trends as in the finite case. We include reach-stay (i.e. persistence) tasks, which require the agent to infinitely maintain a proposition, for ZoneEnv and Warehouse, where this necessitates meaningful closed-loop behaviour. Here, automata-based methods that account for non-determinism perform best, led by StructLTL. 5.2.2 Non-Myopic Reasoning (Q2) We first isolate non-myopic reasoning in ConveyorWorldSimple-k, a simplified variant of Abate et al. (2026)’s grid-based ConveyorWorld. At the first step, the agent enters one of two one-way conveyor belts, which it cannot leave, leading to rooms A and B. It must then satisfy (1∧(2∧⋯∧k)) F\,( p_1 F\,( p_2 … F\, p_k)), where 1,…,k−1 p_1,…, p_k-1 lie in order along both belts, but k p_k is sampled uniformly from ,\ a, b\, with a only reachable in A and b only in B. The correct belt thus depends on a subgoal k steps ahead, which a non-myopic method should be able to account for. Since the only observation is the agent’s position, GenZ-LTL cannot use observation reduction here. Figure 6 (left) shows success rate over k. For k>1k>1, GenZ-LTL and GCRL-LTL drop to 50%50\%, the success rate of always entering the same belt. Both commit to a belt while pursuing 1 p_1, using an action policy conditioned only on the current subgoal, which is reachable via either belt. GCRL-LTL does select a complete subgoal sequence with its goal-conditioned value function (Appendix E), but its policy cannot distinguish between sequence-dependent ways of reaching the same subgoal. The other methods, which condition on the full task, generally maintain high success rates up to k=32k=32. Such long-horizon reasoning is much harder to learn once exploration and credit assignment become non-trivial (see original ConveyorWorld, Section H.2). Figure 6: (Left) Non-myopic reasoning results on different step variants of ConveyorWorldSimple-k. (Middle) Aggregate finite-horizon success rates on ZoneEnv-NM over training. (Right) Results of scaling the number of atomic propositions in FrankaZoneEnv. To test non-myopic reasoning in a high-dimensional setting, we use a variation of ZonEnv (ZoneEnv-NM, Jackermeier et al., 2026), in which entering a purple zone removes all green zones for the rest of the episode, so the agent must avoid purple zones whenever a green zone is required later. On finite-horizon tasks (Figure 6, middle), GenZ-LTL and GCRL-LTL plateau at 70.0%70.0\% and 66.9%66.9\%, while StructLTL and DeepLTL reach 92.7%92.7\% and 83.6%83.6\%. SemLTL plateaus at 67.5%67.5\% despite conditioning on the full task: this suggests that such conditioning alone does not ensure non-myopic behaviour, as the policy must still learn to exploit this information. LTL2Action struggles to converge (44.2%44.2\%). 5.2.3 Scaling with Atomic Propositions (Q3) We train each method in FrankaZoneEnv with an increasing number of propositions, evaluating on the same finite-horizon tasks (spanning the first 88 propositions) throughout. This isolates the difficulty of training with an increasing number of propositions, while keeping the task difficulty fixed. Figure 6 (right) presents the results. All methods except GenZ-LTL with observation reduction degrade as |AP||AP| grows. We attribute this mainly to grounding: each additional proposition must be associated with its own features in an increasingly complex observation space. This affects myopic methods too; GenZ-LTL (unreduced obs.) and GCRL-LTL lose most of their success rate by |AP|=11|AP|=11. Non-myopic methods must additionally generalise over a set of task sequences that grows exponentially with |AP||AP|: StructLTL, the strongest general method up to |AP|=9|AP|=9, degrades sharply beyond that. GenZ-LTL is unaffected only because its hand-designed observation reduction maps zones to generic “reach” and “avoid” features, sidestepping the grounding problem by construction. 6 Conclusion, Limitations, and Future Work We introduced Jaxolotl, a unified, high-performance benchmark suite for multi-task LTL-RL that enables controlled comparisons of existing methods at scale. Our evaluation shows that existing methods have complementary strengths and limitations. Methods that condition on the full task, such as StructLTL and DeepLTL, reason non-myopically, but, like all methods without observation reduction, they degrade as the number of atomic propositions grows. GenZ-LTL scales by exploiting a useful prior in the form of observation reduction, but this requires manual engineering, is not always applicable, and remains myopic. No evaluated method yet combines non-myopic reasoning, scaling to many propositions, and independence from environment-specific preprocessing. Limitations. Our task suites are finite and curated by hand to capture interesting behaviour, but some of our results may depend on the specific task families that we used. Jaxolotl currently only supports PPO training (as in the supported methods), although its abstractions are algorithm-agnostic. Other restrictions stem from the methods rather than the framework: LTL2Action does not support infinite-horizon tasks, GCRL-LTL and GenZ-LTL with observation reduction cannot be applied to Warehouse, and all methods assume known propositions (for GenZ-LTL, a known space of propositions) and an accurate labelling function with access to privileged state information. Future work. We plan to extend Jaxolotl with off-policy algorithms and additional environments, particularly robotics domains such as contact-rich manipulation, and to scale the benchmark to larger proposition vocabularies and richer task distributions. For methods, the central open problems are relaxing the assumptions above, e.g. through learned or uncertain labelling functions and open-vocabulary settings, and designing a single approach with all three properties identified above. AI use statement In this work, we used generative AI tools to implement methods: they helped create and edit software code, including parts of the environment and method implementations as well as plotting and tooling scripts. We have not used generative AI tools to generate synthetic data, develop conceptual frameworks, propose or refine hypotheses, design or give feedback on experiments, or interpret results; formulating or proving mathematical claims, translation, dataset cleaning and qualitative data analysis are not applicable to this work. Additionally, we used generative AI tools to polish and proof read text for readability and to find typos. We have reviewed all AI-assisted work: an author reviewed every AI-assisted code change, the code is checked by automated tests, and we validated our implementations against re-runs of the official codebases and published results (Section G.2). All AI-assisted text was revised by the authors. We take responsibility for the final content of this work, including text, claims or artifacts produced with the aid of generative AI. Reproducibility statement Our full implementation is available at https://github.com/mathiasj33/jaxolotl, including all environments, algorithms and task suites, together with pre-defined Hydra configurations for the entire benchmark suite. Appendix D describes the environments and task suites, Appendix E the implemented methods, and Appendix F the model architectures, curricula and hyperparameters for each method and environment. Appendix C formalises our evaluation protocol: unless stated otherwise, all results use 10 independent training runs, 512 evaluation episodes per policy and specification, and two-sided 95% Student-t confidence intervals over policies. Section G.1 specifies the hardware and timing protocol for the efficiency comparisons, Section G.2 the re-runs and reported results used to validate our implementations, and Section H.1 reports per-specification results for all benchmarks. Acknowledgments This work was supported by the UKRI Erlangen AI Hub on Mathematical and Computational Foundations of AI (No. EP/Y028872/1). MJ and JC are funded by the EPSRC Centre for Doctoral Training in Autonomous Intelligent Machines and Systems (EP/S024050/1). References Abate et al. (2026) A. Abate, G. De Giacomo, M. Jackermeier, J. Kretínský, M. Prokop, and C. Weinhuber Semantically Labelled Automata for Multi-Task Reinforcement Learning with LTL Instructions. In International Joint Conference on Artificial Intelligence, Cited by: Appendix E, §H.2, §4.4, §5.2.2. Agarwal et al. (2021) R. Agarwal, M. Schwarzer, P. S. Castro, A. Courville, and M. Bellemare Deep Reinforcement Learning at the Edge of the Statistical Precipice. In Advances in Neural Information Processing Systems, Vol. 34, p. 29304–29320. Cited by: Appendix A, Appendix C, §4.2, §4.2. Aksaray et al. (2016) D. Aksaray, A. Jones, Z. Kong, M. Schwager, and C. Belta Q-Learning for robust satisfaction of signal temporal logic specifications. In 2016 IEEE 55th Conference on Decision and Control (CDC), p. 6565–6570. Cited by: Appendix A. Andreas et al. (2017) J. Andreas, D. Klein, and S. Levine Modular Multitask Reinforcement Learning with Policy Sketches. In Proceedings of the 34th International Conference on Machine Learning, p. 166–175. External Links: ISSN 2640-3498 Cited by: Appendix A. Araki et al. (2021) B. Araki, X. Li, K. Vodrahalli, J. Decastro, M. Fry, and D. Rus The Logical Options Framework. In Proceedings of the 38th International Conference on Machine Learning, p. 307–317. External Links: ISSN 2640-3498 Cited by: §2. Bacchus and Kabanza (2000) F. Bacchus and F. Kabanza Using temporal logics to express search control knowledge for planning. Artificial Intelligence 116 (1), p. 123–191. External Links: ISSN 0004-3702 Cited by: Appendix E. Bagatella et al. (2025) M. Bagatella, A. Krause, and G. Martius Directed Exploration in Reinforcement Learning from Linear Temporal Logic. Transactions on Machine Learning Research. Cited by: Appendix A. Bonnet et al. (2024) C. Bonnet, D. Luo, D. Byrne, S. Surana, S. Abramowitz, P. Duckworth, V. Coyette, L. I. Midgley, E. Tegegn, T. Kalloniatis, O. Mahjoub, M. Macfarlane, A. P. Smit, N. Grinsztajn, R. Boige, C. N. Waters, M. A. Mimouni, U. A. M. Sob, R. de Kock, S. Singh, D. Furelos-Blanco, V. Le, A. Pretorius, and A. Laterre Jumanji: a Diverse Suite of Scalable Reinforcement Learning Environments in JAX. In 12th International Conference on Learning Representations, Cited by: §2. Bozkurt et al. (2020) A. K. Bozkurt, Y. Wang, M. M. Zavlanos, and M. Pajic Control Synthesis from Linear Temporal Logic Specifications using Model-Free Reinforcement Learning. In 2020 IEEE International Conference on Robotics and Automation (ICRA), p. 10349–10355. External Links: ISSN 2577-087X Cited by: Appendix A. Bradbury et al. (2018) J. Bradbury, R. Frostig, P. Hawkins, M. J. Johnson, Y. Katariya, C. Leary, D. Maclaurin, G. Necula, A. Paszke, J. VanderPlas, S. Wanderman-Milne, and Q. Zhang JAX: composable transformations of Python+NumPy programs. Cited by: §1. Camacho et al. (2019) A. Camacho, R. T. Icarte, T. Q. Klassen, R. A. Valenzano, and S. A. McIlraith LTL and beyond: Formal languages for reward function specification in reinforcement learning. In Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, IJCAI 2019, p. 6065–6073. Cited by: Appendix A, Appendix A, §2. Carta et al. (2023) T. Carta, C. Romac, T. Wolf, S. Lamprier, O. Sigaud, and P. Oudeyer Grounding Large Language Models in Interactive Environments with Online Reinforcement Learning. In Proceedings of the 40th International Conference on Machine Learning, p. 3676–3713. External Links: ISSN 2640-3498 Cited by: §1. Chan et al. (2019) S. C. Y. Chan, S. Fishman, A. Korattikara, J. Canny, and S. Guadarrama Measuring the Reliability of Reinforcement Learning Algorithms. In International Conference on Learning Representations, Cited by: §4.2. Chevalier-Boisvert et al. (2019) M. Chevalier-Boisvert, D. Bahdanau, S. Lahlou, L. Willems, C. Saharia, T. H. Nguyen, and Y. Bengio BabyAI: A Platform to Study the Sample Efficiency of Grounded Language Learning. In 7th International Conference on Learning Representations, Cited by: Appendix A. Cho et al. (2014) K. Cho, B. van Merriënboer, D. Bahdanau, and Y. Bengio On the Properties of Neural Machine Translation: Encoder–Decoder Approaches. In Proceedings of SSST-8, Eighth Workshop on Syntax, Semantics and Structure in Statistical Translation, p. 103–111. External Links: Document Cited by: Appendix E. Cloete et al. (2026) J. Cloete, M. Jackermeier, I. Havoutis, and A. Abate PlatoLTL: Learning to Generalize Across Symbols in LTL Instructions for Multi-Task RL. arXiv:2601.22891. Cited by: §2. Colas et al. (2018) C. Colas, O. Sigaud, and P. Oudeyer How Many Random Seeds? Statistical Power Analysis in Deep Reinforcement Learning Experiments. arXiv:1806.08295. Cited by: Appendix A. Cosler et al. (2023) M. Cosler, C. Hahn, D. Mendoza, F. Schmitt, and C. Trippel Nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models. In Computer Aided Verification, C. Enea and A. Lal (Eds.), Cham, p. 383–396. External Links: ISBN 978-3-031-37703-7 Cited by: Appendix A. Coward et al. (2024) S. Coward, M. Beukman, and J. N. Foerster JaxUED: A simple and useable UED library in Jax. arXiv:2403.13091. Cited by: Appendix A. De Giacomo et al. (2019) G. De Giacomo, L. Iocchi, M. Favorito, and F. Patrizi Foundations for Restraining Bolts: Reinforcement Learning with LTLf/LDLf Restraining Specifications. Proceedings of the International Conference on Automated Planning and Scheduling 29, p. 128–136. External Links: ISSN 2334-0843 Cited by: Appendix A. Feng et al. (2024) Z. Feng, H. Luan, P. Goyal, and H. Soh LTLDoG: Satisfying Temporally-Extended Symbolic Constraints for Safe Diffusion-Based Planning. IEEE Robotics and Automation Letters 9 (10), p. 8571–8578. External Links: ISSN 2377-3766 Cited by: Appendix A. Freeman et al. (2021) C. D. Freeman, E. Frey, A. Raichuk, S. Girgin, I. Mordatch, and O. Bachem Brax - A differentiable physics engine for large scale rigid body simulation. In 35th Annual Conference on Neural Information Processing Systems Datasets and Benchmarks Track, Cited by: §2. Fuggitti and Chakraborti (2023) F. Fuggitti and T. Chakraborti NL2LTL – a Python Package for Converting Natural Language (NL) Instructions to Linear Temporal Logic (LTL) Formulas. In 37th AAAI Conference on Artificial Intelligence, Cited by: Appendix A. Furelos-Blanco et al. (2023) D. Furelos-Blanco, M. Law, A. Jonsson, K. Broda, and A. Russo Hierarchies of Reward Machines. In International Conference on Machine Learning, Proceedings of Machine Learning Research, Vol. 202, p. 10494–10541. Cited by: Appendix A. Gorsane et al. (2022) R. Gorsane, O. Mahjoub, R. de Kock, R. Dubb, S. Singh, and A. Pretorius Towards a Standardised Performance Evaluation Protocol for Cooperative MARL. In 36th Annual Conference on Neural Information Processing Systems, Cited by: Appendix A. Guo et al. (2025) Z. Guo, I. Işık, H. M. S. Ahmad, and W. Li One Subgoal at a Time: Zero-Shot Generalization to Arbitrary Linear Temporal Logic Requirements in Multi-Task Reinforcement Learning. In Advances in Neural Information Processing Systems, Vol. 38, Main Conference, p. 77500–77529. Cited by: Appendix E, §1, §2, §4.1, §4.4, §5.2. Guo et al. (2026) Z. Guo, İ. Işık, H. M. S. Ahmad, and W. Li SpecRLBench: A Benchmark for Generalization in Specification-Guided Reinforcement Learning. arXiv. External Links: 2604.24729 Cited by: §D.1, §2, §4.3, §5.2.1. Guo et al. (2024) Z. Guo, W. Zhou, and W. Li Temporal Logic Specification-Conditioned Decision Transformer for Offline Safe Reinforcement Learning. In Forty-First International Conference on Machine Learning, Cited by: Appendix A. Hahn et al. (2019) E. M. Hahn, M. Perez, S. Schewe, F. Somenzi, A. Trivedi, and D. Wojtczak Omega-Regular Objectives in Model-Free Reinforcement Learning. In Tools and Algorithms for the Construction and Analysis of Systems, T. Vojnar and L. Zhang (Eds.), Cham, p. 395–412. External Links: ISBN 978-3-030-17462-0 Cited by: Appendix A, §2. Hasanbeig et al. (2018) M. Hasanbeig, A. Abate, and D. Kroening Logically-Constrained Reinforcement Learning. arXiv:1801.08099. Cited by: Appendix A. Hasanbeig et al. (2023) M. Hasanbeig, D. Kroening, and A. Abate Certified reinforcement learning with logic guidance. Artificial Intelligence 322, p. 103949. External Links: ISSN 0004-3702 Cited by: Appendix A, §2. Henderson et al. (2018) P. Henderson, R. Islam, P. Bachman, J. Pineau, D. Precup, and D. Meger Deep Reinforcement Learning That Matters. Proceedings of the AAAI Conference on Artificial Intelligence 32 (1). External Links: ISSN 2374-3468 Cited by: Appendix A, §4.2. Hill et al. (2020) F. Hill, S. Mokra, N. Wong, and T. Harley Human Instruction-Following with Deep Reinforcement Learning via Transfer-Learning from Text. arXiv:2005.09382. Cited by: §1. Huang et al. (2022) S. Huang, R. F. J. Dossa, C. Ye, J. Braga, D. Chakraborty, K. Mehta, and J. G. M. Araújo CleanRL: High-quality Single-file Implementations of Deep Reinforcement Learning Algorithms. Journal of Machine Learning Research 23, p. 274:1–274:18. Cited by: Appendix A. Icarte et al. (2019) R. T. Icarte, E. Waldie, T. Q. Klassen, R. A. Valenzano, M. P. Castro, and S. A. McIlraith Learning Reward Machines for Partially Observable Reinforcement Learning. In 33rd Annual Conference on Neural Information Processing Systems, p. 15497–15508. Cited by: Appendix A. Jackermeier and Abate (2025) M. Jackermeier and A. Abate DeepLTL: Learning to Efficiently Satisfy Complex LTL Specifications for Multi-Task RL. In The Thirteenth International Conference on Learning Representations, Cited by: Appendix E, §G.2, §1, §2, §4.1, §4.1, §4.4, §5.2.1. Jackermeier et al. (2026) M. Jackermeier, M. Giuri, J. Cloete, and A. Abate Zero-Shot Instruction Following in RL via Structured LTL Representations. arXiv. External Links: 2602.14344 Cited by: §D.1, Appendix E, §1, §4.3, §4.4, §5.2.2. Ji et al. (2023) J. Ji, B. Zhang, J. Zhou, X. Pan, W. Huang, R. Sun, Y. Geng, Y. Zhong, J. Dai, and Y. Yang Safety Gymnasium: A Unified Safe Reinforcement Learning Benchmark. In 37th Annual Conference on Neural Information Processing Systems Datasets and Benchmarks Track, Cited by: Appendix A. Ji et al. (2024) J. Ji, J. Zhou, B. Zhang, J. Dai, X. Pan, R. Sun, W. Huang, Y. Geng, M. Liu, and Y. Yang OmniSafe: An Infrastructure for Accelerating Safe Reinforcement Learning Research. Journal of Machine Learning Research 25, p. 285:1–285:6. Cited by: Appendix A. Jordan et al. (2020) S. M. Jordan, Y. Chandak, D. Cohen, M. Zhang, and P. S. Thomas Evaluating the Performance of Reinforcement Learning Algorithms. In 37th International Conference on Machine Learning, Proceedings of Machine Learning Research, Vol. 119, p. 4962–4973. Cited by: Appendix A. Jordan et al. (2024) S. M. Jordan, A. White, B. C. da Silva, M. White, and P. S. Thomas Position: benchmarking is limited in reinforcement learning research. In 41st International Conference on Machine Learning, Proceedings of Machine Learning Research, Vol. 235, p. 22551–22569. Cited by: Appendix A. Jothimurugan et al. (2019) K. Jothimurugan, R. Alur, and O. Bastani A Composable Specification Language for Reinforcement Learning Tasks. In Advances in Neural Information Processing Systems, Vol. 32. Cited by: Appendix A. Kingma and Ba (2015) D. P. Kingma and J. Ba Adam: A method for stochastic optimization. In 3rd International Conference on Learning Representations, Y. Bengio and Y. LeCun (Eds.), Cited by: §F.3. Koyamada et al. (2023) S. Koyamada, S. Okano, S. Nishimori, Y. Murata, K. Habara, H. Kita, and S. Ishii Pgx: Hardware-Accelerated Parallel Game Simulators for Reinforcement Learning. In 37th Annual Conference on Neural Information Processing Systems Datasets and Benchmarks Track, Cited by: Appendix A. Lange (2022) R. T. Lange gymnax: a JAX-based Reinforcement Learning Environment Library. External Links: Link Cited by: §2. León et al. (2021) B. G. León, M. Shanahan, and F. Belardinelli Systematic Generalisation through Task Temporal Logic and Deep Reinforcement Learning. arXiv:2006.08767. Cited by: Appendix A. León et al. (2022) B. G. León, M. Shanahan, and F. Belardinelli In a Nutshell, the Human Asked for This: Latent Goals for Following Temporal Specifications. In International Conference on Learning Representations, Cited by: §2. Li et al. (2017) X. Li, C. Vasile, and C. Belta Reinforcement learning with temporal logic rewards. In 2017 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), p. 3834–3839. External Links: ISSN 2153-0866 Cited by: Appendix A. Liesen et al. (2024) J. Liesen, C. Lu, and R. Lange Rejax. External Links: Link Cited by: §2, §4.1. Liu et al. (2024) J. X. Liu, A. Shah, E. Rosen, M. Jia, G. Konidaris, and S. Tellex Skill Transfer for Temporal Task Specification. In 2024 IEEE International Conference on Robotics and Automation (ICRA), p. 2535–2541. Cited by: §1, §2. Liu et al. (2023) J. X. Liu, Z. Yang, I. Idrees, S. Liang, B. Schornstein, S. Tellex, and A. Shah Grounding Complex Natural Language Commands for Temporal Tasks in Unseen Environments. In Conference on Robot Learning, Cited by: Appendix A. Liu et al. (2022) M. Liu, M. Zhu, and W. Zhang Goal-Conditioned Reinforcement Learning: Problems and Solutions. In Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, p. 5502–5511. External Links: ISBN 978-1-956792-00-3 Cited by: §4.1. Lu et al. (2022) C. Lu, J. G. Kuba, A. Letcher, L. Metz, C. S. de Witt, and J. Foerster Discovered policy optimisation. In Proceedings of the 36th International Conference on Neural Information Processing Systems, NIPS ’22, Red Hook, NY, USA, p. 16455–16468. External Links: ISBN 978-1-7138-7108-8 Cited by: §2, §4.1. Luketina et al. (2019) J. Luketina, N. Nardelli, G. Farquhar, J. N. Foerster, J. Andreas, E. Grefenstette, S. Whiteson, and T. Rocktäschel A survey of reinforcement learning informed by natural language. In Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, p. 6309–6317. Cited by: Appendix A. Matthews et al. (2024) M. T. Matthews, M. Beukman, B. Ellis, M. Samvelyan, M. T. Jackson, S. Coward, and J. N. Foerster Craftax: A Lightning-Fast Benchmark for Open-Ended Reinforcement Learning. In 41st International Conference on Machine Learning, Proceedings of Machine Learning Research, Vol. 235, p. 35104–35137. Cited by: §2. Matthews et al. (2025) M. T. Matthews, M. Beukman, C. Lu, and J. N. Foerster Kinetix: Investigating the Training of General Agents through Open-Ended Physics-Based Control Tasks. In 13th International Conference on Learning Representations, Cited by: Appendix A. Meng and Fan (2025) Y. Meng and C. Fan TeLoGraF: Temporal Logic Planning via Graph-encoded Flow Matching. In 42nd International Conference on Machine Learning, Proceedings of Machine Learning Research, Vol. 267. Cited by: Appendix A. Nikulin et al. (2024) A. Nikulin, V. Kurenkov, I. Zisman, A. Agarkov, V. Sinii, and S. Kolesnikov XLand-MiniGrid: Scalable Meta-Reinforcement Learning Environments in JAX. In 38th Annual Conference on Neural Information Processing Systems Datasets and Benchmarks Track, Cited by: §2. Oh et al. (2017) J. Oh, S. Singh, H. Lee, and P. Kohli Zero-Shot Task Generalization with Multi-Task Deep Reinforcement Learning. In Proceedings of the 34th International Conference on Machine Learning, p. 2661–2670. External Links: ISSN 2640-3498 Cited by: Appendix A. Pannacci et al. (2026) M. Pannacci, A. Fanti, E. Umili, and R. Capobianco Grounding LTL Tasks in Sub-Symbolic RL Environments for Zero-Shot Generalization. arXiv:2602.09761. Cited by: Appendix A. Patterson et al. (2024) A. Patterson, S. Neumann, M. White, and A. White Empirical Design in Reinforcement Learning. Journal of Machine Learning Research 25, p. 318:1–318:63. Cited by: Appendix A. Peng et al. (2026) Y. Peng, P. Wang, S. S. Zhan, Y. Lyu, Z. Ni, J. Yan, F. Wong, R. Jiao, H. Yin, X. Cao, H. Shao, M. Li, R. Zhang, and Q. Zhu MANIGUARD: a benchmark and data suite for specification-grounded safety evaluation and improvement of robotic manipulation. arXiv:2608.17386. Cited by: Appendix A, §2. Pignatelli et al. (2025) E. Pignatelli, J. Liesen, R. T. Lange, C. Lu, P. S. Castro, and L. Toni NAVIX: Scaling MiniGrid Environments with JAX. In 39th Annual Conference on Neural Information Processing Systems, Cited by: §2. Pnueli (1977) A. Pnueli The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science (SFCS 1977), p. 46–57. External Links: ISSN 0272-5428 Cited by: Appendix B, §1, §3. Press et al. (2021) O. Press, N. Smith, and M. Lewis Train Short, Test Long: Attention with Linear Biases Enables Input Length Extrapolation. In International Conference on Learning Representations, Cited by: Appendix E. Qiu et al. (2023) W. Qiu, W. Mao, and H. Zhu Instructing Goal-Conditioned Reinforcement Learning Agents with Temporal Logic Objectives. In Thirty-Seventh Conference on Neural Information Processing Systems, Cited by: Appendix E, §1, §2, §4.4. Raffin et al. (2021) A. Raffin, A. Hill, A. Gleave, A. Kanervisto, M. Ernestus, and N. Dormann Stable-Baselines3: Reliable Reinforcement Learning Implementations. Journal of Machine Learning Research 22, p. 268:1–268:8. Cited by: Appendix A. Rumelhart et al. (1986) D. E. Rumelhart, G. E. Hinton, and R. J. Williams Learning representations by back-propagating errors. Nature 323 (6088), p. 533–536. Cited by: §F.1. Rutherford et al. (2024) A. Rutherford, B. Ellis, M. Gallici, J. Cook, A. Lupu, G. Ingvarsson, T. Willi, R. Hammond, A. Khan, C. S. de Witt, A. Souly, S. Bandyopadhyay, M. Samvelyan, M. Jiang, R. Lange, S. Whiteson, B. Lacerda, N. Hawes, T. Rocktäschel, C. Lu, and J. Foerster JaxMARL: Multi-Agent RL Environments and Algorithms in JAX. Advances in Neural Information Processing Systems 37, p. 50925–50951. Cited by: §2. Sadigh et al. (2014) D. Sadigh, E. S. Kim, S. Coogan, S. S. Sastry, and S. A. Seshia A learning based approach to control synthesis of Markov decision processes for linear temporal logic specifications. In 53rd IEEE Conference on Decision and Control, p. 1091–1096. External Links: ISSN 0191-2216 Cited by: Appendix A. Schlichtkrull et al. (2018) M. S. Schlichtkrull, T. N. Kipf, P. Bloem, R. van den Berg, I. Titov, and M. Welling Modeling relational data with graph convolutional networks. In ESWC, Lecture Notes in Computer Science, Vol. 10843, p. 593–607. Cited by: Appendix E. Schulman et al. (2017) J. Schulman, F. Wolski, P. Dhariwal, A. Radford, and O. Klimov Proximal Policy Optimization Algorithms. arXiv:1707.06347. Cited by: §4.1. Serrano-Muñoz et al. (2023) A. Serrano-Muñoz, D. Chrysostomou, S. Bøgh, and N. Arana-Arexolaleiba Skrl: Modular and Flexible Library for Reinforcement Learning. Journal of Machine Learning Research 24, p. 254:1–254:9. Cited by: Appendix A. Shao and Kwiatkowska (2023) D. Shao and M. Kwiatkowska Sample efficient model-free reinforcement learning from LTL specifications with optimality guarantees. In Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence, p. 4180–4189. Cited by: Appendix A. Sickert et al. (2016) S. Sickert, J. Esparza, S. Jaax, and J. Křetínský Limit-Deterministic Büchi Automata for Linear Temporal Logic. In Computer Aided Verification, Lecture Notes in Computer Science, p. 312–332. External Links: ISBN 978-3-319-41540-6 Cited by: Appendix A. Sohn et al. (2018) S. Sohn, J. Oh, and H. Lee Hierarchical Reinforcement Learning for Zero-shot Generalization with Subtask Dependencies. In 32nd Annual Conference on Neural Information Processing Systems, p. 7156–7166. Cited by: Appendix A. Student (1908) Student The probable error of a mean. Biometrika 6 (1), p. 1–25. Cited by: §4.2. Subramanian et al. (2025) V. Subramanian, R. Kushwah, S. Roy, and S. Bansal Inductive generalization in reinforcement learning from specifications. In Automated Technology for Verification and Analysis, Lecture Notes in Computer Science, Vol. 16145, p. 277–298. Cited by: Appendix A. Todorov et al. (2012) E. Todorov, T. Erez, and Y. Tassa MuJoCo: A physics engine for model-based control. In 2012 IEEE/RSJ International Conference on Intelligent Robots and Systems, p. 5026–5033. Cited by: §D.1, §4.3. Toledo (2024) E. Toledo Stoix: Distributed Single-Agent Reinforcement Learning End-to-End in JAX. External Links: Link Cited by: Appendix A. Toro Icarte et al. (2018a) R. Toro Icarte, T. Q. Klassen, R. Valenzano, and S. A. McIlraith Teaching Multiple Tasks to an RL Agent using LTL. In Proceedings of the 17th International Conference on Autonomous Agents and MultiAgent Systems, AAMAS ’18, p. 452–461. Cited by: Appendix A. Toro Icarte et al. (2018b) R. Toro Icarte, T. Q. Klassen, R. Valenzano, and S. A. McIlraith Using Reward Machines for High-Level Task Specification and Decomposition in Reinforcement Learning. In Proceedings of the 35th International Conference on Machine Learning, p. 2107–2116. External Links: ISSN 2640-3498 Cited by: Appendix A. Toro Icarte et al. (2022) R. Toro Icarte, T. Q. Klassen, R. Valenzano, and S. A. McIlraith Reward Machines: Exploiting Reward Function Structure in Reinforcement Learning. Journal of Artificial Intelligence Research 73, p. 173–208. External Links: ISSN 1076-9757 Cited by: Appendix A, §2. Towers et al. (2025) M. Towers, A. Kwiatkowski, J. U. Balis, G. D. Cola, T. Deleu, M. Goulão, K. Andreas, M. Krimmel, A. Kg, R. D. L. Perez-Vicente, J. K. Terry, A. Pierré, S. V. Schulhoff, J. J. Tai, H. Tan, and O. G. Younis Gymnasium: A Standard Interface for Reinforcement Learning Environments. In The Thirty-ninth Annual Conference on Neural Information Processing Systems Datasets and Benchmarks Track, Cited by: Appendix A. Umili et al. (2024) E. Umili, F. Argenziano, and R. Capobianco Neural Reward Machines. arXiv. External Links: 2408.08677 Cited by: Appendix A. Vaezipoor et al. (2021) P. Vaezipoor, A. C. Li, R. A. T. Icarte, and S. A. Mcilraith LTL2Action: Generalizing LTL Instructions for Multi-Task RL. In Proceedings of the 38th International Conference on Machine Learning, p. 10497–10508. External Links: ISSN 2640-3498 Cited by: §D.1, §D.1, Appendix E, §1, §2, §4.1, §4.3, §4.3, §4.4. Vaswani et al. (2017) A. Vaswani, N. Shazeer, N. Parmar, J. Uszkoreit, L. Jones, A. N. Gomez, Ł. ukasz Kaiser, and I. Polosukhin Attention is All you Need. In Advances in Neural Information Processing Systems, Vol. 30. Cited by: Appendix E. Voloshin et al. (2022) C. Voloshin, H. Le, S. Chaudhuri, and Y. Yue Policy Optimization with Linear Temporal Logic Constraints. Advances in Neural Information Processing Systems 35, p. 17690–17702. Cited by: Appendix A. Voloshin et al. (2023) C. Voloshin, A. Verma, and Y. Yue Eventual Discounting Temporal Logic Counterfactual Experience Replay. In Proceedings of the 40th International Conference on Machine Learning, p. 35137–35150. External Links: ISSN 2640-3498 Cited by: Appendix A, §2. Xu and Fekri (2024) D. Xu and F. Fekri Generalization of Temporal Logic Tasks via Future Dependent Options. In RLBRew Workshop, Reinforcement Learning Conference, Cited by: Appendix A. Xu et al. (2020) Z. Xu, I. Gavran, Y. Ahmad, R. Majumdar, D. Neider, U. Topcu, and B. Wu Joint Inference of Reward Machines and Policies for Reinforcement Learning. In 30th International Conference on Automated Planning and Scheduling, p. 590–598. Cited by: Appendix A. Yadan (2019) O. Yadan Hydra - A framework for elegantly configuring complex applications. Note: Github Cited by: §4.1. Yalcinkaya et al. (2024) B. Yalcinkaya, N. Lauffer, M. Vazquez-Chanlatte, and S. A. Seshia Compositional Automata Embeddings for Goal-Conditioned Reinforcement Learning. In The Thirty-eighth Annual Conference on Neural Information Processing Systems, Cited by: Appendix A. Yang et al. (2022) C. Yang, M. L. Littman, and M. Carbin On the (In)Tractability of reinforcement learning for LTL objectives. In Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, L. D. Raedt (Ed.), p. 3650–3658. Cited by: Appendix A. Zaheer et al. (2017) M. Zaheer, S. Kottur, S. Ravanbakhsh, B. Poczos, R. R. Salakhutdinov, and A. J. Smola Deep Sets. In Advances in Neural Information Processing Systems, Vol. 30. Cited by: Appendix E. Zakka et al. (2025) K. Zakka, B. Tabanpour, Q. Liao, M. Haiderbhai, S. Holt, J. Y. Luo, A. Allshire, E. Frey, K. Sreenath, L. A. Kahrs, C. Sferrazza, Y. Tassa, and P. Abbeel MuJoCo Playground. arXiv:2502.08844. Cited by: §2. Zhang et al. (2024) H. Zhang, H. Wang, X. Huang, W. Chen, and Z. Kan Exploiting Hybrid Policy in Reinforcement Learning for Interpretable Temporal Logic Manipulation. In IEEE/RSJ International Conference on Intelligent Robots and Systems, Cited by: Appendix A. Zhang et al. (2023) H. Zhang, H. Wang, and Z. Kan Exploiting Transformer in Sparse Reward Reinforcement Learning for Interpretable Temporal Logic Motion Planning. IEEE Robotics and Automation Letters 8 (8), p. 4831–4838. External Links: ISSN 2377-3766 Cited by: Appendix A. Zoellner et al. (2026) M. Zoellner, A. Manganaris, A. H. Qureshi, and R. Paleja Hint2^2: Hierarchical World Models for Inference-Time Temporal Logic Guidance. arXiv:2608.13678. Cited by: Appendix A. Appendix A Extended Related Work RL from Temporal Logic Specifications. A large body of work uses LTL to specify a single, fixed task to an RL agent. The standard approach translates the formula into an automaton, typically a limit-deterministic Büchi automaton (LDBA; Sickert et al., 2016), and learns a policy on the product of the MDP and the automaton (Sadigh et al., 2014; Hasanbeig et al., 2018; Hasanbeig et al., 2023; Hahn et al., 2019; Bozkurt et al., 2020). Subsequent work develops reward and discounting schemes with optimality guarantees (Voloshin et al., 2022; Voloshin et al., 2023; Shao and Kwiatkowska, 2023), improves exploration under the resulting sparse rewards (Bagatella et al., 2025), and characterises the fundamental limits of learning LTL objectives (Yang et al., 2022). Related work uses quantitative semantics of temporal logics as dense rewards (Aksaray et al., 2016; Li et al., 2017; Jothimurugan et al., 2019), or specifies tasks over finite traces (Camacho et al., 2019; De Giacomo et al., 2019). These methods learn a separate policy per specification, whereas we consider policies that generalise zero-shot to unseen specifications. Reward Machines. Reward machines (RMs) expose the structure of a reward function as a finite-state machine (Toro Icarte et al., 2018b; Toro Icarte et al., 2022), enabling counterfactual experience sharing across machine states and automated reward shaping. RMs can be constructed from formal specifications (Camacho et al., 2019), learned from experience (Icarte et al., 2019; Xu et al., 2020), composed hierarchically (Furelos-Blanco et al., 2023), or grounded in raw observations via neural relaxations (Umili et al., 2024). Since automata derived from LTL formulae can be viewed as RMs, many multi-task LTL-RL methods build on this perspective, although RM methods themselves typically target a single fixed machine. Further LTL-Based Multi-Task RL Methods. Toro Icarte et al. (2018a) learn options for co-safe LTL subformulae and use progression to transfer them to new tasks composed of known subformulae, while León et al. (2021) study systematic generalisation to unseen formulae. Other work encodes specifications with transformers (Zhang et al., 2023; Zhang et al., 2024), conditions policies on pretrained embeddings of compositional DFAs (Yalcinkaya et al., 2024), learns future-dependent options (Xu and Fekri, 2024), or studies inductive generalisation from specifications (Subramanian et al., 2025). Most of these methods, like those we implement, assume access to a ground-truth labelling function mapping observations to propositions; Pannacci et al. (2026) relax this by jointly learning a symbol grounder alongside the policy. Instruction Following and Multi-Task RL. Beyond formal languages, instruction-following agents have been conditioned on natural language, policy sketches, and subtask graphs (Oh et al., 2017; Andreas et al., 2017; Sohn et al., 2018; Chevalier-Boisvert et al., 2019); see Luketina et al. (2019) for a survey. Natural language is flexible but ambiguous, whereas LTL provides precise semantics and automata that track task progress. Translating natural language into LTL is an active area of research (Cosler et al., 2023; Fuggitti and Chakraborti, 2023; Liu et al., 2023), suggesting that LTL-conditioned policies can serve as a backbone for language-driven agents. Offline and Generative Approaches. A complementary line of work satisfies temporal logic specifications with generative models trained on offline data, including diffusion-based planners guided by LTL (Feng et al., 2024; Zoellner et al., 2026), flow matching over graph-encoded specifications (Meng and Fan, 2025), and specification-conditioned decision transformers (Guo et al., 2024). In robotic manipulation, ManiGuard (Peng et al., 2026) evaluates vision-language-action (VLA) policies on LTLf tasks. These settings assume access to demonstration data or pretrained models, whereas Jaxolotl targets online RL. RL Software. General-purpose libraries such as Gymnasium (Towers et al., 2025), Stable-Baselines3 (Raffin et al., 2021), CleanRL (Huang et al., 2022), and skrl (Serrano-Muñoz et al., 2023), as well as safe RL libraries such as Safety-Gymnasium (Ji et al., 2023) and OmniSafe (Ji et al., 2024), do not natively represent temporally extended task specifications. LTL-based RL codebases therefore typically implement automaton construction and progression symbolically in Python on top of these libraries, which runs on the CPU and prevents end-to-end JIT compilation. In addition to the JAX frameworks discussed in Section 2, the ecosystem includes Pgx (Koyamada et al., 2023), Kinetix (Matthews et al., 2025), Stoix (Toledo, 2024), and JaxUED (Coward et al., 2024), none of which support LTL-specified tasks. Evaluation Methodology. Concerns about the reliability of empirical RL results are long-standing (Henderson et al., 2018; Colas et al., 2018). Recommended remedies include performance profiles and aggregate metrics with interval estimates (Jordan et al., 2020; Agarwal et al., 2021), careful experimental design (Patterson et al., 2024), and community-wide standardised protocols (Gorsane et al., 2022; Jordan et al., 2024). Jaxolotl adopts these recommendations, and its computational efficiency makes the required number of seeds and evaluation episodes practical. Appendix B Semantics of LTL LTL semantics are defined over infinite words σ∈(2AP)ωσ∈(2^AP)^ω. The satisfaction relation σ⊧φσ is defined recursively as (Pnueli, 1977): σ σ ⊧⊤ σ σ ⊧ a iff ∈σ0 a∈ _0 σ σ ⊧φ1∧φ2 _1 _2 iff σ⊧φ1∧σ⊧φ2 σ _1 σ _2 σ σ ⊧¬φ iff σ⊧̸φ σ σ σ ⊧φ X\, iff σ1…⊧φ _1… σ σ ⊧φ1φ2 _1\; U\; _2 iff ∃j≥0.σj…⊧φ2∧∀0≤i<j.σi…⊧φ1. ∃ j≥ 0.\; _j… _2 ∀ 0≤ i<j.\; _i… _1. Appendix C Evaluation Protocol This appendix formalises the evaluation protocol summarised in Section 4.2, which adapts the evaluation principles of Agarwal et al. (2021) to generalist policies evaluated on a fixed set of benchmark tasks. Since each training run yields a single policy that is evaluated on every task, we treat independently trained policies, rather than policy–task pairs, as the statistical units. Concretely, let Φ=Φfin⊎Φ∞ = _fin _∞ denote a fixed set of finite- and infinite-horizon benchmark tasks for a given environment, let S denote the number of independently trained policies (i.e. seeds), and let E be the number of evaluation episodes per policy and specification. We first estimate x^s,φ=1E∑e=1Emφ(τs,φ,e), x_s, = 1E _e=1^Em_ ( _s, ,e), where mφm_ is the evaluation metric for φ . For finite-horizon specifications, mφ(τ)≔1[τ⊧φ]m_ (τ) 1[τ ] directly measures satisfaction; for infinite-horizon specifications we use the number of visits to accepting states. Since the initial state of every evaluation episode is drawn from the environment’s episode initialisation distribution (Section D.1), x^s,φ x_s, is an unbiased estimate of the expected performance of policy πs _s on φ under this distribution. For a nonempty subset Ψ⊆Φ of specifications with comparable metrics (e.g. all finite-horizon tasks), we define the per-policy aggregate x^s,Ψ≔|Ψ|−1∑φ∈Ψx^s,φ x_s, | |^-1 _ ∈ x_s, . The overall point estimates across all evaluated runs are μ^φ≔1S∑s=1Sx^s,φ,μ^Ψ≔1S∑s=1Sx^s,Ψ. μ_ 1S _s=1^S x_s, , μ_ 1S _s=1^S x_s, . Aggregating task scores within each policy before estimating uncertainty preserves the correlations between scores obtained from the same training run. To account for uncertainty across seeds, we report two-sided 95% Student-t confidence intervals. For either an individual specification or a task-set aggregate, let zsz_s denote the corresponding policy-level estimate, and define z¯≔1S∑s=1Szs,σ^z2≔1S−1∑s=1S(zs−z¯)2. z 1S _s=1^Sz_s, σ_z^2 1S-1 _s=1^S(z_s- z)^2. The confidence interval is then [z¯−tS−1,0.975σ^zS,z¯+tS−1,0.975σ^zS], [ z-t_S-1,0.975 σ_z S,\ z+t_S-1,0.975 σ_z S ], where tν,qt_ν,q denotes the q-quantile of the Student-t distribution with ν degrees of freedom. We use S=10S=10 independent training runs. These intervals are exact for normally distributed policy-level estimates and otherwise approximate; they quantify uncertainty under repeated training and evaluation, conditional on the fixed benchmark tasks. For performance curves, we apply the same procedure at each training checkpoint, obtaining pointwise rather than simultaneous confidence intervals. Appendix D Environments and Task Suites D.1 Environments We provide a brief overview of the four main environments supported in Jaxolotl. LetterWorld (Vaezipoor et al., 2021). LetterWorld is a discrete navigation environment on a 7×77× 7 grid on which 12 distinct letters are scattered, each appearing in two randomly chosen cells. The letters constitute the atomic propositions: a proposition holds exactly when the agent occupies a cell containing the corresponding letter, so every reachable assignment is a singleton set or the empty set. The agent starts each episode in a fixed corner cell and moves in the four cardinal directions via a discrete action space; the grid is toroidal, so moving across an edge wraps the agent around to the opposite side. The observation is an egocentric view of the entire grid, centred on the agent, encoded as one-hot letter channels plus an additional agent channel. Letter placements are resampled at the beginning of every episode, rejecting layouts in which some cell cannot be reached without crossing a letter; this guarantees that tasks requiring the avoidance of certain letters remain solvable. ZoneEnv (Vaezipoor et al., 2021). ZoneEnv consists of a bounded 6.6×6.6m6.6× 6.6\,m plane containing eight non-overlapping circular zones of radius 0.4m0.4\,m, two of each of four colours. The colours form the atomic propositions: a proposition holds while the agent is inside a zone of the corresponding colour, and since zones never overlap, all reachable assignments are singletons or empty. The agent is a point robot that applies a forward force along its current heading and controls its angular velocity through a 2-dimensional continuous action space. Observations combine proprioceptive information (acceleration, velocity, and angular velocity) with a per-colour LiDAR that partitions the agent’s surroundings into 16 evenly spaced angular bins and reports an exponentially decaying signal based on the distance to the nearest zone of each colour in each bin. Both the zone layout and the initial agent pose are randomly sampled within a central 5×5m5× 5\,m spawn area at the start of every episode, with zone centres kept at least 1.1m1.1\,m apart, and episodes terminate prematurely if the agent leaves the arena. Our implementation replaces the MuJoCo-based point robot of the original environment with lightweight point-mass dynamics that retain the original control interface. FrankaZoneEnv (Guo et al., 2026). FrankaZoneEnv is a 3D robotic manipulation environment in which a 7-DoF Franka Panda arm, simulated with MuJoCo XLA (MJX; Todorov et al., 2012), must visit coloured zones with its end effector. The zones are virtual spheres of radius 7cm7\,cm without contact geometry, one per colour (eight by default), placed uniformly at random in a 0.52×0.64×0.48m0.52× 0.64× 0.48\,m box within the arm’s reachable workspace; rejection sampling ensures that the sphere centres are at least 14cm14\,cm apart, reachable, and clear of the initial end-effector position. Each colour is an atomic proposition that holds while the grasp centre lies inside the corresponding sphere, so all reachable assignments are singletons or empty. The 6-dimensional continuous action specifies Cartesian pose increments (up to 2cm2\,cm of translation and 0.1rad0.1\,rad of rotation per step) of the end effector, which a differential inverse-kinematics controller converts into joint-space position targets. Observations consist of arm proprioception (joint angles and velocities, the actual and commanded end-effector poses, and an inverse-kinematics feasibility flag) together with range–bearing information for every zone, i.e. the relative position of and distance to each sphere. The initial arm configuration is perturbed around a home pose with up to ±0.15rad± 0.15\,rad of per-joint noise, and the zone centres are resampled at the beginning of each episode. The number of colours is configurable, which makes the environment particularly suited to studying how methods scale with the number of propositions. Warehouse (Jackermeier et al., 2026). The Warehouse environment couples continuous navigation with object interaction. A point robot with the same dynamics as in ZoneEnv moves in a bounded 6.6×6.6m6.6× 6.6\,m world containing four vases and four crates at randomised positions, along with three fixed axis-aligned rectangular regions: region A (2.2×2.2m2.2× 2.2\,m), region B (2.9×1.5m2.9× 1.5\,m), and a door area (1.6×0.8m1.6× 0.8\,m). The action space is hybrid: at every step, the agent applies a continuous (force, angular velocity) pair and simultaneously selects one of five discrete interactions (do nothing, pick up or drop a vase, pick up or drop a crate). An object can be picked up when the agent is within a radius of 0.2m0.2\,m of it, and a carried object is deposited at the agent’s current position when dropped, after which a 10-step cooldown prevents an immediate pickup. The five atomic propositions indicate whether the agent is inside each of the three regions and whether it is currently carrying a vase or a crate. In contrast to the other environments, multiple propositions can hold simultaneously (e.g. carrying both a vase and a crate while inside region A), giving rise to non-singleton assignments; since the regions are disjoint and at most one object of each type can be carried, 16 assignments are reachable in total. Observations comprise proprioception, the agent’s global position, a per-object-type egocentric LiDAR with 16 angular bins, direction vectors towards the three regions, and binary carrying flags. Episodes terminate prematurely if the agent leaves the world. D.2 Task Suites Table 2, Table 3, and Table 4 present the finite-horizon, infinite-horizon, and reach-stay LTL specifications used for evaluation in Section 5.2.1, respectively. Table 2 also includes the specifications used to compute the evaluation curves for ZoneEnv-NM in Section 5.2.2. For LetterWorld, ZoneEnv, Warehouse, and ZoneEnv-NM, these specifications were largely taken from the literature, and augmented with a broader coverage of more challenging tasks. For FrankaZoneEnv, the specifications are new and span a broad range of complex and interesting temporally extended behaviours; the pool of eight unique propositions allows for much greater compositional complexity compared to, e.g., ZoneEnv (which only names four unique propositions in its standard formula set). As stated in Section 5.2.2, ConveyorWorld and ConveyorWorldSimple evaluate on sequential reachability specifications of the form (1∧(2∧⋯∧k))( p_1 F\,( p_2 … F\, p_k)) where i≠j p_i≠ p_j, and propositions up to k−1 p_k-1 are accessible in both rooms, but k∼U(,) p_k U(\ a, b\) is sampled evenly between a (only accessible in room A) and b (only accessible in room B). Appendix E Supported LTL-RL Algorithms We provide a brief characterisation of the multi-task LTL-RL methods supported in Jaxolotl, focusing on their task representations, task encoder architectures, and evaluation-time procedures. The corresponding training and model hyperparameters are listed in Appendix F.3. LTL2Action (Vaezipoor et al., 2021). LTL2Action conditions the policy directly on the syntax tree of the LTL formula and keeps the task Markovian via formula progression (Bacchus and Kabanza, 2000): after every environment step, the formula is rewritten into an equivalent residual formula expressing what remains to be satisfied given the observed assignment, and the task counts as satisfied (or violated) once the formula progresses to ⊤ (or ⊥ ). The syntax tree of the current formula is encoded with a relational graph convolutional network (RGCN; Schlichtkrull et al., 2018): every operator and proposition corresponds to a node with a learned embedding, and messages are passed from children to parents along three edge relations (unary operand, left and right binary operands) for a fixed number of rounds with shared weights, after which the embedding of the root node serves as the task embedding. Since messages only flow upwards, the number of message-passing rounds bounds the formula depth visible at the root, and must therefore be chosen to cover the deepest formulae in the task distribution. The policy is trained on randomly sampled reach–avoid formulae with a curriculum of increasing depth. Because progression only signals success for specifications that resolve to ⊤ after finitely many steps, LTL2Action does not support infinite-horizon tasks. In our implementation, the closure of each formula under progression is precomputed offline, reducing run-time progression to indexing a static transition table; at evaluation time, a new specification requires no further machinery, as the same progression mechanism applies unchanged. GCRL-LTL (Qiu et al., 2023). GCRL-LTL trains a goal-conditioned policy to reach individual atomic propositions, sampled uniformly at random and presented to the policy as a learned embedding of the goal proposition; no LTL formulae or curriculum are involved during policy training. Once the policy has been trained, a goal-conditioned value function (GCVF) is fitted in a second phase: it estimates the value of pursuing a new goal g′g from states encountered while travelling towards a goal g, and, following the official implementation, is trained by regressing onto the critic’s value estimates along successful trajectories of the frozen policy. At evaluation time, a given LTL specification is converted to an LDBA, and a depth-first search extracts candidate reach–avoid paths representing accepting runs from every automaton state, with accepting loops unrolled for infinite-horizon tasks. Whenever the automaton state changes, GCRL-LTL scores each candidate path by accumulating negative log-values along its subgoals—the first edge using the policy’s critic, and subsequent edges using the GCVF—and directs the goal-conditioned policy towards the first subgoal of the best-scoring path; ε -transitions of the LDBA are taken automatically whenever the plan calls for them. Avoidance is handled heuristically: if the value estimate for an avoid proposition is sufficiently high, the action that the policy would greedily take towards it is masked out of the action distribution. Since this masking operates on discrete action logits, GCRL-LTL runs on discretised variants of the continuous-control environments. The proposition-based avoidance heuristic furthermore does not translate to environments with more complex avoidance requirements, making GCRL-LTL not applicable to Warehouse. DeepLTL (Jackermeier and Abate, 2025). DeepLTL conditions the policy on sequences of reach–avoid pairs of assignment sets, which represent accepting runs of an LDBA and inform the policy of the subgoals that remain until satisfaction. Training requires no LTL formulae: the policy learns on randomly sampled reach–avoid sequences under a curriculum of increasing depth, including sequences that begin with an ε -transition and repeat their final element to capture stability ( F\, G\,-type) tasks. To embed a sequence, each assignment is mapped to a learned embedding (with a dedicated token for ε -transitions), the reach and avoid sets of every step are pooled by a permutation-invariant deep sets network (Zaheer et al., 2017), and the resulting per-step representations are processed by a gated recurrent unit (GRU; Cho et al., 2014) traversed from the end of the sequence backwards, so that its final hidden state is aligned with the current subgoal. The ε -transitions of the LDBA, which resolve its non-determinism, are exposed to the agent as an additional binary action that advances the automaton without affecting the environment. At evaluation time, a given specification is converted into an LDBA, and a depth-first search enumerates the reach–avoid sequences corresponding to possible accepting runs from every automaton state, unrolling accepting loops for infinite-horizon tasks. Whenever the automaton state changes, the agent selects among the candidate sequences of the new state using its learned value function. Since the policy is trained on arbitrary sequences, it generalises across automata, and hence across LTL specifications. GenZ-LTL (Guo et al., 2025). GenZ-LTL is a decomposition-based method that handles one reach–avoid subgoal at a time, where a subgoal consists of a single assignment to reach and a set of assignments to avoid. Instead of learning a task embedding, GenZ-LTL relies on hand-designed observation reduction functions that map the observation into a subgoal-relative form containing only the features relevant to the current subgoal, rendering the policy invariant to the number and identity of propositions. In ZoneEnv, for instance, the per-colour LiDARs are reduced to the LiDAR of the reach colour and an element-wise maximum over the LiDARs of the avoid colours; in LetterWorld, the per-letter grid channels are collapsed into a single channel marking reach and avoid cells; and in FrankaZoneEnv, the range–bearing features of the reach zone are retained alongside the avoid zones sorted by distance. This reduction assumes that observations decompose into proposition-specific components; where this does not hold, the unreduced variant conditions on the full observation together with one-hot encodings of the subgoal. The policy is trained on randomly sampled subgoals without a curriculum, using a safe-RL formulation: a Lagrangian-constrained variant of PPO in which a cost critic estimates the (maximum-based, reachability-style) probability of violating the avoid set, weighted against the reward objective by a state-dependent Lagrange-multiplier network. At evaluation time, a specification is converted into an LDBA, and the first reach–avoid pair of every accepting run from the current automaton state yields the set of candidate subgoals. The agent selects the subgoal maximising the learned value minus the multiplier-weighted cost estimate, re-selects when the automaton state changes or a subgoal times out, and takes ε -transitions automatically whenever doing so is safe. SemLTL (Abate et al., 2026). SemLTL conditions the policy on semantic state labels of an LDBA. Each specification is compiled into a semantically labelled LDBA, in which every automaton state carries a feature vector summarising the semantics of its associated formulae; crucially, semantically equivalent states of different automata receive identical labels, which is what enables generalisation across specifications. The dimensionality of this label vector (the semantic input size) depends on the number of atomic propositions, and a single learned linear projection maps it to the task embedding. To resolve the non-determinism of the LDBA, the policy additionally receives the labels of all states reachable via ε -transitions, and a dedicated categorical action head chooses at every step between acting in the environment and jumping to one of the ε -successors. The policy is trained on sampled LTL formulae—including infinite-horizon G\, F\,- and F\, G\,-type tasks—under a curriculum of increasing complexity, receiving reward for accepting transitions of the automaton and a penalty for entering rejecting sink states. At evaluation time, a new specification is simply compiled into its semantically labelled LDBA and the policy acts directly on the resulting labels; no search or planning is involved. StructLTL (Jackermeier et al., 2026). StructLTL conditions the policy on sequences of reach–avoid pairs of Boolean formulae over propositions, which represent the transitions along accepting runs of an LDBA: the reach formula is a conjunction of literals that characterises the transition to be taken, while the avoid formula is a disjunction of such conjunctions that must not be triggered. The encoder mirrors this logical structure hierarchically: propositions receive learned embeddings, with negation applied as a learned linear transform; a first deep sets module (the clause network) pools the literals of each conjunction; a second deep sets module (the disjunct network) pools the clause embeddings of each avoid formula; and the resulting per-step subgoal representations are combined by a single-head attention mechanism (Vaswani et al., 2017) in which the current subgoal attends over future ones, with a linear ALiBi position bias (Press et al., 2021) whose slope controls how strongly attention is biased towards nearby subgoals. As in DeepLTL, training requires no LTL formulae: the policy learns on randomly sampled sequences of Boolean reach–avoid pairs under a curriculum, including ε -prefixed stability sequences, and ε -transitions are exposed as an additional binary action. At evaluation time, a specification is converted into an LDBA and a depth-first search extracts accepting runs from every automaton state; the assignment sets labelling each transition are then synthesised into minimal Boolean formulae, with disjunctive reach formulae split into one candidate sequence per disjunct. Whenever the automaton state changes, the agent re-selects among the candidate sequences of the new state using its learned value function. Having been trained on arbitrary formula sequences, the policy generalises across automata and therefore across LTL specifications. Appendix F Training Details F.1 Model Architectures All methods in Jaxolotl instantiate the same modular policy architecture, assembled from interchangeable components configured per environment. An observation encoder (“Env Net” in the tables of Section F.3) maps the environment observation to a feature vector: in LetterWorld, a convolutional network processes the egocentric grid channels, whereas in every other environment the observation is flattened and passed through a multi-layer perceptron (MLP; Rumelhart et al., 1986). In parallel, the method-specific task encoder of Appendix E (“LTL Encoder”) produces an embedding of the current task representation. The observation features and task embedding are concatenated into a joint representation on which both the actor and the critic operate; the two encoders are thus shared, while the actor and critic themselves have no common parameters. The critic is an MLP mapping the joint representation to a scalar value estimate. The actor is an MLP whose final hidden layer feeds one linear head per parameter group of the action distribution. GenZ-LTL deviates from this pattern only in that it has no task encoder: its observation reduction (see Appendix E) injects the subgoal into the observation itself, so the joint representation coincides with the encoded (reduced) observation; in the unreduced variant, one-hot encodings of the reach and avoid assignments are appended to the flattened observation before encoding. All linear layers are initialised with orthogonal weights and zero biases. The actor heads follow the action space of the environment. In LetterWorld and ConveyorWorld, as well as in the discretised environment variants on which GCRL-LTL operates, a single head outputs the logits of a categorical distribution over the discrete actions. In ZoneEnv, ZoneEnv-NM, and FrankaZoneEnv, two heads output the mean and the state-dependent standard deviation of a diagonal Gaussian, with a softplus transformation guaranteeing positivity of the latter. In Warehouse, whose hybrid action space pairs a continuous control input with a discrete interaction, the Gaussian heads are complemented by a categorical head, and the resulting distributions are treated as independent factors of a joint distribution. Methods that expose the ε -transitions of the LDBA to the agent extend the actor with dedicated heads. In DeepLTL and StructLTL, an additional scalar head defines a Bernoulli distribution over taking the ε -action, masked out whenever no ε -transition is available in the current automaton state; if the ε -action is taken, the sampled environment action is discarded and only the automaton advances. In SemLTL, the analogous head is instead evaluated once per ε -successor—on a joint representation formed from the observation features and the projected semantic label of that successor—and once on the current state, yielding a masked categorical distribution that selects between jumping to one of the ε -successors and acting in the environment. Two methods maintain auxiliary networks alongside the actor and critic. GenZ-LTL, trained with the Lagrangian-constrained variant of PPO, adds a cost critic with the same structure as the critic, together with a state-dependent Lagrange-multiplier network whose softplus activation keeps the multiplier non-negative; both operate on the same encoded observation as the actor. GCRL-LTL fits its goal-conditioned value function as an entirely separate model comprising its own observation encoder and goal-embedding table: the encoded observation is concatenated with the embeddings of the currently pursued and the prospective goal propositions and mapped to a scalar value by an MLP. F.2 Curricula A curriculum in Jaxolotl is a sequence of stages, each of which defines a distribution over tasks via a sampler (or a mixture of samplers with associated probabilities). Since sampled tasks are dynamic Python objects, curricula are precomputed: before training, we draw a fixed number of tasks per stage and convert them into the method-specific static array representation. At the beginning of each episode, a task is then sampled uniformly at random from the precomputed samples of the current stage. If sampling is expensive (as for SemLTL, which compiles every sampled formula into an LDBA), the precomputed curriculum is generated once and cached on disk. The agent progresses through the stages based on a stage frontier shared across all parallel environments. We track the success rate at the frontier stage over a rolling window of recently completed episodes, where an episode counts as successful if it terminates with positive reward. The frontier advances once this rate exceeds the threshold of the current stage, provided that the window has been filled and that a minimum fraction of environments has contributed episodes at the frontier (this prevents a small number of environments from dominating the estimate). Environments behind the frontier do not switch immediately: after each training rollout, a lagging environment advances one stage with a fixed adoption probability, so that the training distribution shifts gradually. The task distributions reflect the task representation of each method. DeepLTL and StructLTL are trained on reach–avoid sequences, where later stages increase the sequence depth and the number of reach and avoid propositions per step, and additionally include reach–stay tasks in environments with infinite-horizon specifications. For StructLTL, the reach and avoid components are Boolean formulae drawn from environment-specific pools rather than single assignments; the two methods share identical curricula in several environments. LTL2Action and SemLTL sample LTL formulae from templates of the corresponding families (sequenced reach and reach–avoid objectives, as well as reach–stay objectives for SemLTL), such that all curriculum-based methods are trained on comparable task distributions. In all cases, the samplers ensure that sampled tasks are feasible, e.g. by never sampling a reach objective that is already satisfied by the preceding step. As discussed in Section 4.4, GenZ-LTL and GCRL-LTL are trained on a single stage without progression, which samples uniformly random reach–avoid subgoals and goal propositions, respectively. Depending on the method and environment, curricula consist of between one and seven stages. Where the original works prescribe curricula, ours closely follow them; for the remaining environments, we design analogous curricula. The exact stage definitions for each method and environment (samplers, parameter ranges, mixture weights, and thresholds) can be found in the accompanying codebase. F.3 Hyperparameters We provide the full set of training and model hyperparameters for each method in each environment; see Table 8 for LetterWorld, Table 9 for ZoneEnv and ZoneEnv-NM, Table 10 for FrankaZoneEnv, Table 11 for Warehouse, and Table 12 for ConveyorWorld and ConveyorWorldSimple. For GenZ-LTL and GCRL-LTL, the training “curriculum” consists of a single stage (i.e. no curriculum), so hyperparameters related to curriculum progression do not apply. Hyperparameters were largely taken from the literature where applicable. We use Adam (Kingma and Ba, 2015) for all experiments. Appendix G Experimental Details G.1 Computational Efficiency All timing experiments were run on a single desktop machine with consumer hardware: an NVIDIA GeForce RTX 5070 Ti GPU (16 GiB VRAM), an Intel Core i5-13600K CPU, and 32 GiB of RAM. For the comparison in Figure 3, Jaxolotl trains multiple seeds in parallel on the GPU by vectorising the training loop over seeds with vmap. The reference implementations train a single seed per run. Running two reference instances concurrently increases their overall throughput, whereas running more reduces it due to resource contention. For each number of seeds k, we therefore report the fastest wall-clock time in which each implementation produces k trained seeds, and measure evaluation times in the same way. Timings for Jaxolotl include JIT compilation. Environment Throughput. Figure 7 compares raw environment throughput, measured in environment steps per second (SPS) over 8,192 steps of each parallel environment. Jaxolotl batches environments on the GPU with vmap, whereas the reference implementations run each environment in a separate process and step them asynchronously. We evaluate Jaxolotl with up to 2,048 parallel environments and the references with at most 128, since larger numbers caused them to crash. At its largest setting, Jaxolotl is between 35× (FrankaZoneEnv) and 5,010× (ZoneEnv) faster than the best reference measurement. On FrankaZoneEnv, which simulates a 7-DoF arm with MJX, Jaxolotl only overtakes the reference from 32 parallel environments onwards. Part of the ZoneEnv speedup comes from replacing the MuJoCo-based point robot of the original environment with point-mass dynamics (Section D.1). Figure 7: Environment throughput of Jaxolotl and the reference implementations against the number of parallel environments (log scales). The references run at most 128 parallel environments; the dashed line marks their best measured throughput. Annotations give the peak throughput of Jaxolotl and its speedup over this best reference measurement. G.2 Implementation Validation We validate our implementations on the finite-horizon ZoneEnv task set of Jackermeier and Abate (2025). We re-run DeepLTL, GenZ-LTL, SemLTL and StructLTL with their official codebases over 10 seeds on this task set and compare them to our implementations on the same tasks. The reference success rates in Figure 4 (left) come from these re-runs, except for LTL2Action and GCRL-LTL, for which we use the results reported by Jackermeier and Abate (2025) on the same task set. The training curves in Figure 4 (right) show the re-runs of DeepLTL and GenZ-LTL. Appendix H Additional Results H.1 Per-Specification Results Table 5, Table 6, and Table 7 present per-specification benchmark results (aggregated in Section 5.2.1) for the finite-horizon, infinite-horizon, and reach-stay LTL specifications, respectively. H.2 Non-Myopic Reasoning While many of the methods studied are capable of non-myopic reasoning in principle, reasoning over many steps becomes difficult to learn in practice once exploration and credit assignment are non-trivial. To demonstrate, we evaluate them on k-step variants of the original ConveyorWorld environment (Abate et al., 2026), of which ConveyorWorldSimple-k (Section 5.2.2) is a simplification. The task structure is the same: the agent must commit to one of two one-way conveyor belts leading to rooms A and B before satisfying (1∧(2∧⋯∧k)) F\,( p_1 F\,( p_2 … F\, p_k)) with i≠j p_i≠ p_j, where 1,…,k−1 p_1,…, p_k-1 are accessible in both rooms and k∼U(,) p_k U(\ a, b\) is accessible only in room A (for a) or B (for b). Unlike the simplified version, the agent must first explore the starting room to reach the belts, and then explore the room it arrives in to enter the grid tile associated with each proposition in order from 1 p_1 to k p_k before receiving any reward. Figure 8(a) provides a visualisation of ConveyorWorld-k. Figure 8(b) presents success rate over k in ConveyorWorld; we see severe degradation of all non-myopic methods as k increases. The performance of trained policies is trimodal across seeds for each: some seeds learn the task and achieve 100%100\% success rate, others collapse to always entering the same room as a local optimum, and the rest never learn to exploit any reward within the training budget (e.g. continually staying in the initial room). The distribution generally shifts from the first mode through the second into the last with increasing k as exploration and credit assignment become more challenging, since the agent must visit all k subgoals in order before receiving any reward. Note that using a multi-stage curriculum did not improve performance, as many seeds failed to learn even simple k F\, p_k reach tasks in the first curriculum stage. (a) (b) Figure 8: (a) A visualisation of ConveyorWorld-k; the green circle marks the agent start position, and the upper and lower one-way conveyor belts lead to rooms A and B respectively. (b) Non-myopic reasoning results on different step variants of ConveyorWorld-k. Table 2: Finite-horizon LTL specifications used for evaluation. ID LTL Formula LetterWorld φ1 _1 (∧(¬))∧ F\,( a ( b\; U\; c)) F\, d φ2 _2 ()∧(¬(∧))( F\, d) ( f\; U\;( d F\, b)) φ3 _3 (((∨)∧))∧((∧))∧( F\,(( a c j) F\, b)) ( F\,( c F\, d)) F\, k φ4 _4 ¬(∧(¬(∧(¬)))) a\; U\;( b ( c\; U\;( d ( e\; U\; f)))) φ5 _5 ¬(∨)∧(∧(∧(∧))) G\, ( k l) F\,( a F\,( e F\,( i F\, d))) φ6 _6 ¬(∨)∧(→¬)∧∧(∧) G\, ( a b c d) G\,( h→ f\; U\; g) F\, g F\,( h F\, i) φ7 _7 ((∨)∧((→(¬(∧)))∧(→))) F\,(( a l) (( a→( b\; U\;( c F\, d))) ( l→ F\, g))) φ8 _8 (∧(∧(∧(∧(∧(∧(∧))))))) F\,( a F\,( b F\,( c F\,( d F\,( e F\,( f F\,( g F\, h))))))) φ9 _9 ¬∧(∧(∧(∧(∧(∧))))) G\, l F\,( i F\,( e F\,( a F\,( k F\,( g F\, c))))) φ10 _10 ¬(∨)(∧((∨)∧((→)))) ( b d f h j)\; U\;( l F\,(( a k) (( a→ F\, c)))) ZoneEnv φ11 _11 (∧(¬))∧ F\,( green ( red\; U\; yellow)) F\, purple φ12 _12 ()∧(¬(∧))( F\, red) ( red\; U\;( green F\, yellow)) φ13 _13 (∨)∧∧ F\,( red green) F\, yellow F\, purple φ14 _14 ¬(∨)(∧) ( purple yellow)\; U\;( red F\, green) φ15 _15 ¬((∨)∧(¬)) green\; U\;(( red purple) ( green\; U\; yellow)) φ16 _16 ((∨)→(¬))(( green red)→( yellow\; U\; purple))\; U\; yellow φ17 _17 ¬∧(∧(∧)) G\, purple F\,( red F\,( green F\, yellow)) φ18 _18 ¬(∨)(∧(∧(¬))) ( green purple yellow)\; U\;( red F\,( yellow ( red\; U\; green))) φ19 _19 ¬∧(∧(∧(∧))) G\, yellow F\,( red F\,( purple F\,( green F\, red))) φ20 _20 ((∨)∧((→(¬(∧)))∧(→(¬(∧))))) F\,(( red green) (( red→( yellow\; U\;( purple F\, green))) ( green→( purple\; U\;( yellow F\, red))))) FrankaZoneEnv φ21 _21 ¬(∨)∧((∧(∧))∨(∧(∧))) G\, ( cyan pink) ( F\,( red F\,( yellow F\, purple)) F\,( blue F\,( green F\, orange))) φ22 _22 (∧(∧))∧(∧(∧)) F\,( red F\,( green F\, blue)) F\,( orange F\,( pink F\, cyan)) φ23 _23 ∧∧∧∧(¬)∧(¬) F\, yellow F\, purple F\, cyan F\, blue ( cyan\; U\; yellow) ( blue\; U\; purple) φ24 _24 (¬)∧(∧)( pink\; U\; cyan) F\,( pink F\, red) φ25 _25 ¬(∨)((∨)∧(¬(∨)(∨))) ( green yellow)\; U\;(( red purple) ( ( blue pink)\; U\;( cyan orange))) φ26 _26 (¬(∨))∧(((→(¬))∧(→(¬)))(∧))( red\; U\;( green pink)) ((( green→( red\; U\; cyan)) ( pink→( red\; U\; orange)))\; U\;( red F\, yellow)) φ27 _27 ¬(∨)∧((∨)∧(∧(∧))) G\, ( red pink) F\,(( green blue) F\,( yellow F\,( cyan F\, orange))) φ28 _28 (∧∧¬(∨))∨(∧∧¬(∨))( F\, red F\, green G\, ( blue yellow)) ( F\, blue F\, yellow G\, ( red green)) φ29 _29 (∧(∧(∧(∧(∧(∧(∧))))))) F\,( red F\,( green F\,( purple F\,( yellow F\,( blue F\,( orange F\,( cyan F\, pink))))))) φ30 _30 ¬(∧(¬(∧(¬(∧(¬(∧(¬(∧(¬(∧(¬(∧(¬)))))))))))))) green\; U\;( red ( purple\; U\;( green ( yellow\; U\;( purple ( blue\; U\;( yellow ( orange\; U\;( blue ( cyan\; U\;( orange ( pink\; U\;( cyan ( red\; U\; pink)))))))))))))) Warehouse φ31 _31 (_∧(∧_)) F\,( region\_a F\,( crate F\, region\_b)) φ32 _32 ¬(_∨)(∧_) ( region\_a door)\; U\;( vase region\_b) φ33 _33 ¬(_∧(¬_)) door\; U\;( region\_a ( vase\; U\; region\_b)) φ34 _34 ¬(∨)(_∧(∧_)) ( vase crate)\; U\;( region\_a F\,( door F\, region\_b)) φ35 _35 (∧_∧(_(¬∧_))) F\,( vase region\_a ( region\_a\; U\;( vase region\_a))) φ36 _36 (∧_∧(_(¬∧¬∧_))) F\,( vase crate region\_b ( region\_b\; U\;( vase crate region\_b))) φ37 _37 (→(_))(∧_∧(_(¬∧_)))( crate→( crate\; U\; region\_b))\; U\;( crate region\_b ( region\_b\; U\;( crate region\_b))) φ38 _38 (→())((∧_∧(_(¬∧_)))∧(∧((¬∧))))( vase→( vase\; U\; door))\; U\;( F\,( crate region\_b ( region\_b\; U\;( crate region\_b))) F\,( vase door ( door\; U\;( vase door)))) φ39 _39 (→(¬(_∨_)))(∧((¬∧)))( crate→( ( region\_a region\_b))\; U\; door)\; U\;( vase door ( door\; U\;( vase door))) φ40 _40 (∧_∧(_(¬∧_)))∧(∧((¬∧))) F\,( crate region\_a ( region\_a\; U\;( crate region\_a))) F\,( vase door ( door\; U\;( vase door))) ZoneEnv-NM φ41 _41 ()∧(¬(∧))( F\, red) ( red\; U\;( green F\, yellow)) φ42 _42 (∨)∧∧ F\,( red green) F\, yellow F\, purple φ43 _43 ¬(∨)(∧) ( purple yellow)\; U\;( red F\, green) φ44 _44 ¬((∨)∧(¬)) green\; U\;(( red purple) ( green\; U\; yellow)) φ45 _45 ((∨)→(¬))(( green red)→( yellow\; U\; purple))\; U\; yellow φ46 _46 (∧(¬))∧ F\,( green ( red\; U\; yellow)) F\, purple φ47 _47 (∨)∧(¬) F\,( yellow purple red) ( yellow\; U\; green) φ48 _48 ∧∧∧ F\, purple F\, green F\, yellow F\, red φ49 _49 ((∨)∧((∨)∧)) F\,(( purple yellow) F\,(( purple red) F\, green)) φ50 _50 (¬)∧(∧(∧))( yellow\; U\; purple) F\,( green F\,( red F\, green)) Table 3: Infinite-horizon LTL specifications used for evaluation. ID LTL Formula LetterWorld ψ1 _1 ∧∧ G\, F\, a G\, F\, b G\, F\, c ψ2 _2 (∧)∧(∧) G\, F\,( a F\, d) G\, F\,( b F\, e) ψ3 _3 ¬∧∧∧ G\, l G\, F\, c G\, F\, g G\, F\, j ψ4 _4 (¬)∧∧∧∧( a\; U\; b) G\, F\, a G\, F\, f G\, F\, g G\, F\, h ψ5 _5 (→)∧∧ G\,( a→ F\, d) G\, F\, a G\, F\, h ψ6 _6 (∧(¬))∧ G\, F\,( c ( d\; U\; e)) G\, F\, b ψ7 _7 (∧(∧))∧∧∧∧ F\,( a F\,( b F\, c)) G\, F\, d G\, F\, e G\, F\, f G\, F\, g ψ8 _8 (→(¬))∧∧ G\,( b→( c\; U\; d)) G\, F\, b G\, F\, c ψ9 _9 (∧)∧ G\, F\,( e F\, h) G\, F\, k ψ10 _10 ∧∧∧∧¬ G\, F\, a G\, F\, b G\, F\, c G\, F\, d G\, l ZoneEnv ψ11 _11 ∧∧ G\, F\, yellow G\, F\, green G\, F\, red ψ12 _12 ∧∧∧¬ G\, F\, red G\, F\, green G\, F\, yellow G\, purple ψ13 _13 ∧∧ G\, F\, red G\, F\, yellow G\, F\, purple ψ14 _14 (∧)∧ G\, F\,( red F\, green) G\, F\, purple ψ15 _15 ¬∧(∧)∧ G\, purple G\, F\,( red F\, green) G\, F\, yellow ψ16 _16 (→)∧∧ G\,( red→ F\, yellow) G\, F\, red G\, F\, green ψ17 _17 (∧(¬))∧ G\, F\,( green ( yellow\; U\; purple)) G\, F\, red ψ18 _18 (¬)∧∧∧( red\; U\; purple) G\, F\, red G\, F\, yellow G\, F\, green ψ19 _19 (→(¬))∧∧ G\,( purple→( green\; U\; yellow)) G\, F\, purple G\, F\, green ψ20 _20 (∧)∧∧∧ F\,( red F\, green) G\, F\, yellow G\, F\, purple G\, F\, red FrankaZoneEnv ψ21 _21 ∧∧∧ G\, F\, red G\, F\, green G\, F\, blue G\, F\, yellow ψ22 _22 (∧)∧(∧) G\, F\,( orange F\, pink) G\, F\,( cyan F\, purple) ψ23 _23 ¬(∨)∧∧∧ G\, ( red pink) G\, F\, green G\, F\, orange G\, F\, cyan ψ24 _24 (∧(¬(∨)))∧ G\, F\,( yellow ( ( blue red)\; U\; purple)) G\, F\, orange ψ25 _25 (¬)∧∧( blue\; U\; cyan) G\, F\, blue G\, F\, pink ψ26 _26 (→)∧(→)∧∧ G\,( blue→ F\, yellow) G\,( green→ F\, purple) G\, F\, blue G\, F\, green ψ27 _27 ∧∧(→(¬)) G\, F\, cyan G\, F\, purple G\,( cyan→( purple\; U\; orange)) ψ28 _28 (∧(∧))∧∧ F\,( yellow F\,( orange F\, pink)) G\, F\, red G\, F\, green ψ29 _29 (→(¬))∧(→(¬))∧∧ G\,( red→( blue\; U\; green)) G\,( blue→( red\; U\; green)) G\, F\, red G\, F\, blue ψ30 _30 (∧(¬))∧(∧(¬)) G\, F\,( cyan ( pink\; U\; purple)) G\, F\,( pink ( cyan\; U\; yellow)) Warehouse ψ31 _31 _∧_∧ G\, F\, region\_a G\, F\, region\_b G\, F\, door ψ32 _32 (∧¬)∧(∧¬)∧∧¬_ G\, F\,( vase F\, vase) G\, F\,( crate F\, crate) G\, F\, door G\, region\_a ψ33 _33 (∧_∧(_(¬∧_)))∧∧_ F\,( vase region\_a ( region\_a\; U\;( vase region\_a))) G\, F\, door G\, F\, region\_b ψ34 _34 (∧_∧(_(¬∧_)))∧(∧_∧(_(¬∧_))) G\, F\,( vase region\_a ( region\_a\; U\;( vase region\_a))) G\, F\,( crate region\_b ( region\_b\; U\;( crate region\_b))) ψ35 _35 _∧_∧∧(→_) G\, F\, region\_a G\, F\, region\_b G\, F\, door G\,( door→ F\, region\_a) ψ36 _36 (∧(¬∧_))∧_ G\, F\,( vase F\,( vase region\_a)) G\, F\, region\_b ψ37 _37 (∧(¬∧_))∧ G\, F\,( crate F\,( crate region\_b)) G\, F\, door ψ38 _38 ¬_∧_∧∧(∧¬) G\, region\_b G\, F\, region\_a G\, F\, door G\, F\,( vase F\, vase) ψ39 _39 (_∧_)∧ G\, F\,( region\_a F\, region\_b) G\, F\, door ψ40 _40 (→(¬∧_))∧∧ G\,( vase→ F\,( vase region\_a)) G\, F\, vase G\, F\, door Table 4: Reach-stay LTL specifications used for evaluation. ID LTL Formula ZoneEnv χ1 _1 F\, G\, red χ2 _2 ∧(∧) F\, G\, red F\,( yellow F\, green) χ3 _3 ∧¬ F\, G\, purple G\, yellow χ4 _4 ((∨)→)∧(∨) G\,(( green yellow)→ F\, red) F\, G\,( green purple) χ5 _5 F\, G\, green χ6 _6 F\, G\, yellow χ7 _7 ∧¬ F\, G\, green G\, red χ8 _8 ∧(∧) F\, G\, purple F\,( green F\, red) χ9 _9 ∧¬ F\, G\, purple G\, green χ10 _10 (→)∧ G\,( yellow→ F\, red) F\, G\, purple Warehouse χ11 _11 _ F\, G\, region\_a χ12 _12 (∧_∧(_(¬∧_)))∧_ F\,( vase region\_b ( region\_b\; U\;( vase region\_b))) F\, G\, region\_b χ13 _13 _ F\, G\, region\_b χ14 _14 ∧¬_ F\, G\, vase G\, region\_a χ15 _15 ∧_ F\, vase F\, G\, region\_a χ16 _16 ∧_ F\, crate F\, G\, region\_b χ17 _17 _∧¬ F\, G\, region\_a G\, crate χ18 _18 ∧_ F\, vase F\, G\, region\_b χ19 _19 (∧_∧(_(¬∧_)))∧_ F\,( crate region\_a ( region\_a\; U\;( crate region\_a))) F\, G\, region\_a χ20 _20 _∧(∧¬) F\, G\, region\_b F\,( crate F\, crate) Table 5: Per-specification finite-horizon benchmark results (success rate), averaged over 512 evaluation episodes, with 95%95\% Student-t CIs over training seeds. Best results are bold, second best underlined, — denotes unsupported configurations. φ LTL2Action GCRL-LTL DeepLTL GenZ-LTL† GenZ-LTL (unreduced obs.) SemLTL StructLTL LetterWorld φ1 _1 0.62±0.14 0.99±0.00 1.00±0.00 0.99±0.00 1.00±0.00 1.00±0.00 1.00±0.00 φ2 _2 0.74±0.15 0.99±0.00 0.96±0.01 1.00±0.00 0.98±0.00 0.95±0.01 0.97±0.01 φ3 _3 0.45±0.13 1.00±0.00 1.00±0.00 1.00±0.00 1.00±0.00 1.00±0.00 1.00±0.00 φ4 _4 0.52±0.20 0.98±0.01 0.95±0.01 0.99±0.00 0.97±0.01 0.94±0.01 0.95±0.01 φ5 _5 0.02±0.01 0.92±0.01 0.73±0.03 1.00±0.00 0.85±0.02 0.57±0.07 0.79±0.04 φ6 _6 0.00±0.00 0.72±0.01 0.53±0.07 0.97±0.01 0.77±0.02 0.32±0.04 0.62±0.03 φ7 _7 0.63±0.15 1.00±0.00 1.00±0.00 0.99±0.00 1.00±0.00 1.00±0.00 1.00±0.00 φ8 _8 0.90±0.03 1.00±0.00 1.00±0.00 1.00±0.00 0.99±0.00 0.81±0.06 1.00±0.00 φ9 _9 0.01±0.01 0.97±0.01 0.79±0.02 1.00±0.00 0.89±0.01 0.62±0.07 0.83±0.03 φ10 _10 0.27±0.10 0.85±0.02 0.78±0.02 1.00±0.00 0.89±0.02 0.70±0.02 0.81±0.02 ZoneEnv φ11 _11 0.33±0.11 0.99±0.00 0.96±0.02 1.00±0.00 1.00±0.00 0.97±0.02 0.98±0.02 φ12 _12 0.24±0.21 0.95±0.01 0.94±0.01 1.00±0.00 0.97±0.01 0.92±0.01 0.97±0.01 φ13 _13 0.68±0.13 1.00±0.00 0.98±0.01 1.00±0.00 1.00±0.00 0.98±0.01 0.99±0.00 φ14 _14 0.68±0.15 0.92±0.01 0.91±0.02 0.99±0.00 0.93±0.01 0.91±0.02 0.94±0.01 φ15 _15 0.79±0.16 0.93±0.01 0.94±0.01 1.00±0.00 0.95±0.01 0.90±0.05 0.97±0.00 φ16 _16 0.90±0.04 0.99±0.00 0.96±0.01 1.00±0.00 0.99±0.01 0.98±0.01 0.99±0.01 φ17 _17 0.06±0.06 0.88±0.02 0.83±0.07 0.99±0.00 0.93±0.02 0.83±0.05 0.94±0.02 φ18 _18 0.47±0.19 0.85±0.01 0.81±0.03 0.98±0.00 0.88±0.02 0.83±0.01 0.88±0.01 φ19 _19 0.03±0.06 0.83±0.02 0.84±0.07 0.99±0.00 0.92±0.02 0.71±0.09 0.88±0.08 φ20 _20 0.17±0.07 1.00±0.00 0.98±0.01 1.00±0.00 1.00±0.00 0.32±0.07 0.98±0.02 FrankaZoneEnv φ21 _21 0.02±0.01 0.50±0.26 0.39±0.18 1.00±0.00 0.45±0.21 0.50±0.13 0.88±0.01 φ22 _22 0.00±0.00 0.56±0.31 0.76±0.14 1.00±0.00 0.38±0.26 0.48±0.08 0.99±0.00 φ23 _23 0.02±0.01 0.54±0.28 0.54±0.18 1.00±0.00 0.44±0.23 0.62±0.10 0.94±0.01 φ24 _24 0.07±0.03 0.66±0.29 0.62±0.20 1.00±0.00 0.55±0.27 0.89±0.04 0.97±0.01 φ25 _25 0.14±0.05 0.72±0.19 0.50±0.10 1.00±0.00 0.71±0.20 0.83±0.02 0.97±0.01 φ26 _26 0.01±0.01 0.53±0.30 0.50±0.21 1.00±0.00 0.45±0.26 0.28±0.05 0.95±0.01 φ27 _27 0.00±0.00 0.43±0.27 0.25±0.16 1.00±0.00 0.32±0.18 0.44±0.15 0.81±0.01 φ28 _28 0.13±0.03 0.70±0.20 0.63±0.14 1.00±0.00 0.60±0.19 0.52±0.19 0.95±0.01 φ29 _29 0.00±0.00 0.47±0.33 0.58±0.21 1.00±0.00 0.31±0.25 0.34±0.11 0.99±0.00 φ30 _30 0.00±0.00 0.39±0.28 0.35±0.26 1.00±0.00 0.27±0.23 0.23±0.08 0.95±0.01 Warehouse φ31 _31 0.97±0.02 — 0.98±0.01 — 0.96±0.03 0.95±0.10 0.99±0.01 φ32 _32 0.41±0.26 — 0.94±0.02 — 0.91±0.03 0.92±0.03 0.95±0.01 φ33 _33 0.19±0.22 — 0.97±0.03 — 0.95±0.04 0.99±0.01 0.94±0.08 φ34 _34 0.21±0.10 — 0.93±0.02 — 0.74±0.27 0.78±0.08 0.79±0.14 φ35 _35 0.62±0.33 — 0.76±0.22 — 0.99±0.01 0.98±0.02 0.99±0.00 φ36 _36 0.52±0.31 — 0.72±0.20 — 0.96±0.01 0.83±0.16 0.99±0.01 φ37 _37 0.12±0.10 — 0.85±0.11 — 0.97±0.02 0.75±0.11 0.98±0.01 φ38 _38 0.11±0.19 — 0.60±0.24 — 0.63±0.31 0.41±0.14 0.88±0.22 φ39 _39 0.11±0.14 — 0.77±0.20 — 0.66±0.33 0.80±0.12 0.95±0.03 φ40 _40 0.11±0.20 — 0.51±0.27 — 0.64±0.31 0.94±0.04 0.88±0.22 Table 6: Per-specification infinite-horizon benchmark results (completed accepting cycles), averaged over 512 evaluation episodes, with 95%95\% Student-t CIs over training seeds. Best results are bold, second best underlined, — denotes unsupported configurations. ψ GCRL-LTL DeepLTL GenZ-LTL† GenZ-LTL (unreduced obs.) SemLTL StructLTL LetterWorld ψ1 _1 9.4±0.1 6.8±0.3 9.8±0.1 6.9±0.1 6.0±0.2 6.7±0.4 ψ2 _2 6.4±0.0 4.3±0.2 6.7±0.1 4.5±0.0 4.1±0.1 4.3±0.2 ψ3 _3 8.8±0.5 5.3±0.4 9.8±0.1 6.2±0.1 4.5±0.3 5.7±0.3 ψ4 _4 6.3±0.0 4.0±0.3 6.7±0.1 4.5±0.0 3.3±0.2 4.1±0.2 ψ5 _5 9.4±0.3 6.3±0.9 6.4±0.3 5.2±0.3 6.0±0.3 7.1±0.8 ψ6 _6 9.3±0.1 6.4±0.5 9.9±0.1 6.8±0.2 4.2±0.6 6.8±0.4 ψ7 _7 5.6±0.1 3.6±0.2 5.9±0.0 3.8±0.1 2.7±0.2 3.5±0.2 ψ8 _8 9.7±0.1 6.2±0.4 10.5±0.1 7.0±0.1 2.1±0.3 6.8±0.2 ψ9 _9 9.4±0.1 6.6±0.4 9.9±0.1 7.0±0.2 6.2±0.4 6.8±0.3 ψ10 _10 6.0±0.1 3.4±0.2 6.7±0.1 3.9±0.1 2.7±0.2 3.5±0.2 ZoneEnv ψ11 _11 6.0±0.1 3.3±0.4 6.7±0.3 5.1±0.2 3.3±0.2 3.9±0.4 ψ12 _12 4.5±0.2 2.3±0.4 6.6±0.3 4.7±0.1 2.8±0.1 3.0±0.3 ψ13 _13 6.0±0.1 3.2±0.3 6.7±0.3 5.1±0.2 3.2±0.1 3.9±0.5 ψ14 _14 5.9±0.1 3.3±0.5 6.6±0.2 5.1±0.2 3.1±0.1 3.6±0.6 ψ15 _15 4.4±0.2 2.2±0.4 6.6±0.3 4.6±0.2 2.8±0.2 2.9±0.3 ψ16 _16 6.9±0.1 3.5±0.6 5.1±0.9 4.7±0.7 3.2±0.2 4.2±0.5 ψ17 _17 5.7±0.1 3.1±0.5 6.6±0.3 5.0±0.2 2.3±0.3 3.7±0.5 ψ18 _18 5.6±0.1 3.0±0.3 6.7±0.3 5.0±0.1 2.5±0.2 3.7±0.4 ψ19 _19 6.3±0.1 3.3±0.4 7.3±0.2 5.5±0.2 1.2±0.4 4.3±0.2 ψ20 _20 5.7±0.1 2.9±0.3 6.4±0.3 4.8±0.1 2.1±0.2 3.5±0.4 FrankaZoneEnv ψ21 _21 5.3±4.0 4.0±2.7 24.6±0.3 3.4±2.9 15.1±1.7 11.9±0.3 ψ22 _22 5.4±4.0 3.9±2.6 23.9±0.3 3.6±3.0 14.3±1.2 11.5±0.4 ψ23 _23 5.7±4.6 2.2±2.5 32.1±0.6 3.3±3.0 12.7±3.5 10.7±0.9 ψ24 _24 7.3±5.5 5.0±3.6 33.9±0.5 4.4±3.3 8.2±2.0 15.3±0.4 ψ25 _25 17.1±12.7 8.6±5.8 67.7±2.3 9.9±7.9 35.7±2.9 27.8±1.1 ψ26 _26 5.6±3.4 4.1±1.7 13.5±2.1 3.0±1.4 15.8±1.4 11.1±0.5 ψ27 _27 7.7±5.1 5.1±3.3 33.7±0.8 5.2±3.5 2.8±1.6 14.0±0.8 ψ28 _28 16.3±12.4 8.2±6.3 68.1±1.9 9.5±7.6 28.9±4.7 28.0±1.2 ψ29 _29 6.2±4.0 3.7±2.5 28.4±0.7 4.2±3.0 1.1±1.1 11.2±0.5 ψ30 _30 4.8±3.5 3.5±2.6 23.6±0.3 4.9±3.4 1.3±0.4 11.3±0.2 Warehouse ψ31 _31 — 2.3±0.4 — 1.6±0.6 0.2±0.2 2.5±0.2 ψ32 _32 — 4.0±3.3 — 2.6±1.5 0.3±0.4 2.1±1.2 ψ33 _33 — 1.9±0.7 — 1.9±0.9 0.3±0.2 3.0±0.1 ψ34 _34 — 1.7±0.9 — 3.0±0.3 0.1±0.1 3.8±0.2 ψ35 _35 — 2.3±0.3 — 1.5±0.7 0.2±0.2 2.8±0.1 ψ36 _36 — 3.7±0.5 — 3.2±0.9 0.2±0.2 4.4±0.3 ψ37 _37 — 2.5±0.5 — 1.9±0.8 0.0±0.0 2.9±0.1 ψ38 _38 — 1.9±0.6 — 1.8±0.7 0.3±0.2 2.6±0.5 ψ39 _39 — 2.2±0.4 — 1.6±0.6 0.2±0.2 2.4±0.3 ψ40 _40 — 3.7±0.6 — 3.0±0.9 0.1±0.1 4.2±0.2 Table 7: Per-specification reach-stay benchmark results (completed accepting cycles), averaged over 512 evaluation episodes, with 95%95\% Student-t CIs over training seeds. Best results are bold, second best underlined, — denotes unsupported configurations. χ GCRL-LTL DeepLTL GenZ-LTL† GenZ-LTL (unreduced obs.) SemLTL StructLTL ZoneEnv χ1 _1 24.2±5.0 645.1±85.6 548.0±57.2 340.6±119.3 615.7±38.5 608.4±61.8 χ2 _2 51.2±16.2 497.2±61.5 471.7±61.7 307.4±99.8 445.5±22.1 501.2±56.8 χ3 _3 21.6±3.3 512.8±79.5 533.1±51.9 317.6±103.0 591.4±67.9 575.4±63.8 χ4 _4 28.4±6.7 520.9±85.7 495.6±37.5 303.1±104.9 285.3±101.4 571.0±64.9 χ5 _5 25.9±4.3 635.4±51.3 541.4±51.2 333.8±129.0 679.1±64.9 593.8±100.8 χ6 _6 18.9±2.6 513.4±113.3 299.4±94.5 341.8±104.1 639.0±66.7 626.8±97.9 χ7 _7 22.8±4.3 603.1±44.7 511.4±52.9 321.6±127.6 631.5±71.5 573.9±106.0 χ8 _8 60.3±12.9 438.9±71.3 477.3±60.3 306.9±93.7 495.3±53.7 511.6±61.2 χ9 _9 22.1±4.1 513.6±88.2 511.2±54.7 318.4±104.1 605.0±61.7 577.8±76.8 χ10 _10 26.1±3.6 521.1±81.9 530.7±53.6 325.0±103.9 341.4±90.3 586.7±59.3 Warehouse χ11 _11 — 860.6±63.4 — 128.6±48.6 823.1±24.9 872.2±35.1 χ12 _12 — 337.4±216.5 — 66.4±27.7 538.6±86.2 800.2±64.3 χ13 _13 — 600.5±224.8 — 70.9±32.3 759.4±78.6 867.8±48.0 χ14 _14 — 656.5±175.3 — 193.9±79.6 622.1±157.2 712.9±86.0 χ15 _15 — 791.5±65.1 — 117.9±45.3 745.9±45.2 815.9±36.6 χ16 _16 — 563.4±197.4 — 75.6±30.2 712.9±40.1 808.9±41.8 χ17 _17 — 819.9±83.0 — 115.1±34.7 613.4±120.6 788.7±142.4 χ18 _18 — 568.4±210.6 — 69.1±26.2 671.6±76.1 797.3±65.4 χ19 _19 — 414.2±222.1 — 121.2±58.1 592.0±85.8 821.8±30.0 χ20 _20 — 568.4±202.8 — 67.2±23.8 655.7±61.6 813.0±42.8 Table 8: Training and model hyperparameters for LetterWorld. Values spanning multiple columns are shared by those methods; N/A marks settings that do not apply to a method. Category Hyperparameter LTL2Action SemLTL DeepLTL StructLTL GCRL-LTL GenZ-LTL PPO Total environment steps 2×1072× 10^7 Environments 16 Steps/update 128 Minibatches 8 Update epochs 8 Discount (γ) 0.94 GAE lambda (λ) 0.95 Clip epsilon 0.2 Entropy coef. 0.01 0.05 Value func. coef. 0.5 Learning rate 3×10−43× 10^-4 Max grad norm 0.5 Adam epsilon 10−810^-8 Safe PPO Cost discount (γc _c) N/A 0.94 Cost value func. coef. N/A 1.0 Lagrangian coef. N/A 1.0 Target cost N/A −0.1-0.1 Min Lagrangian N/A 10−310^-3 Max Lagrangian N/A 3.0 Target KL N/A 0.015 Curriculum Samples per stage 10410^4 10510^5 Episode window N/A 256 N/A Adoption prob. N/A 0.1 N/A Min coverage N/A 0.9 N/A Env Net Channels [16, 32, 64] Kernel size [2, 2] Activation ReLU Actor Hidden sizes [64, 64, 64] Activation ReLU Critic Hidden sizes [64, 64] Activation Tanh Cost Critic Hidden sizes N/A [64, 64] Activation N/A Tanh Lagrangian Net Hidden sizes N/A [64, 64] Activation N/A Softplus LTL Encoder Embedding dim. 32 64 32 N/A RGCN layers 8 N/A RGCN activation Tanh N/A Semantic input size N/A 762 N/A Sequence model N/A GRU ALiBi attention N/A Deep sets hidden sizes N/A [32, 32] N/A Deep sets output size N/A 32 N/A Deep sets activation N/A ReLU N/A Clause net output size N/A 32 N/A Disjunct net output size N/A 32 N/A Attention hidden dim. N/A 32 N/A ALiBi slope N/A 0.5 N/A GCVF Samples N/A 2×1052× 10^5 N/A Batch size N/A 512 N/A Learning rate N/A 4×10−44× 10^-4 N/A Epochs N/A 100 N/A Environments N/A 16 N/A Steps/env N/A 2,048 N/A Environment Precomputed resets 10,240 Max episode length 75 Table 9: Training and model hyperparameters for ZoneEnv and ZoneEnv-NM. Values spanning multiple columns are shared by those methods; N/A marks settings that do not apply to a method. Category Hyperparameter LTL2Action SemLTL DeepLTL StructLTL GCRL-LTL GenZ-LTL PPO Total environment steps 2×1072× 10^7 Environments 16 Steps/update 4,096 Minibatches 32 Update epochs 10 Discount (γ) 0.998 GAE lambda (λ) 0.95 Clip epsilon 0.2 Entropy coef. 0.003 Value func. coef. 0.5 1.0 Learning rate 3×10−43× 10^-4 Max grad norm 0.5 Adam epsilon 10−810^-8 Safe PPO Cost discount (γc _c) N/A 0.998 Cost value func. coef. N/A 1.0 Lagrangian coef. N/A 1.0 Target cost N/A −0.05-0.05 Min Lagrangian N/A 0.01 Max Lagrangian N/A 5.0 Target KL N/A 0.015 Curriculum Samples per stage 10410^4 10510^5 Episode window 256 N/A Adoption prob. 0.1 N/A Min coverage 0.9 N/A Env Net Hidden sizes [128] Output size 64 Activation Tanh Actor Hidden sizes [64, 64, 64] Activation ReLU Output activation Tanh N/A Tanh Critic Hidden sizes [64, 64] Activation Tanh Softplus Cost Critic Hidden sizes N/A [64, 64] Activation N/A Tanh Lagrangian Net Hidden sizes N/A [64, 64] Activation N/A Softplus LTL Encoder Embedding dim. 32 16 N/A RGCN layers 8 N/A RGCN activation Tanh N/A Semantic input size N/A 138 N/A Sequence model N/A GRU ALiBi attention N/A Deep sets hidden sizes N/A [32] N/A Deep sets output size N/A 16 N/A Deep sets activation N/A ReLU N/A Clause net output size N/A 16 N/A Disjunct net output size N/A 16 N/A Attention hidden dim. N/A 32 N/A ALiBi slope N/A 0.5 N/A GCVF Samples N/A 2×1052× 10^5 N/A Batch size N/A 512 N/A Learning rate N/A 4×10−44× 10^-4 N/A Epochs N/A 100 N/A Environments N/A 16 N/A Steps/env N/A 2,048 N/A Environment Precomputed resets 10,240 Max episode length 1,000 Table 10: Training and model hyperparameters for FrankaZoneEnv. Values spanning multiple columns are shared by those methods; N/A marks settings that do not apply to a method. The table covers FrankaZoneEnv-k for k∈8,9,10,11,12k∈\8,9,10,11,12\. Hyperparameters that vary with k are given as functions of k. Category Hyperparameter LTL2Action SemLTL DeepLTL StructLTL GCRL-LTL GenZ-LTL PPO Total environment steps 2×1082× 10^8 Environments 2,048 Steps/update 64 Minibatches 4 Update epochs 5 Discount (γ) 0.995 GAE lambda (λ) 0.95 Clip epsilon 0.2 Entropy coef. 0.003 Value func. coef. 0.5 1.0 Learning rate 5×10−45× 10^-4 Max grad norm 1.0 Adam epsilon 10−810^-8 Safe PPO Cost discount (γc _c) N/A 0.995 Cost value func. coef. N/A 1.0 Lagrangian coef. N/A 1.0 Target cost N/A −0.05-0.05 Min Lagrangian N/A 0.01 Max Lagrangian N/A 5.0 Target KL N/A 0.015 Curriculum Samples per stage 10410^4 Episode window 512 N/A Adoption prob. 0.1 N/A Min coverage 0.9 N/A Env Net Hidden sizes [128] Output size 64 Activation Tanh Actor Hidden sizes [128, 128] Activation ReLU Output activation Tanh N/A Tanh Critic Hidden sizes [128, 128] Activation Tanh Softplus Cost Critic Hidden sizes N/A [128, 128] Activation N/A Tanh Lagrangian Net Hidden sizes N/A [128, 128] Activation N/A Softplus LTL Encoder Embedding dim. 32 16 N/A RGCN layers 8 N/A RGCN activation Tanh N/A Semantic input size N/A 4k2+14k+184k^2+14k+18 N/A Sequence model N/A GRU ALiBi attention N/A Deep sets hidden sizes N/A [32] N/A Deep sets output size N/A 16 N/A Deep sets activation N/A ReLU N/A Clause net output size N/A 16 N/A Disjunct net output size N/A 16 N/A Attention hidden dim. N/A 32 N/A ALiBi slope N/A 0.5 N/A GCVF Samples N/A 2×1052× 10^5 N/A Batch size N/A 512 N/A Learning rate N/A 4×10−44× 10^-4 N/A Epochs N/A 100 N/A Environments N/A 16 N/A Steps/env N/A 2,048 N/A Environment Precomputed resets 10,240 Max episode length (train) 200 Max episode length (eval) 1,000 Table 11: Training and model hyperparameters for Warehouse. Values spanning multiple columns are shared by those methods; N/A marks settings that do not apply to a method. Category Hyperparameter LTL2Action SemLTL DeepLTL StructLTL GenZ-LTL PPO Total environment steps 2×1082× 10^8 Environments 1,024 Steps/update 128 Minibatches 4 Update epochs 5 Discount (γ) 0.998 GAE lambda (λ) 0.95 Clip epsilon 0.2 Entropy coef. 0.003 Value func. coef. 0.5 1.0 Learning rate 5×10−45× 10^-4 Max grad norm 1.0 Adam epsilon 10−810^-8 Safe PPO Cost discount (γc _c) N/A 0.998 Cost value func. coef. N/A 1.0 Lagrangian coef. N/A 1.0 Target cost N/A −0.1-0.1 Min Lagrangian N/A 10−310^-3 Max Lagrangian N/A 3.0 Target KL N/A 0.015 Curriculum Samples per stage 10410^4 10510^5 Episode window 256 N/A Adoption prob. 0.1 N/A Min coverage 0.9 N/A Env Net Hidden sizes [128] Output size 64 Activation Tanh Actor Hidden sizes [64, 64, 64] Activation ReLU Output activation Tanh Critic Hidden sizes [64, 64] Activation Tanh Softplus Cost Critic Hidden sizes N/A [64, 64] Activation N/A Tanh Lagrangian Net Hidden sizes N/A [64, 64] Activation N/A Softplus LTL Encoder Embedding dim. 16 32 16 N/A RGCN layers 8 N/A RGCN activation Tanh N/A Semantic input size N/A 488 N/A Sequence model N/A GRU ALiBi attention N/A Deep sets hidden sizes N/A [32] N/A Deep sets output size N/A 16 N/A Deep sets activation N/A ReLU N/A Clause net output size N/A 16 N/A Disjunct net output size N/A 16 N/A Attention hidden dim. N/A 32 N/A ALiBi slope N/A 5.0 N/A Environment Precomputed resets 10,240 Max episode length 1,000 Table 12: Training and model hyperparameters for ConveyorWorld and ConveyorWorldSimple. Values spanning multiple columns are shared by those methods; N/A marks settings that do not apply to a method. The table covers ConveyorWorld-k for k∈1,2,3,4,5,6,7,8,9,10k∈\1,2,3,4,5,6,7,8,9,10\ and ConveyorWorldSimple-k for k∈1,2,4,8,16,32k∈\1,2,4,8,16,32\. Hyperparameters that vary with k are given as functions of k. Note that environment resets are not precomputed for these environments (since they are trivially cheap), and the training “curriculum” only consists of a single stage (i.e. no curriculum) for all methods. Category Hyperparameter LTL2Action SemLTL DeepLTL StructLTL GCRL-LTL GenZ-LTL PPO Total environment steps 2×1062× 10^6 Environments 256 Steps/update 64 Minibatches 4 Update epochs 8 Discount (γ) 0.9 GAE lambda (λ) 0.95 Clip epsilon 0.2 Entropy coef. 0.05 Value func. coef. 0.5 Learning rate 3×10−43× 10^-4 Max grad norm 0.5 Adam epsilon 10−810^-8 Safe PPO Cost discount (γc _c) N/A 0.9 Cost value func. coef. N/A 1.0 Lagrangian coef. N/A 1.0 Target cost N/A −0.1-0.1 Min Lagrangian N/A 10−310^-3 Max Lagrangian N/A 3.0 Target KL N/A 0.015 Curriculum Samples per stage 10410^4 Env Net Hidden sizes [] [128] Output size 4 64 Activation Tanh Actor Hidden sizes [64] Activation ReLU Critic Hidden sizes [64] Activation Tanh Softplus Cost Critic Hidden sizes N/A [64] Activation N/A Tanh Lagrangian Net Hidden sizes N/A [64] Activation N/A Softplus LTL Encoder Embedding dim. 32 16 N/A RGCN layers 2k+12k+1 N/A RGCN activation Tanh N/A Semantic input size N/A 4k2+22k+364k^2+22k+36 N/A Sequence model N/A GRU ALiBi attention N/A Deep sets hidden sizes N/A [] N/A Deep sets output size N/A 32 N/A Deep sets activation N/A ReLU N/A Clause net output size N/A 16 N/A Disjunct net output size N/A 16 N/A Attention hidden dim. N/A 32 N/A ALiBi slope N/A 0.5 N/A GCVF Samples N/A 2×1052× 10^5 N/A Batch size N/A 512 N/A Learning rate N/A 4×10−44× 10^-4 N/A Epochs N/A 100 N/A Environments N/A 16 N/A Steps/env N/A 2,048 N/A Environment Max episode length 50 (ConveyorWorld), max(50,4k) (50,4k) (ConveyorWorldSimple)