Jaxolotl: A Unified High-Performance Benchmark Suite for LTL-Based Multi-Task RL

• Different environments, evaluation protocols, and implementation details make existing methods difficult to compare, while computational costs restrict experiments to few seeds.These differences leave unclear whether reported performance gaps reflect algorithm choices or experimental setup.Source: §1 · p. 1
• JAXOLOTL unifies six representative algorithms and four environments in an end-to-end JAX benchmark suite.It precompiles symbolic task structures, such as finite automata and syntax trees, into static tensor representations.Source: §1 · p. 1
• Up to 220× end-to-end speedups over reference implementations on hardware accelerators support substantially larger controlled experiments.For example, 10 independent seeds can be trained in under four minutes rather than 13.4 hours.Source: §1 · p. 2
• General methods capable of non-myopic reasoning struggle as proposition counts grow, while stronger-scaling methods rely on environment-specific observation reduction and remain myopic.The benchmark examines general task satisfaction, non-myopic reasoning, and scaling with the number of atomic propositions.Source: §1 · p. 2
• The benchmark adds curated task suites and a standardised evaluation protocol with uncertainty estimates over independently trained policies.Its design is modular, with shared abstractions for task representations, policy architectures, and common modules.Source: §1 · p. 2, Figure 1 · p. 2

• LTL multi-task methods include decomposition-based policies that tackle subgoals sequentially and holistic policies conditioned on broader task structure.Decomposition can simplify learning but limit reasoning over the whole task and lead to myopia.Source: §2 · p. 2
• Existing evaluations remain difficult to compare because methods use different environments, task distributions, and evaluation protocols.JAXOLOTL builds on existing methods by unifying them within one JAX framework.Source: §2 · p. 3
• Unlike SpecRLBench, which retains original codebase differences, JAXOLOTL unifies six algorithms, curated task suites, and evaluation protocols.JAXOLOTL also enables accelerator-based training and evaluation with orders-of-magnitude speedups over reference implementations.Source: §2 · p. 3
• Accelerated RL frameworks have not supported LTL-specified tasks because dynamic automata and syntax trees challenge JIT compilation.XLand-MiniGrid uses fixed-size arrays for symbolic rules and goals, but does not address LTL task structures.Source: §2 · p. 3

• An MDP comprises states, actions, transitions, rewards, a discount factor, and an initial-state distribution; the policy maximises expected discounted cumulative reward.Trajectories are generated by the policy through interactions with the environment.Source: §3 · p. 3
• LTL specifies temporal properties using atomic propositions, Boolean connectives, and temporal operators such as next and until.A labelling function maps states to true propositions, and a trajectory satisfies a formula when its label sequence meets the formula's semantics.Source: §3 · p. 3
• Multi-task LTL-RL optimises a policy conditioned on each task to maximise expected task satisfaction over an arbitrary task distribution.The task-conditioned policy receives the LTL formula as its conditioning input.Source: §3 · p. 3

4 JAXOLOTL

• JAXOLOTL unifies representative multi-task LTL-RL algorithms and environments in a modular, end-to-end JAX benchmark suite.The framework is designed to support controlled benchmarking at substantially greater experimental scale.Source: §4 · p. 4

4.1 DESIGN PRINCIPLES

• Task representations and policy components share modular abstractions, while symbolic task structures are precompiled into static arrays for JIT-compatible training and evaluation.The shared architecture includes task and observation encoders and an actor–critic module; the framework also supports PPO and reusable curricula.Source: §4.1 · pp. 4–5

4.2 EVALUATION INFRASTRUCTURE

• The evaluation protocol reports mean performance across fixed benchmark tasks with 95% confidence intervals over independently trained policies.It also provides per-task scores and uses policies, rather than task-policy pairs, as statistical units.Source: §4.2 · p. 5

4.3 ENVIRONMENTS AND EVALUATION TASKS

• JAXOLOTL includes four environments spanning discrete navigation, continuous control, and object interaction, with curated finite- and infinite-horizon task suites.Figure 3 reports speedups of up to 220× for training and 79× for evaluation on ZoneEnv.Source: §4.3 · p. 5, Figure 3 · p. 6

4.4 ALGORITHMS

• The benchmark provides unified implementations of six multi-task LTL-RL methods, but GenZ-LTL uses domain-specific observation reduction and LTL2Action does not support infinite-horizon tasks.Curriculum learning is not applied to the subgoal-based methods GCRL-LTL and GenZ-LTL because their representations do not naturally support gradual increases in task complexity.Source: §4.4 · p. 6

5.1 EFFICIENCY AND CORRECTNESS

• With 10 seeds, training is 102× faster for DeepLTL and 220× for GenZ-LTL; evaluation is 79× and 34× faster, while ZoneEnv success stays within ±1.1% of references.The validation also finds that DeepLTL and GenZ-LTL training dynamics closely follow their references.Source: §5.1 · pp. 6–7, Figure 4 · p. 7

5.2 BENCHMARKING EXISTING METHODS

• The benchmark uses curated finite- and infinite-horizon tasks, generally training 10 independent seeds and evaluating each policy–task result over 512 episodes with 95% Student-t confidence intervals.GenZ-LTL’s standard observation reduction assumes proposition-specific observation components and a hand-designed fusion operator; its unreduced variant is used when those assumptions do not hold.Source: §5.2 · p. 7

5.2.1 GENERAL LTL TASK SATISFACTION (Q1)

• GenZ-LTL performs exceptionally with suitable observation reduction, while StructLTL dominates among general methods in more complex environments; automata-based methods led by StructLTL perform best on recurrence tasks.GCRL-LTL, DeepLTL, and SemLTL perform similarly overall, but GCRL-LTL is unsupported on Warehouse; LTL2Action is consistently outperformed by more modern approaches.Source: §5.2.1 · pp. 7–8

5.2.2 NON-MYOPIC REASONING (Q2)

• On ConveyorWorldSimple-k, GenZ-LTL and GCRL-LTL fall to 50% for k > 1, while full-task methods generally stay strong through k = 32; on ZoneEnv-NM, StructLTL reaches 92.7% and DeepLTL 83.6%.SemLTL reaches 67.5% on ZoneEnv-NM despite full-task conditioning, indicating that the policy must learn to use that information.Source: §5.2.2 · pp. 8–9, Figure 6 · p. 9

5.2.3 SCALING WITH ATOMIC PROPOSITIONS (Q3)

• As proposition count grows, all methods except reduced-observation GenZ-LTL degrade; StructLTL drops sharply beyond 9 propositions, while unreduced GenZ-LTL and GCRL-LTL lose most success by 11.The authors attribute the pattern mainly to increasingly complex feature grounding, with non-myopic methods additionally facing an exponentially growing set of task sequences; GenZ-LTL’s hand-designed reach/avoid features sidestep grounding by construction.Source: §5.2.3 · p. 9

6 CONCLUSION, LIMITATIONS, AND FUTURE WORK

• No evaluated method combines non-myopic reasoning, scaling to many propositions, and independence from environment-specific preprocessing.StructLTL and DeepLTL reason over the full task but degrade as propositions grow; GenZ-LTL scales using observation reduction, which requires manual engineering and remains myopic.Source: §6 · p. 9
• The task suites are finite and hand-curated, so some results may depend on the specific task families used.JAXOLOTL currently supports PPO training; methods also impose restrictions, including known propositions and accurate labelling with privileged state information.Source: §6 · p. 9
• Planned extensions include off-policy algorithms, additional environments, larger proposition vocabularies, richer task distributions, and methods that relax current assumptions.The authors also identify designing one approach with all three desired properties as an open problem.Source: §6 · p. 9

A EXTENDED RELATED WORK

• Prior LTL-RL work includes single-policy-per-specification approaches and reward-machine methods, while multi-task methods seek zero-shot generalisation across specifications.Related approaches include options, formula generalisation, transformer encoders, pretrained DFA embeddings, and learned future-dependent options; most assume a ground-truth labelling function.Source: A EXTENDED RELATED WORK · p. 17
• LTL offers precise semantics and automata for tracking task progress, unlike flexible but ambiguous natural language; other approaches use offline demonstrations or pretrained models.JAXOLOTL instead targets online RL.Source: A EXTENDED RELATED WORK · p. 17
• Existing RL libraries do not natively represent temporally extended tasks, and symbolic CPU-side LTL processing prevents end-to-end JIT compilation.JAXOLOTL adopts recommended evaluation practices, with its efficiency making the required seeds and episodes practical.Source: A EXTENDED RELATED WORK · pp. 17–18

B SEMANTICS OF LTL

• LTL semantics are defined over infinite sequences of assignments to atomic propositions, with satisfaction specified recursively over formulas.The supplied semantics include truth, proposition membership, conjunction, negation, next, and until.Source: B SEMANTICS OF LTL · p. 18

C EVALUATION PROTOCOL

• Independent policies, rather than policy–task pairs, are the statistical units because each run evaluates one generalist policy across multiple tasks.The resulting task scores from a policy are correlated.Source: C EVALUATION PROTOCOL · p. 18
• For each policy, the protocol estimates task-level performance and averages scores across comparable specifications before computing aggregate estimates.Finite-horizon satisfaction is measured directly; infinite-horizon performance uses visits to accepting states, and episode initial states follow the environment’s initialisation distribution.Source: C EVALUATION PROTOCOL · p. 18
• Aggregating scores within each policy before estimating uncertainty preserves correlations among tasks from the same training run.The protocol reports confidence intervals for both individual specifications and task-set aggregates.Source: C EVALUATION PROTOCOL · p. 18
• Two-sided 95% Student-t intervals use 10 independent training runs and quantify uncertainty conditional on the fixed benchmark tasks.Intervals are exact for normally distributed policy-level estimates and otherwise approximate; checkpoint-wise performance curves have pointwise, not simultaneous, intervals.Source: C EVALUATION PROTOCOL · pp. 18–19

D.1 ENVIRONMENTS

• LetterWorld is toroidal 7 × 7 discrete navigation, with 12 letter propositions and reachable assignments limited to singletons or the empty set.Letters are resampled each episode, and layouts ensure avoidance tasks remain solvable.Source: §D.1 · p. 19
• ZoneEnv uses a continuous point robot in a bounded plane with four colour propositions and singleton-or-empty reachable assignments.Its observations combine proprioception with per-colour LiDAR; the implementation uses lightweight point-mass dynamics.Source: §D.1 · p. 19
• FrankaZoneEnv is a configurable 3D Franka Panda manipulation task whose colour propositions encode end-effector visits to virtual zones.Its configurable number of colours makes it suited to studying scaling with proposition count.Source: §D.1 · p. 19
• Warehouse combines continuous navigation with object interaction, allowing multiple propositions to hold simultaneously and yielding 16 reachable assignments.Its five propositions indicate three regions and whether the robot carries a vase or crate.Source: §D.1 · pp. 19–20

D.2 TASK SUITES

• Task suites add challenging specifications to literature-derived tasks, while FrankaZoneEnv receives new tasks spanning complex temporally extended behaviors.Its eight propositions allow greater compositional complexity than the standard ZoneEnv formula set; ConveyorWorld tasks also sample the final sequential reachability proposition between two rooms.Source: §D.2 · p. 20

E SUPPORTED LTL-RL ALGORITHMS

• LTL2Action encodes the progressing residual formula with a relational graph convolutional network, but supports only specifications resolving in finite time.Its formula-progression closure is precomputed offline as a static transition table.Source: E SUPPORTED LTL-RL ALGORITHMS · p. 20
• GCRL-LTL learns to reach individual propositions, then uses a goal-conditioned value function to rank candidate accepting paths at evaluation.Its proposition-based avoidance heuristic does not cover Warehouse’s more complex avoidance requirements, so the method is not applicable there.Source: E SUPPORTED LTL-RL ALGORITHMS · pp. 20–21
• DeepLTL trains on reach–avoid sequences and uses a backward GRU to represent subgoals, including sequences for stability tasks.At evaluation, it enumerates accepting sequences and selects among them using its learned value function.Source: E SUPPORTED LTL-RL ALGORITHMS · p. 21
• GenZ-LTL handles one reach–avoid subgoal at a time using hand-designed observation reductions that retain features relevant to that subgoal.The reduction assumes observations decompose into proposition-specific components; without it, the policy conditions on the full observation and a one-hot subgoal encoding.Source: E SUPPORTED LTL-RL ALGORITHMS · p. 21
• SemLTL conditions its policy on semantic labels of LDBA states, enabling equivalent states across automata to share labels and generalise across specifications.At evaluation, it compiles the new specification and acts directly on labels without search or planning.Source: E SUPPORTED LTL-RL ALGORITHMS · pp. 21–22
• StructLTL encodes reach–avoid formula structure hierarchically and uses attention over future subgoals, with a position bias favoring nearby ones.At evaluation, accepting runs are extracted from an LDBA and converted into candidate subgoal sequences.Source: E SUPPORTED LTL-RL ALGORITHMS · p. 22

F.1 MODEL ARCHITECTURES

• Methods share an observation encoder and separate actor and critic networks, while task encoders and auxiliary networks vary by algorithm.DeepLTL and StructLTL add a masked ε-action head, SemLTL selects among ε-successors categorically, and GenZ-LTL omits the task encoder in favor of observation reduction.Source: §F.1 · pp. 22–23

F.2 CURRICULA

• Curricula are precomputed as static method-specific task arrays, sampled uniformly within each stage, and advanced through a shared frontier with gradual adoption by lagging environments.Curriculum-based methods use feasible, comparable task distributions; GenZ-LTL and GCRL-LTL instead train on a single stage without progression.Source: §F.2 · p. 23

G.1 COMPUTATIONAL EFFICIENCY

• At 2,048 parallel environments, JAXOLOTL is 5,010× faster on ZoneEnv and 35× faster on FrankaZoneEnv than the best reference measurement.On FrankaZoneEnv, it overtakes the reference only from 32 parallel environments; part of the ZoneEnv speedup comes from replacing MuJoCo point-robot dynamics with point-mass dynamics.Source: Figure 7 · p. 24, §G.1 · p. 24

F.3 HYPERPARAMETERS

• Training and model hyperparameters are specified for each method and environment, largely following prior literature where applicable; all experiments use Adam.GenZ-LTL and GCRL-LTL use a single-stage training setup, so curriculum-progression hyperparameters do not apply.Source: §F.3 · p. 24

G.2 IMPLEMENTATION VALIDATION

• DeepLTL, GenZ-LTL, SemLTL, and StructLTL were rerun from their official codebases over 10 seeds and compared with JAXOLOTL implementations on the same ZoneEnv task set.LTL2Action and GCRL-LTL reference success rates instead use results reported by Jackermeier & Abate (2025) on that task set.Source: §G.2 · pp. 24–25
• Figure 8 depicts ConveyorWorld-k and reports non-myopic reasoning results across its step variants.Source: Figure 8 · p. 25
• Figure 4’s training curves show the DeepLTL and GenZ-LTL reruns.Source: §G.2 · p. 25

H.1 PER-SPECIFICATION RESULTS

• Table 5 presents per-specification results for finite-horizon LTL specifications.Source: §H.1 · p. 25
• Table 6 presents per-specification results for infinite-horizon LTL specifications.Source: §H.1 · p. 25
• Table 7 presents per-specification results for reach-stay LTL specifications.Source: §H.1 · p. 25

H.2 NON-MYOPIC REASONING

• ConveyorWorld-k requires choosing a one-way belt, then exploring the destination room to visit k ordered propositions before receiving reward.Source: §H.2 · p. 25
• As k increases, all non-myopic methods degrade severely, with seeds splitting among 100% success, one-room local optima, and no learned reward.The distribution shifts toward the latter outcomes as exploration and credit assignment become more challenging.Source: §H.2 · p. 25
• A multi-stage curriculum did not improve performance; many seeds failed to learn even the first-stage F pk reach tasks.Source: §H.2 · p. 25