One Subgoal at a Time: Zero-Shot Generalization to Arbitrary Linear Temporal Logic Requirements in Multi-Task Reinforcement Learning
Authors: Zijian Guo
İlker Işık
H M Sabbir Ahmad
Wenchao Li
Venue: NeurIPS 2025 poster ()
Keywords: Linear Temporal Logic
Safe Reinforcement Learning
Zero-shot Generalization
Primary area: reinforcement_learning

Abstract: Generalizing to complex and temporally extended task objectives and safety constraints remains a critical challenge in reinforcement learning (RL). Linear temporal logic (LTL) offers a unified formalism to specify such requirements, yet existing methods are limited in their abilities to handle nested long-horizon tasks and safety constraints, and cannot identify situations when a subgoal is not satisfiable and an alternative should be sought. In this paper, we introduce GenZ-LTL, a method that enables zero-shot generalization to arbitrary LTL specifications. GenZ-LTL leverages the structure of Büchi automata to decompose an LTL task specification into sequences of reach-avoid subgoals. Contrary to the current state-of-the-art method that conditions on subgoal sequences, we show that it is more effective to achieve zero-shot generalization by solving these reach-avoid problems $\textit{one subgoal at a time}$ through proper safe RL formulations. In addition, we introduce a novel subgoal-induced observation reduction technique that can mitigate the exponential complexity of subgoal-state combinations under realistic assumptions. Empirical results show that GenZ-LTL substantially outperforms existing methods in zero-shot generalization to unseen LTL specifications.

One Subgoal at a Time: Zero-Shot Generalization to Arbitrary Linear Temporal Logic Requirements in Multi-Task Reinforcement Learning
Zijian Guo', iiker Işik², H. M. Sabbir Ahmad', Wenchao Li DDivision of Systems Engineering, Boston University Department of Electrical and Computer Engineering, Boston University {zjguo, i iilker, sabbir92, wenchao)@bu. edu
Abstract
Generalizing to complex and temporally extended task objectives and safety con- straints remains a critical challenge in reinforcement learning (RL). Linear temporal logic (LTL) offers a unified formalism to specify such requirements, yet existing methods are limited in their abilities to handle nested constraints, and cannot identify situations when a subgoal is not satisfiable and alternative should be sought. In this paper, introduce GenZ-LTL, method that enables zero-shot generalization to arbitrary LTL specifications. GenZ-LTL leverages the structure of Büchi automata to decompose an LTL task specification into sequences of reach-avoid subgoals. Contrary to the current sate-of-the--a method that conditions on subgoal sequences, show that it is more effective to achieve zero-shot generalization by solving these reach-avoid problems one subgoal time through proper safe RI. formulations. In addition, we introduce a novel subgoal-inducee observation reduction technique that can mitigate the exponential complexity of subgoal-state combinations under realistic assumptions. Empirical results show that GenZ-LTL substantially outperforms existing methods in zero-shot generalization unseen LTL specifications. The code is available http: http:///w........EE/////////////
tasks and safety
Introduction
Generalization is critical aspect of reinforcement learning (RL), which aims to develop policies that are capable of adapting to novel and unseen tasks 38
48 21 and varying safety constraints [7].
Various methods have been proposed and show promising results in applications such autonomous
driving [49] 36), robotics [37] 33 28), and healthcare [8] [1] However, most existing approaches fall short in handling complex and temporally extended task objectives and safety constraints. For
example, an autonomous vehicle may be instructed to reach a sequence of destinations for passenger pick-up and drop-off while adhering traffic rules such as speed limits and yielding at intersections.
Temporal logic provides principled framework for specifying system behaviors over time. Linear temporal logic (LTL) [39] in particular, has been considered extensively in single-task and multi- task RL settings 20 29 51). LTL has well-defined semantics and a compositional syntax, which facilitates the unambiguous specification of task objectives and safety constraints. However, existing methods often fail to account for the potential conflicting objectives within a specification [50 40 23 For example,
autonomous vehicle navigating between multiple destinations aims to minimize travel time, but adhering to speed limits and other safety constraints may slow the vehicle down. In such cases, the vehicle must prioritize satisfying safety requirements over optimizing for travel time.
39th Conference on Neural Information Processing Systems (NcurIPS 2025).

---

In this paper, we propose a novel framework, called GenZ-LTL. for learning RL policies that generalize in zero-shot manner to satisfy arbitrary LTL specifications, including both finite-horizon and infinite-horizon tasks. We adopt the subgoal decomposition approach, which exploits the structure of the equivalent Büchi automaton to decompose an L.TI. specificaati into individual subgoals, each comprising reach component that defines task progression and an avoid component that encodes safety constraints. We show that training goal-conditioned policy to achieve the subgoals one at time, which is often perceived myopic by existing literature, is more effective in general than conditioning the policy on subgoal sequences [23] or the entire automaton [54]. This somewhat surprising result stems from two key innovations in this paper: a proper safe RL formulation with state-wise constraints for solving the individual reach-avois subgoals, and a novel subgoal-induced observation reduction technique to address the exponential complexity of inservation-subgonn combinations. The former builds on recent advances of Hamilton-Jacohi reachability in RI. [12] whereas the latter exploits symmetry in the state observations to extract information only relevant to the immediate subgoal. To zero-shot generalize to arbitrary LTL specifications at test time, we use the equivalent Büchi automata as well as the learned value functions to guide the subgoal selection. Our main contributions are summarized as follows.
We propose a novel approach for learning RL policies that can satisfy arbitrary LTL specifica- tions in a zero-shot manner by sequentially completing individual subgoals. To our knowledge. this is the first safe RL formulation with state-wise constraints for LTL task satisfaction.
We introduce subgoal- inguuuedd observation reduction technique to mitigate the combinatorial explosion of observation-subgou pairs and enable efficient generalization, along with timeout mechanism that handles subgoal switching and unsatisfiable subgoals.
We conduct comprehensive experiments across set of navigation-style environments and diverse task specifications, demonstrating that our method consistently outperforms state-of- the-art baselines in zero-shot generalization to arbitrary LTL specifications.
2 Related Work
Specification-uiieed and goal-conditioned RL. Various methods have been proposed to guide RL agents by extending traditional goal-conditioned RL [35 to temporal-logic goals. Early works focused on learning policies for a single and fixed specification, including methods based on LTL specifications and automaton-like like models 20
46 45 3] and methods leveraging quantitative More recently, the importance of adapting to changing conditions in real-world applications has brought increased attention zero-shot generalization to new specifications. Existing approaches can be broadly categorized into subgoal decomposition [30] 34 [23] and direct ppecifcation/automaaaa encoding [50 55). Our work follows the direction of subgoal decomposition, but shows that it is more effective to solve the subgoals one at a time through proper safe RL formulations and subgoal-induce observation reduction.
18
51
semantics of specifications [32 26
16
RL with safety constraints. Various methods have been proposed to solve RL problems with safety constraints, such as policy optinization-based methods [59] 56 24 (33, Gaussian processes-
based approaches [52] (60]. and control theory-based methods, including Hamilton-Jccobian (HJ)
reachability [10 57
61 and control barrier functions [14
6 We point the readers to [T5]
for a comprehensive survey of safe RI. techniques. In the context of formal specification-guiie -uuidd
RL, the interplay between task progression and safety constraints remains underexplored. Most existing methods simply assign positive reward when a specification or a subgoal is satisfied, and negative reward at episode termination if unsatisfied. This approach is ineffective achieving safety I 4, especially when the task progression objective and the safety requirements exert conflicting influences on policy learning. In this paper, we show how to prioritize safety satisfaction properly by incorporating Hamilton- -Jacbii reachability constraints.
3 Preliminaries
Reinforcement learning. RL agents learn policies by interacting with enviromments, which is usually modeled as a Markov Decision Process (MDP), defined by the tuple M := (S, A, P.r, 7, do). where S is the state space and A is the action space, P S x A S + [0, 1] defines the transition dynamics, S x A + the reward function, 7 E [0, 1) the discount factor, and dg E ASS) is the initial state distribution. Let S x A A+ [0, 1] denote a policy and {st, at T Tio denote a trajectory

---

where r, = =r(s;, at). The value function under policy ग is (s) = Byno, 80== 2==0 y'r,] and the corresponding state-action value function is O (s. Rey =0= Dt= 7/re]- An additional constraint violation function h S
can be used model state-wise safety constraints, such that a state s is considered safe if (ss) S. 0 and unsafe if la(s) > 0. The reachability value function ViT(s) is defined (s) == m (()), Su s, a ~ that captures the worst-case constraint violation under policy x from state s. The largest feasible set contains the largest set of states from which the agent can reach a goal safely: S := {s 3x, V (s) 0}. To handle such constraints, Hamilton-Jacon Jacobi (HJ) reachability has been incorporated into RL [12] by simultaneously learning the
reachability value function to estimate the feasible set and learning the policy:
max Eg (s) 1[s Sy] V (s) [s & Sy]l s.t. V7 S 0, E Sy no
where Sy : {s s do) } is the set of initial states, Intuitively, the goal is to maximize expected return and ensure safety for initial states within the largest feasible set, while minimizing the reachability value function for states outside it, where constraint violations are inevitable.
Linear Temporal Logic. LTT. 39 is a formal language for specifying temporal properties of a system. LTL formulas are built from a set of Boolean operators negation (-), conjunction (A), disjunction (V), and temporal operators - "until" (U), "eventually" (F), and "always" (G). Given a finite set of atomic propositions AP and AP, the syntax of LTL defined recursively as:
6 a - P1 A P2
p1 V P2 F G p1 U P2
Intuitively, the formula 1 U p2 holds if yo is satisfied at all time steps prior to the first occurrence of P2- The operator F op holds if yp satisfied at some future time, while G holds if yp is satisfied from the current step onward. To relate LTL to MDPs, we assume a known labeling function L S - 24P that maps each state to the set of true atomic propositions. The satisfaction probability of y under policy is Pr(T - s) Er-r [1[r F E]]. where т } yp denotes that the trace of the trajectory, TT(T) = (()))[(s)
satisfies the formula yp, and is the indicator function. We are interested in training a policy that maximizes this probability for an arbitrary yp
Büchi automata and subgoals. To enable algorithmic reasoning over LTL specifications, we use Büchi automata (5) as a formal representation of temporal-logit formulas. Given an LTL formula p, the corresponding (non-deterministic) Büchi automaton is defined by a tuple B, == (Q, 3, F.))) where Q is the finite set of automaton states, Σ 2 the finite alphabet, 8 C Q x Σ Q the transition relation, F C Q the set of accepting automaton states, and qu the initial state. An infinite I" induces a run r = 9091 ... over w if for every i 2 0. (g., Ciy. 9++1) E 6. A run r is accepting if it visits an accepting state infinitely often. A product MDP MMP [ synchronizes given MDP and Büchi automaton with a new state space S S x Q and a transition function pe ((s', (') (s. q), a) that equals P(s') 18 a, if a E A and (4, I(s). g') E 5, and 0 otherwise. In practice, rather than explicitly building the product MDP, one can simply update the current automaton state q with the propositions L(s) observed at each time step. Given state 9. reach subgoal is defined as an o E such that (q, a .q') E å and g and q' are consecutive automaton states along avoid subgoal is defined as an a E Σ
word w = ag
some accepting run, and q' & if q & F. Conversely, such that (g, or "=,''') 8 and q and o' are not consecutive automaton states along any accepting run. Intuitively, reach subgoal indicates progression towards satisfying the LTL specification, and an avoid subgoal indicates a way that leads to violation of the specification.
4 Method
In this section, we present our proposed method, as illustrated in Figure 1 During training, we begin by sampling subgoals (possibly empty) set of avoid subgoals (and a+ & A-). Given the current state and subgoal a, we apply subgoal-induced observation reduction (details in Section 4.2). when applicable, to obtain a processed state s². We then train a general reach-avoid its corresponding value functions. During testing, given a target LTL task specification ya, we first construct an equivalent Büchi automaton, and then extract a set of reach-avoid subgoals )o,) ) based on the current MDP and automaton state. For each candidate subgoal d; we compute 8 and evaluate the value functions to select the optimal subgoal o². The agent then generates actions a according to x (a]ss"). ). In Section 4.1 4.11 we describe how to construct reach-avoid subgoals from a Büchi automaton. In Section 4.2 we introduce subgoal- -adgoal-induced observation reduction technique to
(a+ "o+,,A),, AA),, where at is a single reach subgoal and A is
cobgoal-conditionee policy along with
3

---

Training
Testing
Environment
Agent W
LTL. fomrula
Environment
Subgnal-inducced obsrrvation reduction
Biihi Automatt
Agent
Subgoal
sampler
(or
Exemet subgozi
An
Subgnal-induced observation reduction
condriattes
Figure 1: Overview of GenZ-LTL. During training, we sample reach-avoid subgoals o o= (a+ ) and apply subgoal-induced observation reduction to learn subgoal-conditione policy and value functions. test time, given a target LTL formula ye, we construct the corresponding Büchi automaton and identify candidate subgoals based on the current automaton state. The optimal subgoal o² is selected using the learned value functions, and the policy generates actions conditioned on o².
mitigate the exponential complexity arising from the combination of subgoals and MDP states. In Section 4.3, we detail the learning of value functions and policies under reachability constraints to comply with the safety constraints (A-) while optimizing for the task progression objective (ar+).
4.1 Reach-Avoid Subgoal Construction from Büchi Automaton
Büchi automata can be represented directed trate-trnnsttinn graphs 40), and an accepted run can be viewed as having a lasso structure with cycle containing an accepting state and prefix path that leads the cycle. Similar to existing approaches 40 23), we use depth-first search (DFS) over the state-trane transsrtanttion graph to enumerate all possible lasso structures starting from a given state q. From these lasso paths, we extract the set of reach subgoals, denoted by A+, following definition in Section 3 Similarly, we extract the set of avoid subgoals A by considering transitions to state that is different from q and not along any of the lasso paths. Each pair (a+ E A+ A-) then becomes candidate reach-avoid subgoal. To satisfy subgoal (a+t, (A+,A")) ). the agent must visit a state 8 such that L(s) = at, while avoiding any states labeled with propositions in AT For example, for (A+ = Ha, b), {c)},
A A- {{d), {e])), it forms subgoals 0 = (4a A A-) and T2 = (fc}. ). and the agent can choose to reach a state labeled with a A or a state labeled with while avoiding states labeled with d and in both cases. While our method follows similar subgoal decomposition approach as prior works, the way that we solve the reach-avoid subgoals is significantly different. In fact, straightforward way is encode a reach-avoid subgoal as bitvector of dimension AAP| + 2|AP), where the first |AP| bits encodes the reach subgoal, and the rest of the bits encode the avoid subgoal.
4.2 Subgoal-Induced Observation Reduction
Given reach-avoid subgoal, our next step is to train subgoal-conditioned policy based on the MDP state or observation of the MDP state, and the subgoal. However, notice that the number of possible subgoals grows exponentially with the number of atomic propositions. Additionally, in order for the agent to complete task in such complex environment, it needs to be able to make observation of every subtellubooal combination, i.e. being able to determine the label L(s) of state s that observes (possibly indirectly through an observation function o). Otherwise, task completion cannot be determined in general. For instance, if the task requires the agent to reach a 'green' region, then an agent equipped with only 'blue' sensors cannot leam accomplish this task if the green and blue regions are placed randomly in the environment. Thus, the number of observations that the policy also grows exponentially with |AP], and directly learning a goal-conditioned policy this way quickly becomes intractable as [AP| grows. While various dimensionality reduction techniques have been proposed in the RL literature 22] 19 58 they are based abstraction or bisimulation of the MDP states, and do not consider state-subgoal combinations.
needs to condition
In this paper, we introduce a novel nubgoal-inducee observation reduction technique that can circum- vent this exponential complexity. The key observation that, ultimately, each subgoal reduces to reach-avoid problem, where there is some state that we want to reach while avoiding some other states. In other words, what really matters whether a state is 'reach' or 'avoid", and not its label T.(s) once subgoal is fixed. Thus, can perform symbolic simplification of the statc/observation space

---

feasible set, along with the subgoal while preserving information essential for solving the reach-avoid problem. Formally, for an MDP state s, we assume that it can be partition into component 8 -AP and proposiion-depender component SAP (e.g, the blue and green sensors). For the cepositioo-dependeen component, we further assume that it can be broken down into individ- ual observations each corresponding to an element in 2AP, and the observations are produced by identical observation functions under output transformation. We say that two observation functions (with a slight abuse of notation of s), 01 (s) E K and 02(s) E R are identical under output transformation g if Vs, 01 (s) = ((02(s)). For instance, suppose 01 (s) E R6: is a LiDAR sensor for sensing the shortest distance to blue state along each of its 360 beams, and (s) R is the same type of LiDAR sensor for sensing the shortest distance to a green state but rotated 180", then g is the 180 rotation (a permutation of the beam indices). Then, we can reduce the pepposiiion-depeddeee component (of size k x 2|AP)) and the encoding of reach-avoid subgoal (of size (IAP)- 2 APl) into just two observations each of size k, where the first observation is an observation corresponding to the reach subgoal and the second observation is a fused observation of the observations corresponding to the avoid subgoals. For simplicity deriving fusion operator that preserves task-relevant semantics such distances to avoid zones, assume that the (ss) are coordinate wise monotonic. The actual it will be an elementwise min over R Implementation details are provided in Appendix B Empirically,
fusion operator f is environment/senor-ppee specific- - in the LiDAR example, as shown in Figure 2
we demonstrate the benefits of this reduction, when it is applicable, in Sections 5.3 and Apendix
Environment
Suhgnal induccdd observation reduccion
NAP
Life L.D.
Foud - Agps titifho Aptan?
Agent
Subgoal
n [o", )
[pree]
[[Ma]] [edow]] Unaad Macse ycloo)
sampler
Figure 2: Illustration of the subgoal- -nduuued observation reduction for LiDAR observations. The environment provides the raw state consisting of proposition coopoitioonindeeendenn component S-AP and proposition-dependee component SAP. Given a subgoal a, SAp is reduced to two vectors; a reach observation and fused avoid observation. Together with the .PP, these form the agent's 's input.
4.3 Goal-Conditioned Policy Learning with Reachability Constraints
A key difference between our approach and existing subgoal-based approaches lies in the treatment of the avoid subgoal. We treat an avoid subgoal as hard constraint, since whenever a violation occurs, satisfying the LTL formula becomes impossible. For example, consider the specification -a U b. where a and b are atomic propositions; this requires the agent to avoid reaching any state labeled with until a state labeled with b is reached. If a is encountered before b, the whole trajectory can no longer satisfy the specification. To enforce these hard constraints, we leverage the notion of HJ reachability as introduced in Section and formulate RL objective follows:
max Berdd (V*T(T") 1[s E S71 V, (s*) )- 1[s" $ s71]
s.t. Vi, 0, E SJ n
, Vo ~ Unif(g)
where & is the set of all possible subgoals (details on its construction are provided in Appendix B 8² := [(s. o) is the processed state if the observation reduction is applied, and 8 := (s. o) otherwise, S7 == (s" | 3π, V (s") I 0} denotes the largest bubgoal-dependee Sg == (8" 0. 8= ~ do) denotes the set of processed initial states given a subgoal a, and V, (s") is the reachability value function of a policy starting from a processed state s" with the current subgoal o. We use π as a shorthand for the policy π (a) s²"). However, since Sy is unknown when learning policies, directly solving Eq. ① is not possible. Inspired by previous methods [1.57]. we convert the objective into the following constrained policy optimization problem:
π A (s
T = arg max (g. TamiT
T
s.t. Ug (DKL (TT, mx) Se
(2)
E Eo annts (1 - (T))
T A (s a)
50
n
5

---

where A7(s", a) := Q7 (**) and aa) == 27 .0) (s") are the ad- vantages functions with (T .a) == m h(s)), 8o = s" , ag a, maxteN h(.),a a ~ π is the maximum safety violation for trajectory under policy л. By maximizing the discounted cumulative reward, the policy optimized to effectively satisfy the reach subgoal, while the safety constraints ensures that the avoid subgoals are satisfied, Then we incorporate the clipped surrogate objective [43] to handle the trust-region constraint and a state stete-dependent Lagrangian multiplier [57] to enforce the state-wise safety constraint:
and (n(T) :=
min max (agd X20 a
min
A. (8,,a)
a): clip
c, +,1+))
(8
(3)
X(5 ((s)((1 Jn
- (s" [a)] Th
The overall method is summarized in Algorithm T The training process of our method is simple compared to previous methods that sample full LTL specifications [50] 40] or employ curriculum learning that gradually exposes the policy to more challenging reach-avoid sequences [23]. We sample one subgoal at a time, apply observation reduction to obtain a reduced state when applicable, and execute the policy collect data. When the subgoal is satisfied, a new one is sampled, and this cycle continues until the episode terminates due to reaching the maximum length or subgoal violation. During evaluation, given an LTL formula yo, we convert a Büchi automaton and track the current automaton state q. We identify the set of candidate subgoals {or } J==1 that can advance toward satisfying sp. The subgoal that achieves the best trade-off between task progression and satisfying safety constraint is selected as o² arg max, V, (s) A(s V (s"). The agent takes actions based on the selected subgoal and updates upon each transition to a new automaton state.
Subgoal switching, In general, we cannot determine priori whether a selected subgoal is satisfiable the environment. To handle this issue, we introduce mechanism to identify unsatisfiable subgoals and allow the agent to switch to alternative ones. The mechanism is triggered if the current subgoal is not satisfied within a timeout threshold, which set to (1 + Guaale) Hsubgoal where Hsubgoal denotes the maximum number of steps required to complete a subgoal after policy convergence during training, and Gscale is a scaling factor. When a reach subgoal times out, the best option from the remaining reach subgoals in A is selected. This procedure is sound because the avoid subgoals are respected during the attempt for the prior reach subgoal(s). Appendix B.2 provides further details.
Remark. there is no more subgoal remaining, our method returns failure. However, this does not necessarily mean that the specification unsatistiable. It possible that the specification is satisfiable but the greedy nature of solving the subgoals sequentially prevents us from finding solution. In general, unless the environment MDP is known, cannot determine a priori if the LTL specification is satisfiable or not. If the agent is allowed to reset in the same environment, then one can enumerate the possible subgoal sequences from the initial state of the automaton.
Experiments
In this section, we evaluate our method GenZ-LTL in multiple environments and across a wide range of LTL specifications of varying complexity to answer the following questions: Q1: How well can GenZ-LTL zero-shot generalize to arbitrary LTL specifications? Q2: How does GenZ-LTL perform under increasing specification complexity and environment complexity? Q3: What are the individual impacts of the proposed observation reduction and safe RL approach? Additional evaluations and results in are provided in Appendix C
Environments. Our environments include the LetterWorld 7 discrete grid world with discrete actions where letters are placed at randomly sampled positions, and the ZoneEnv environment [50], a tigh-dimensional envi- ronment with lidar observations, where a robotic agent with continuous action space must navigate between randomly positioned colored regions. We exclude the FlatWorld envi- ronment (23 51] from our experiments, as its configuration is fixed and the state space includes only the agent's 's (æ, y)- position, without any information about the environment state. We also consider variant of ZoneEnv that contains over- lapping regions which by design more challenging than FlatWorld. Additional details are provided in Appendix A.
environment (50]
6
Figure 3: Environment illustrations of LetterWorld and ZoneEnv with example trajectories for -l U j and -green U blue, respectively.

---

Baselines. We compare GenZ-LTL against the following baselines, all of which train a goal- conditioned policy of some sort: 1) LTL2Action [50], which applies technique called LTL pro- gression to dynamically track the parts of a specification that remain to be satisfied, and use graph neural network to encode the specification; 2) GCRL-LITI 40), which uses a heuristic to identify the optimal subgoal sequence; 3) DeepL.TI. [23]. which learns policies conditioned on embeddings of subgoal sequences; 4) RAD-embeddings [54]. which pre-trains embeddings of compositions of deterministic finite automata (DFAs) and learns policies conditioned on these embeddings. While these baselines consider safety, as the LTL specification itself can involve the notion of safety, they do not model safety constraints explicitly in their RL formulation. Further details of the implementation
are provided in Appendix B
LTL specifications. We consider a wide variety of LTL specifications with varying complexity.
including (1) sequential reach-only specifications of the form F ((1 A (F 02 A (... A F Fon)): (2) sequential reach-avoid specifications of the form -01 U (az A (~a3 U (a4 A... A (-0,,1 U a.,)) )), and (3) complex specifications that combine reach-only and reach-avoid properties. We also conduct a separate evaluation infinite-horizon tasks that span a diverse set of LTL objectives, including safety, liveness, and their combinations. The specifications used for evaluation are listed in Table [ and a full set of specifications is provided in Appendix A.2 with trajectory visualizations in Appendix D In this section, all specifications are satisfiable.
Table 1:
LTL specifications used for evaluation. For specifications in ZoneEnv, b, g. m, and denote blue, green, magenta, and yellow, respectively. Results are shown in Table and
Latteroorld
ZonaFny
(-b
Vb (Fb) (-b (y)))))
#: (
Pha (m (b)
U (bA (de (N))
Pa U A
Fi (avbvevd (CAF U (hAFi)
iha (g (-y Um)) Yyy
Finite-horizon
ihu (g< Uy U (-g
She (ib (ly (( mmjlii (y ((bb
-(jbvdd U (=
iis <mmy)) (
gt -(f U. (M(=bUe)AF((AA(=UUR
F F(bA gha
GF(e U G()vd-
GFB GFBA CaFFFgGG--yyi
Infiiiteborizoo 0/ GFuA.FFAAGEAGG-iieVVV
ab. GFbA.GFAAGFAAGG
GFEAGFAAGF/eM( GFRAA-TVV
sh. FGyAG-(gVbVmm
Evaluation metries. For fair comparisons, follow the standard practice of executing a determinis- tic policy by taking the mean of the action distribution [22). For each LTL specification, we report the following rates: success rate 77 defined as the ratio of trajectories that satisfy the specification; violation rate 7/. defined as the ratio of trajectories that violate it; and other rate no = 1 - (77 + nt). We also report the average number of steps μ to satisfy the specification among successful trajectories as secondary metric, as step count is less important when the success rate is low.
5.1 Can GenZ-LTL zero-shot generalize to arbitrary LTL specifications (Q1)?
Finite-horizon tasks. We first evaluate finite-horizon tasks, i.e. tasks that can be satisfied with finite- length trajectories. All the specifications considered are complex LTL formulas with nested temporal and Boolean operators (details in Table []. The evaluation results are shown in Table 2 Our method consistently outperforms the baselines in terms of both success and violation rates. I.TI 2Action encodes the full structure of the current LTL specification, making less effective adapting to -i--o--dittiittion (OOD) specifications at test time. GCRL-LTL Iearns a goal-conditioned policy but does not model safety constraints explicitly, limiting its ability enforce constraint satisfaction. DeepLTL relies on curriculum training which samples random reach-avoid subgoal sequences only up to certain length. When evaluating specifications (o-11 although the specifications themselves are unseen, the underlying subgoal sequences are likely to have been encountered during training, leading to better efficiency, i.e., smaller u. However, for specifications with longer subgoal sequences, e.g. P13- which are OOD with respect to the training sequences, DeepL.TL exhibits reduced performance. RAD-embeddings pre-trains the automaton embeddings by sampling from a fixed distribution. As result, it also struggles with the issue of OOD generalization when faced with unseen
7

---

Table 2: Evaluation results for success rate 7/,, violation rate 7/e and average steps μ to satisfy the complex specifications listed in [ Specifications (1-(ps are evaluated in LetterWorld, and (P-- in ZoneEnv. (91- and 4o-1 P13--91.. t: higher is better; J: lower is better. Bold: the best performance for each metric. Each value is averaged over seeds, with 100 trajectories per seed.
from [23] and we construct more complex PP--is and
LTL2Action
OCRL LTL
DeepLTT
RAD embeddiigs
GeaZ (TL(suss)
8112am
0.00gave
1877
0
U.llllas
23.5
g.00
0.00pan
0.77
156
1000g 20000
(175warr (cHfas
0.77aa
0.0
0.00.ame
0.80
0.08
0.000am 0.000aam
LateWWed
0.56ux
0,00.a00
0.90uaue
0.00..00
0.00
7.061125
0.00uri1
0.00..oo
18.7811
0.08aat
0.00
7.4.a
Ase, 0:62uss 6.07
25.84ss5t
087am
0.03aas
16
0.00
7.
0.00uc
17.70
0.08.aaz
0.00
1.22.LLa
0.00gaan
0.07
20.53c
0.00ga
12,24
2.00
26 20
0.00g
0.00
10
0.18pxa
0.00.000
25,40a635
0.700
0.35amm
14.00cm
0.00ga
0.00.a0e
19 Ra
0.9Guaat
0.00
1.48
0.14emm
19.57amm
0.7laaoo
0.00-ax
11,80am
0.73ccm
0.77mmm
0.98gim
0.000ga
10.9
37,50423
0.00-au
11,200m
0.20sem
0.13mom
25 Olaam
0.33gga
0.000
10.20
Avc, (.3kwaz 0.50uss
0.11aom
18.7
(.7iaass 0.Mlaao
0.82ac
0.7
2: 2:20
0.00 0.95paa
(.15wass 0.18aas
0.83.
0.00amm
476,llamia
(.8laa 0.Mlaa 527
0.90acm
0.88amm
0.90gam
0.01gam
yhu (..0uaz (..8aa.. 121
0.8.
S1S (Seass
0.88aas 0.00aax 221.9
0.90c
0.08mmm
901.
0.97gam
0.02gaaz
25 ela
Puu 0.82aus 3.88mm 256.4,ass
0,06
136,9411a
I.DLas (.MLaae 215.42.15m
0.00aa
0.44ma
247.53uass
0.00
0.01
20.07
ihu (.9kum 0.02um 122.90_axn
0.00aa
0.05amm
136.30azee
(.95aax, 0.0laae
116.00gaar
1.00
0.00
106.97
1.00
0.00
ii Ave, 1.57uur 0.3Tunai 333
0,00000
300,25111 u RtMlaso (.M
220.39.mm
0.M4ca
200553100
0.00gam
3.00 26 Wll
Phu 0.FFunas 8.0am SStUMigaaa 0.73am
0,0910m
0.00
0.01ac1
0.00..0e
0.08
2.00 no 436.25..1.s
you (1Slusms (601es 885 Veii 0.00e
0.11am
611.7l-uu
0.00gamm
(73
0.77 ni (000give 618
08.57
0.08gsn
0.000gam is 451.45
the 0.08.nm, 9.10aaa 565.00 0.70.e
0.30mmm
(.78.a
0.12-a
0.22..
0.22eem
65001lamm
0.07gin
0.01gams 385.01gima
you (.08ur. 0.02ar. 361 19 0ffaa
0.00.
0.00
0.00
0.00 0.00 306.85.
Ave. 8.12aax 8.1Taa. 500.20,.o. 0.70am 0.0 EX0.2 0.5.a 0.0.aa
0.30a 175.1
0.00
0.08 1.M0 118.71.. 20
automata, which is reflected in its performance degradation under more complex LTL specifications: the success rate drops from 0.9 on 4f141 to 0.82 on 495-8 and 0.94 on (Py-12 to 0.7 on P13-16- In contrast, our method conditions only on the current subgoal, sidestepping the issue of OOD subgoal sequences. By incorporating an HJ reachability constraint, our method improves adherence to safety constraints. Additionally, since we optimize for the discounted cumulative reward obtained upon satisfying subgoal, efficient policies that take fewer steps are encouraged. We further evaluate our method in ZoneEnv with agents featuring more complex dynamics, which induce additional hard constraints such as preventing head-down falls. Our method consistently outperforms the baselines in both success and violation rates. Details of the setup and results are provided in Appendix C
Table Evaluation results for violation rate T7 and average number of visits to accepting states Mace on infinite-horizon tasks listed in Table [ Specifications V/-tbs are evaluated in LetterWorld, and 4 in Env.Env. 1: higher better; I: lower is better. Each value is averaged over seeds, with 100 trajectories per seed. Bold indicates the best performance for each metric.
LetterWorld
ZoneLay
Methods
Metrics
59
a/s
5/4
5%
GenZ-L)LL(ouss)
206. 10.00
102. 122.122
35.17g1.00
35.10.... an
$2. $2.78gn..n
8135.61
22
g.00
0.00
0.00
0.07 30.00
3.08
0.08
DespLITL
Mac
142.56gax.i
15.28
19:2 19:21g
30.03
15.70
7337.38
(337.38gamn
2.04
2.00
0.00
0.3 0.30
0.38
0.18
GCRL-LTL
Mar
41 11:
22, 77.7 oo
9.50
30 20
61 m
3384.4gaaan is
4.18
0.30ge.1a
a.37
0.40
0.144001
Infinite-horizon tasks. Next, we evaluate performance on infinite-horizon tasks, i.e. tasks that can only be satisfied with infinite-length trajectories. RAD-embeddings is excluded from this evaluation, as DFAS cannot represent such specifications. Since it is not possible to simulate infinite trajectories in these environments, we set the maximum episode length to be 10 times of the length used during training. The evaluated specifications are listed in Table [] and results are reported in Table [3] including the average number of visits to accepting states for non-violating trajectories Mace and the violation rate that is calculated based on the proportion of trajectories that violate the G-a constraint in the evaluated specifications. For example, in the specification GF A G 012 A...A GF an A G -o,, each successful cycle of a1-00n-1 (in any order) increases Plces while any visit to an counts as a violation. In the case of Ga, plac is computed as the number of consecutive steps, counted backward from the final timestep, in which holds. As shown
8

---

in Table 3 our method outperforms the baselines on both metrics. By conditioning only on the current subgoal, it naturally extends to shinite-horizon tasks. The agent can follow the infinite subgoal sequence extracted from the automaton one subgoal at a time. The integration of reachability constraints further enables safe execution, whereas the baselines often struggle to satisfy safety constraints in long-horizon settings.
5.2 How does GenZ-LTL perform under increasing specification complexity and environment complexity (Q2)?
To further evaluate the zero-shot adaptation ability of our method, we design experiments that test performance under increasing complexity in specification and environment: (1) Subgoal chaining: we evaluate performance on reach-only and reach-avoid specifications with an increasing of sequence length of subgoals up to n 12; (2) Environment complexity: we vary the region size and the number of regions associated with each atomic proposition; and (3) Unsatisfiable subgoals.
DeepLTL
GCRL-LTL
LTL2Action
GenZ-LTL(oous)
Reach-only specifications
Reach-avoid specifications
16
Op C4
0:"
f)
00 63
06
04
02
06
61
Sequence length n
Figure 4: Performance in ZoneEnv under increasing subgoal sequence lengths, showing success rate Ta. violation rate 7u. and others rate To- We use reach-only specifications with sequence lengths {4, 6, 8, 10, 12) and reach-avoid specifications with E {2, 4, 6, 8, 10). The specifications are shown in Table Each value is averaged over seeds, with 100 trajectories per seed.
Subgoal chaining. In this experiment, we increase the number of subgoals that the agent must reach sequentially. Since satisfying longer specifications naturally requires more steps, double the maximum episode length used in Section 5.1 The results are shown in Figure 4 For the reach-only specifications, the performance of Deepl.T.. TT. and GCRL-LITL degrades more rapidly grows. In the case of DeepLTI., it suffers from OOD specifications that involve longer subgoal sequences than those used during training. GCRL-LTL performs the worst as it struggles complete the subgoals in an efficient manner, preventing it from reaching all the subgoals within the maximum episode length. LTL2Action performs better than DeepLTL and GCRL-LTL as the corresponding graph structures remain relatively simple compared to the complex and nested specifications Section Our method maintains high success rate and low violation rate despite the increase in sequence length, as it solves one subgoal at a time, thus avoiding the distribution shift that affects other methods and resulting in better generalization. For reach-avoid specifications, where safety satisfaction is critical, we can observe that our method achieves near-zero constraint violations compared to the baselines, which validates our safe RI. approach with reachability constraints.
reach-only specifications,
DeepLTL
GCAL-LTL
LTL2Action
GenZ-LYL(ours)
342
404
06
4
XX
55
14
14
14
04 04
15 44 46
Zone size
Zone count
Figure 5: Performance in ZoneEnv under varying environment complexity. including different zone sizes and different numbers of zones per atomic proposition. Visualizations of the environment layout are provided in Figure [6] We report success rate 7/s, violation rate 7/, and other rate 7)-- The default zone size is 0.4, and the default number of zones per atomic proposition is 2. The evaluated specifications are the reach-avoid specifications with n = 2 shown in Table

---

Environment complexity. We next investigate the impact of varying environment complexity performance. The results are shown in Figure As the zone size increases or the number of zones associated with each atomic proposition increases, satisfying the safety constraints becomes more challenging. While all methods experience performance degradation, our method achieves the highest success rates and the lowest violation rate, which highlights its better ability to comply with safety constraints and generalize under environment variations.
Unsatisfiable subgoals. To evaluate the subgoal-switchee we use a satisfiable specification that contains an unsatisfiable subgoal: Φ1 -yellow U ((blue A green) V magenta) in ZoneEnv. We randomly generate region layouts such that the green and blue regions (without overlaps) are positioned closer to the agent than the magenta region. In this setup, blue A green usually selected as the first subgoal based on the learned value functions. As shown in Figure (6] the baselines struggle to satisfy the specification: the subgoal unsatisfiable due to non-overlapping regions, and the agent gets stuck due to the lack of mechanism to switch to an alternative. In contrast, our method can escape this deadlock by selecting an alternative subgoal. The trajectories in Figure in Appendix C further illustrate this behavior.
mechanism,
Unsatisfiable subgoals
LTLZAction
GCRL-LTI
DeeptTl
Ours
Figure 6: Evaluation re- sults on tasks with unsat- isfiable subgoals.
5.3 Ablation study: what are the individual impacts of the proposed observation reduction and safe RL approach (Q3)?
We consider ZoneEnv environment with one region per color and reach-avoid specifications with sequence length of 2. The environment layout is randomized a controlled manner such that the region to be avoided is placed between the agent and the region to be reached according to an LTL specification. Under this setting, the agent must first circumvent the avoid region before reaching the goal region. For example, consider -magenta U blue, the magenta agent and the blue area. We construct a variant of our method by removing the observation reduction module and instead encoding the subgoal using the bitvector encoding discussed in Section 4.1 We also include DeepLTL as a reference, as it achieves the best performance among the baselines. The results are shown in Figure 7 We can observe that integrating the state-wis wise constraints leads to improved safety performance compared to the baseline method, and further incorporating the subgoal-indue induccdd observation reduction technique improves performance by significantly reducing the input dimension of the policy.
fr
Letrowellerte
Zonatne
is placed between the
0670 571
(wlo 5*1
Figure 7: Average performance of success rate 7) violation rate Te others rate Yo for Ours(w/o s"), Ours and DeepLTL for reference.
6 Conclusion
This paper presents novel method for learning RL policies that generalize, in a zero-shot manner, to arbitrary LTL specifications by performing subgoal decomposition through the corresponding Büchi automata and completing one subgoal at time. Empirical results demonstrate that our method, despite being myopic, achieves substantially better generalization to complex and unseen specifications compared to existing baselines. We posit that the real complexity of LTL task generalization does not lie the structure of the LTL formula or the corresponding automata, but rather in the combinatorial nature of the atomic propositions associated with the MDP states. The observation reduction technique that we introduce is step towards addressing this complexity. Future work will explore alternative techniques that can exploit the Boolean structure within subgoal, such as Boolean task algebra [37, with the goal of further improving the sample efficiency and generalization ability of our method.
Acknowledgement
The authors thank the anony mous reviewers for their invaluable feedback and constructive suggestions. This work was supported in part by the U.S. National Science Foundation under grant CCF-2340776.
10

---

References
[1] J. Achiam, D. Held, A. Tamar, and P. Abbeel. Constrained policy optimization. In International conference machine learning, pages 22-31. PMLR, 2017.
[2] C. Allen, N. Parikh, O. Gottesman, and G. Konidaris. Learning markov state abstractions for deep reinforcement learning. Advances in Neural Information Processing Systems, 34:8229- 8241, 2021.
[3] M. Bagatella, A. Krause, and G. Martius. Directed Exploration in Reinforcement Learning from Linear Temporal Logic. Seventeenth European Workshop on Reinforcement Learning. Oct. 2024.
[4] H. Bharadhwaj. A. Kumar, N. Rhinchart, S. Levine, F. Shkurti, and A. Garg. Conservative safety critics for exploration. arXiv preprint arXiv:2010. 14497, 2020.
[5] R. Büchi. Symposium decision problems: On decision method in restricted second order arithmetic. In Studies in Logic and the Foundations of Mathematics, volume 44, pages 1-11. Elsevier, 1966.
[6] Y. Cheng, P. Zhao, and N. Hovakimyan. Safe and efficient reinforcement learning using settubbance-obseeve--baass control barrier functions. In Learning for Dynamics and Control Conference, pages 104-115. PMLR, 2023.
[7] M. Cho and C. Sun. Constrained meta-reinforcemeee learning for adaptable safety guarantee with differentiable convex programming. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 38, pages 20975-20983, 2024.
[8] S. Cui and P. Mitra. Automated multi-tast learning for joint disease prediction on electronic health records. In The Thirty--ighth Annual Conference on Neural Information Processing Systems, 2024.
[9] G. Dalal, K. Dvijotham, M. Vecerik, T. Hester, C. Paduraru, and Y. Tassa. Safe exploration in continuous action spaces. arXiv preprint arXiv: 1801 2018.
[10] J. F. Fisac, N. F. Lugovoy, V. Rubies-Royo, S. Ghosh, and C. Tomlin. Bridging hamilton- jacobi safety analysis and reinforcement learning. In 2019 International Conference on Roboties and Automation (ICRA), pages 8550-8556. IEEE, 2019.
[11] J. Fu and U. Topcu. Probably Approximately Correct MDP Learning and Control With Temporal Logic Constraints. In Robotics: Science and Systems X, July 2014.
[12] M. Ganai, S. Gao, and S. Herbert. Hamilton-jacohi reachability in reinforcement learning: A survey. IEEE Open Journal of Control Systems, 2024.
[13] M. Ganai, Z. Gong, C. Yu, S. Herbert, and S. Gao. Iterative reachability estimation for safe reinforcement learning. Advances Neural Information Processing Systems, 36:69764-69997, 2023.
[14] B. Gangopadhyay, P. Dasgupta, and S. Dey. Safe and stable rl driving policies using control barrier and control lyapunov functions. IEEE Transactions on Intelligent Vehicles, 8(2):1889-189,, 2022.
[15] Gu, I.. Yang, Y. Du, G. Chen, F. Walter, J. Wang, and A. Knoll. A review of safe reinforcement learning: Methods, theory and applications. arXiv preprint 2rXiv:2205.10330 2022.
[16] Z. Guo, W. Zhou, and W. Li. Temporal logic specification-condtionn decision transformer for offline safe reinforcement learning. In Forty-first International Conference Machine Learning. 2024.
[17] Z. Guo, W. Zhou, S. Wang, and W. Li. Constraint-conddtioned actor-critic for offline safe rein- forcement learning. In The Thirteenth International Conference on Learning Representations, 2025.
11

---

[18] E. M. Hahn, M. Perez. S. Schewe, F. Somenzi, A. Trivedi, and D. Wojtczak. Mungojerrie: Linear-Tine Objectives in Model-Free Reinforcement Learning. In Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, pages 527-545, 2023.
[19] P. Hansen-Estruce A. Zhang, A. Nair, P. Yin, and S. Levine. Bisimulation makes analogies in goal-conditioned reinforcement learning. In International Conference on Machine Learning, pages 8407-8426. PMIR, 2022.
[20] M. Hasanbeig, A. Abate, and D. Kroening. Logically-constraaneed reinforcement learning. arXiv preprint arXiv: 1801,0809, 2018.
[21] A. Hendawy. J. Peters, and C. D'Eramo. Multi-task reinforcement learning with mixture of orthogonal experts. In The Twelfth International Conference on Learning Representations, 2024.
[22] S. Huang, Q. Gallouédec, F. Felten, A. Raffin, R. J.J. Dossa, Y. Zhao, R. Sullivan, V. Makoviy- chuk, D. Makoviichuk, M. H. Danesh, C. Roumégous, J. Weng. C. Chen, M. M. Rahman, J. G. M. Araújo, G. Quan, D. Tan, T. Klein, R. Charakorn, M. Towers, Y. Berthelot, K. Mehta, D. Chakraborty, A. KG, V. Charraut, C. Ye, Z. Liu, L. N. Alegre, A. Nikulin, X. Hu, T. Liu,
J. Choi, and B. Yi. Open RL Benchmark: Comprehensive Tracked Experiments for Reinforce- ment Learning. arXiv preprint arXiv:2402.03046. 2024.
[23] M. Jackermeier and A. Abate. Deepltl: Learning to efficiently satisfy complex Itl specifications for multi-task rl. In The Thirteenth International Conference on Learning Representations. 2025.
[24] A. K. Jayant and S. Bhatnagar. Model-based safe deep reinforcement learning via constrained proximal policy optimization algorithm. Advances in Neural Information Processing Systems, 35:24432-244 -2445, 2022.
[25] Ji, B. Zhang, J. Zhou, X. Pan, W. Huang, R. Sun, Y. Geng. Y. Zhong, Dai, and Y. Yang. Safety gymnasium: A unified safe reinforcement learning benchmark. In Thirty-sevnnth Conference on Neural Information Processing Systems Datasets and Benchmarks Track, 2023.
[26] K. Jothimurugan, R. Alur, and O. Bastani. A composable specification language for reinforce- ment learning tasks. Advances in Neural Information Processing Systems, 32, 2019.
[27] D. Kim, K. Lee, and S. Oh. Trust region- based safe distributional reinforcement learning for multiple constraints. Advances in neural information processing systems, 36:1 19998-19999, 2023.
[28] K. Kim, G. Swamy, 2. Liu, D. Zhao, S. Choudhury, and S. Z. Wu. Learning shared safety constraints from multi-task demonstrations. Advances in Neural Information Processing Systems, 36:5808-5826, 2023.
[29] B. G. León, M. Shanahan, and F. Belardinelli. Systematic generalisation through task temporal logic and deep reinforcement learning. arXiv preprint arXiv:2006.08767, 2020.
[30] B. G. León, M. Shanahan, and F. Belardinelli. Systematic Generalisation through Task Temporal Logic and Deep Reinforcement Learning. In arXiv. arXiv, 2021.
[31] B. G. León, M. Shanahan, and Belardinelli. a Nutshell, the Human Asked for This: Latent Goals for Following Temporal Specifications. In International Conference on Learning Representations, 2022.
[32] X. Li, C.-I. Vasile, and C. Belta. Reinforcement learning with temporal logic rewards. In 2017 IEEF/RSJ International Conference on Intelligent Robots and Systems (IROS), pages 3834-3839. IEEF, 2017.
[33] Q. Lin, B. Tang, Z. Wu, C. Yu, S. Mao, Q. Xie, X. Wang, and D. Wang. Safe offline rein- forcement learning with real-time budget constraints. In International Conference on Machine Learning, pages 21127-21152. PMLR, 2023.
12

---

[34] 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), pages 2535-2541, 2024.
[35] M. Liu, M. Zhu, and W. Zhang. Goal-conditioned reinforcement learning: Problems and solutions. arXiv preprint arXiv:2201.08299 2022.
[36] Ma, X. Liu, and Huang. Unsupervised reinforcement learning for multi-task autonomous driving: Expanding skills and cultivating curiosity. IEEE Transactions Intelligent Trans- portation Systems, 2024.
[37] G. Nangue Tasse. S. James, and B. Rosman. A boolean task algebra for reinforcement learning. Advances in Neural Information Processing Systems, 33:9497-9507, 2020.
[38] J. Oh, S. Singh, H. Lee, and P. Kohli. Zero-shot task generalization with multi-task deep reinforcement learning. In International Conference on Machine Learning, pages 2661-2670. PMLR, 2017.
[39] A. Pnueli. The temporal logic of programs. In 18th annual symposium on foundations of computer science (sfcs 1977), pages 46-57, ieee, 1977.
[40] W. Qiu, W. Mao, and H. Zhu. Instructing goal-conditioned reinforcement learning agents with temporal logic objectives. Advances in Neural Information Processing Systems, 36:39147- 39175, 2023.
[41] A. Rafiei, R. Moore, S. Jahromi, F. Hajati, and R. Kamaleswaran. Meta-leaming in healtheare: A survey. SN Computer Science, 5(6):791, 2024.
[42] Schulman, Moritz, Levine, M. Jordan, and Abbeel. High-dimensional continuous control using generalized advantage estimation. arXiv preprint
2015.
[43] Schulman, Wolski, Dhariwal, A. Radford, and O. Klimov. Proximal policy optimization algorithms. arXiv preprint arXiv: 1707:00777.0347 2017.
[44] A. Shah, C. Voloshin, C. Yang, A. Verma, S. Chaudhuri, and A. Seshia. Deep policy optimization with temporal logic constraints. arXiv e-prints, pages arXiv-2404, 2024.
[45] A. Shah, C. Voloshin, C. Yang, A. Verma, S. Chaudhuri, and S. A. Seshia. LTL-Constrained Policy Optimization with Cycle Experience Replay. In arXiv, 2024.
[46] D. Shao and M. Kwiatkowska. Sample efficient model-free reinforcement learning from LTL specifications with optimality guarantees. In Proceedings of the Vecooy-Second International Joint Conference on Artificial Intelligence, pages 4180-4189, 2023.
[47] O. So and C. Fan. Solving Stabilize-Avoid Optimal Control via Epigraph Form and Deep Reinforcement Learning. In Proceedings of Robotics: Science and Systems, July 2023.
[48] A. A. Taiga, R. Agarwal, Farebrother, A. Courville, and M. G. Bellemare. Investigating multi- task pretraining and generalization in reinforcement learning. In The Eleventh International Conference Leurning Representations, 2023.
[49] Z. Tang, X. Chen, Y. Li, and J. Chen. Efficient and generalized end-to-end autonomous driving system with latent deep reinforcement learning and demonstrations. arXiv preprint arXiv:2401.11792, 2024.
[50] Vaezipoor, A. C. Li, R. Icarte, and S. A. Mcilraith. Ltl2action: Generalizing Itl instructions for multi-task rl. In International Conference on Machine Learning, pages 10497- 10508. PMIR, 2021.
[51] C. Voloshin, A. Verma, and Y. Yue. Eventual discounting temporal logic counterfactual experience replay. International Conference on Machine Learning, pages 35137-351.0.. PMLR, 2023,
13

---

[52] A. Wachi, Y. Sui, Y. Yue, and M. Ono. Safe exploration and optimization of constrained mdps using gaussian processes, In Proceedings of the AAAI Conference on Artificial Intelligence. volume 32, 2018.
[53] N. Xiong, Y. Du, and L. Huang. Provably safe reinforcement learning with step-wise violation constraints. Advances in Neural Information Processing Systems, 36:54341-544 2023.
[54] B. Yalcinkaya, N. Lauffer, M. Vazquez-Chanlatte, and S. Seshia. Compositional automata embeddings for coal-conditioned reinforcement learning. Advances in Neural Information Processing Systems, 37:72933-72963, 2024.
[55] B. Yalcinkaya, N. Lauffer, M. Vazquez-Chanlatee and S. A. Seshia. Provably correct au- tomata embeddings for optimal autommta--onnittioee reinforcement learning. arXiv preprint arXiv:2503.05042, 2025.
[56] T.Y. Yang. J. Rosca, K. Narasimhan, and P. J. Ramadge. Projection-based constrained policy optimization. In International Conference on Learning Representations, 2020.
[57] D. Yu, H. Ma, S. Li, and J. Chen. Reachability constrained reinforcement learning. In International conference machine learning, pages 25636-25655. PMLR, 2022.
[58) H. Zang, X. Li, L. Zhang, Y. Liu, B. Sun, R. Islam, R. Tachet des Combes, and R. Laroche. Understanding and addressing the pitfalls of bisimulation-based representations in offiine reinforcement learning. Advances Neural Information Processing Systems, 36:28311-222 1-24440, 2023.
[59] Y. Zhang, Q. Vuong, and K. Ross. First order constrained optimization in policy space. Advances Neural Information Processing Systems, 14115338-153444 2020.
[60] W. Zhao, T. He, and C. Liu. Probabilistic safeguard for reinforcement learning using safety index guided gaussian process models. In Learning for Dynamics and Control Conference, pages 783-796. PMLR, 2023.
[61] Y. Zheng, Li, D. Yu, Y. Yang, S. E. Li, X. Zhan, and Liu, Safe offline reinforcement learning with sessibillity-uuide diffusion model. In The Twelfth International Conference on Learning Representations, 2024.
14

---

Broader Impacts
Our work aims to improve the generalization reinforeement learning to satisfy arbitrary LTL specifications. This framework enables flexible and expressive task definitions, but it also places responsibility on the user to ensure that the specifications are well designed. The behavior of the agent is tightly coupled with the given specification, poorly constructed or harmful specifications may lead to unsafe or unintended behaviors. Thus, careful design and verification of specifications essential when applying such methods real-world settings.
A Experimental Settings
A.1 Environments
We use the LetterWorld [50] and ZoneEnv [50 233 for evaluation. The LetterWorld grid world that contains 12 letters corresponding to atomic propositions AP = {a. b.....Iff Each letter appears twice and randomly placed on the grid. The observation consists of the entire grid in egocentric view. The agent move in four directions: up, down, left, and right. The grid wraps around, i.e., the agent moves out of bounds, it reappears on the opposite side. The maximum episode length is T = 75. The ZoneEnv contains different colored regions corresponding to atomic propositions AP = fblue, green, magenta, yellow] and walls acting as boundaries. Our implementation is adapted from (23). We the point robot that has continuous action space for acceleration and steering. Observations consist of Lidar measurements of the colored regions and ego- centric state information from other sensors. The maximum episode length is T 1000. We further construct several variants of the ZoneEnv to evaluate the generalization performance of our method and baselines by modifying: (1) the region size, with {0.2, 0.3, 0.4 (ef(uullll 0.5, 0.6}: (2) the number of regions per atomic proposition, with count {1. 2(default), 3, 4, 5); (3) and the number of atomic propositions, expanded to include new symbols {red, cyan, orange, purple, teal, lime). Illustrations of the environments are provided in Figure and trajectories under different LTL
specifications are provided in Figure
15 and [6
We exclude the FlatWorld 23 45 environment from our evaluation. It contains colored regions similar to ZoneEnv. However, the region layout is fixed, meaning that certain Boolean formulas over the atomic propositions cannot be evaluated since they are never true in this environment. Additionally, the observation space is limited to the agent's (I, pposition.. Due to this lack of variability and expressiveness, we exclude FlatWorld from our evaluation.
Figure Visualisations of environments, Left: LetterWorld, Right: ZoneEnv
A.2 LTL Specifications
We evaluate zero-shot generalization across a range of specifications, including complex and nested finite-horizon tasks (Table complex infnite-horizon tasks (Table varying specification complex- ity with different sequence lengths of reach-only and reach-avoid specifications (Table varying environment complexity in reach-avoid tasks (Table and different numbers of atopic propositions (Table 5). The specifications i - 4p and 4o - P12 are from 23). better evaluate each method's generalization ability and its handling of the trade-off between task progression and safety constraints, we construct more complex specifications, P5-$$ and PP33-P16. which feature longer temporal sequences and stricter safety requirements, i.c., more atomic propositions appear under negation.
15

---

Table 4: Reach-only and reach-avoid specifications. Evaluation results are shown in Figure 4
[yelime AF (Mon AF (grwe. Fmagenta)))
ggrees (magenta (Miee-Fyelow)
us W fydlow (magenca A Fageee))
Igreen RF (Bue NF (magems RF (yllow (M Figme)))1
[ysllow Uapeen (magenta X (velow Faremn)))))
us A (magrnts AF [g (yelow X. (Miw Fmogetal)))
Rasdooly
1brue yellow [grees/ (magreta AFF (Mee [grees (yellow maggttal))))))
2-3
igreen (Mie FF (jellow A (magrsts (gren/ (blee A (magenta A (1100))01))
Imageria AF (yclow AF Egroon F ( (nagenta A.F ( (groen A FFyeoo00000)
(ysllow
(
F. (grssn (ydllo A /Nue (grssn Fvdllo))331111
10
M.ue F (groce (ycllow AF (magentaa A A F (scllow (groen (magenta A.F [Drue A AFyllow))311)
Flysllow A (Blue A. Imagenta AF (gnsen F (yellow AF (blue (maganta (grsen A [buu A Fmagenal033) (yelow (green AT (magenta Immaganta X (Blu A "green (vellow AF (magenta o. (blue (yellow (green A.F (maganca A (blu A Igreen A F1el0001000000
(yelose Imageers (grenn
tgreen X.F (yello magents))))) (0000))
1-12
[yelloee// (magenta AF ( (grwen (yelow AF (biue (magutts AF (gwea. (Nie A (jellow [mageeta g100)))00
[-Blae grwnn yelow
an2
(-yellow A -magenta) U gren
(-greon
blu
-(Blue v yelow)
is (- v magenta) yellow))
x:4
-Egresn yollow)
(magenaa (-Iblus V ycllow) U (roan))
-fyelow magenta)
magenta) yellow))
Readh saadh-nood
-1alae yellow) U
(aroon / (- y magenta) U (ydlow A (-rapoon V (buss U magental)))
3+5
"yellow v blue)
(magenta (gwen V/ yellow) U (blae (ggreen magerna) U yellww11)
-igreen yellow
(magonta (-igrese (lue) (yelow [-Ible mageria) gees)))))
(green 7 NMm) U
(magenta A (yelow Noe) U [gres A ("(bee pellown D. (magrets A (-lyylos Vhive gree)))0)))
and
-Igreen yellow] (magenta (-(grese (buue) (yelow (-igreon
U (-tnagett
green2)11)
"magonta Mue)
(yslow (-farnn magerta) (Blae (nimaagnnttttaa Vproos) U (yollow (-fgresn Mue) 0 magemta)11))
(magenta v Mie)
(yren A (pelow Non) U (magents (
(yelow grenn D (Bla (-maageetaa grees) U (ye yeloon S. (Sla magamna g1
10 -farsn Mue)
(magenta (-Caron
(yellww (-<Mue magenta]
(n vylloo) (blu [-Imagenca greee)) vellowstii))
(yelow blue)
(gren ( maggents) (yelow A ( (magenta Mow] U (gres A (xlyelow V Hiuee U (magents A (olggs Vyllloo) b10)))00)
Table 5: Reach-avoid specifications with more APs. Evaluation results are shown in Table 6
- (blue V yellow) U (green A (-(blue magenta) U (yellow A (~igreen (blue) U magenta)))) ))))
IAPI
(yellow v blue) U (magenta A ( ([green v yellow) U (blue A ( (green V maggetta) U yellow))))
-(green V yellow)
U (magenta A (-[green blue) (yellow A (-(blue V mmggetaa)
green))))
-(red V cyan)
(blue A (-Cellow green) (magenta A [cyan V yellow) U groen]])
IAPI=
-[green red)
(cyan A (-(blue magenta) V (yellow Ccyan redd U blue))))
(yelloww eyan) U (red (-(green V blue) U (magenta
(red V/ yellow) U green))))
ZoneEnv
-(orange V red)
(eyan A (-(blue green) U (yellow A (- purple V blue) U magenta]]]]
IAPI= 8
(purple v cyan) U (orange A ("ee V yellow) U (green A (-magennta V red) U blue))
"yyellow V purple) U (green A (m(cyan orange) U (blue A (-mmagenta V green) U orange))))
(teal V magenta) 0 (orange A (-<lime V blue) U (yellow A -grron purple) V red))))
-(cyan V parple)
(magenta (-(red V teal) (lime (-(orange V yellow) green]]))
-(blue green)
(yellow (-(seal v llime)
(purple A ( (magenta v red) U orange))))
B Implementation Details
We use the official codebases of the baselines: LTL2Action] GCRL-LTIP RAD RAD-embeddingg and D Our implementation is adapted from DeepLTL by incorporating a safety value function and state-dependent Lagrangian multiplier and removing Tp-pe.ff modules. For DeepLTTL, LTI LTT.2Action, and our method, we use fully connected actor network with three hidden layers of sizes [64, 64, 64). The value function network has two hidden layers of sizes [64, 64). For our method, both the safety value function and the Lagrangian multiplier network share the same architecture as the value function. GCRL-LTL employs larger actor-critic architecture with [512, 1024, 256] units due to its use of a graph neural network. For fair comparison, we use the Adam optimizer with learning rate of 3e - 4 and train all methods for 15M environment interactions. The discount factor is set to y = 0.94 for LetterWorld and 7 0.998 for ZoneEnv. Additional hyperparameter details are provided in the code in the supplementary materials. We train all the methods using a 16-core AMD CPU and an NVIDIA GeForce RTX 4090 GPU, and it takes roughly 3 hours to train model.
Our method is summarized in Algorithm We begin by constructing a subgoal set that includes all feasible subgoals: we first enumerate each assignment E 24P as candidate a+. For each such at we filter out the remaining assignments that conflict with it. We then enumerate all possible
16

---

combinations of the filtered assignments to form A resulting in the full set of feasible reach-
subgoals {(at A } from which subgoals are sampled uniformly. The agent receives a reward r- = 1 if the subgoal is satisfied and r = 0 otherwise. At each timestep, it receives a safety signal h = -1 if the subgoal not violated, and h = 1 otherwise. The reward and safety functions are defined
a+) and h = 2 1 (T((s) E A-] 1, respectively. If the current subgoal is satisfied, we sample a new subgoal whose avoid set does not contain the current state, i.c. L(s)) & AA, and whose reach set also excludes the current state, i... L(xs) & at, to prevent the new subgoal from being immediately violated or trivially satisfied. a subgoal is violated, the episode terminates. We use Generalized Advantage Estimation (GAE)
= 1 (7)(s")
42
estimate value functions:
A7 = E0= (TAGA)) 5r,+t A --=----
o,,5= = r: 7V - V(sg)
(5) where AGAE = 0.95 is the discount factor of GAE. At test time, given a target LTL specification, we convert it into Büchi automaton and apply the DFS to enumerate all possible paths to accepting states. For each path, we evaluate the current subgoal using the learned value functions and select the optimal subgoal to execute. This process is applied iteratively until an accepting state is reached.
Ei=0 (3GGA) (n 5n,1 = (1 - 7)h + max(h,, (s
Algorithm 1 GenZ-LTL
Require: Initial policy π, value and safety value function Vy, Vh, state-dependent Lagrangian multiplier A, subgoal set ç. maximum training iterations K, interactions per iteration N
1: for k = 1........... K do for 0, 1.2........ do
2:
if the current subgoal is not specified or the current subgoal is satisfied/violated then Sample subgoal a Unif(E) 5: end if
3:
4:
6:
Collect trajectory (69 0t, rt,, he] end for
7:
Compute reward-to-go R. = ET I'T; and cost-to-go H, = max, hy for each t
8:
9:
Compute advantage functions A,, A7, based on V,, and V₂2 using (4) and (5).
Compute the Lagrangian multiplier
11:
Fit value function, safety value function by regression
square error.
12:
Update the policy parameters by maximizing (
13:
Update the multiplier parameters by minimizing
14:
end for
B.1 Subgoal-induced observation reduction.
For Lidar measurements in the ZoneEnv, f(-) is implemented as the element-wise min to obtain the closest distance along each Lidar beam, such that the resulting s" For grid maps in LetterWorld, we assign distinct values to each cell associated with a at location (i.j): f(s.)) = Ureach if L(s,,) at: Uavoid if ((s,g) E A Uneuiral otherwise. This reduction allows the agent to focus on "reach" and "avoid" rather than specific set of atomic propositions and eliminates the need of encoding subgoals, enabling efficient policy learning and generalization to new atomic propositions that satisfies the conditioned discussed in Section 4.2 as shown later in Appendix C If multiple observation functions are available, each capable of observing
assignment a E 2 we can first fuse the observations within each observation type based on the current subgoal a and then concatenate the results to form the final state 8". In cases where each atomic proposition is tied to a distinct observation type, our method can be applied: however, learning policies in such settings is inherently intractable due to the exponential number of subgoal-state combinations.
The actual implementation of the observation reduction may appear straightforward, as the fusion However, the idea behind this technique is broadly applicable. When solving the reach-avoid problem, what truly matters is whether a state satisfies the reach or avoid condition under the current subgoal, rather than its specific label L(s) as we mentioned in Section 4.2 Moreover, our method can be extended to more realistic settings with some additional effort, but without requiring fundamental changes to the core approach. For example, in autonomous driving scenarios with multiple sensors such as cameras and LiDAR,, observation reduction can be enabled through perception modules. Semantic segmentation can be applied to both image and point
operator is enviroomenttsensoosppeecci
17

---

cloud data to extract relevant features based on the current reach-avoid subgoals. For instance, if the avoid subgoal involves avoiding other cars and pedestrians, and the reach subgoal involves staying within the current lane, then perception can be used to segment the scene accordingly. This allows the agent focus on task-relevant information and use processed observations, rather than raw sensory data, to learn value functions and policies effectively.
Algorithm Timeout-barn based subgoal-switching mechanism
Require: Trained agent, Büchi automaton B = (Q, [Q, go). timeout value tmax
1: Q. f {
Current set of states.
2: 4 < 0
D Set of unsatisfiable transitions.
3: while (indSubgoallsB,,, Qc,11 do
4: Select subgoal o (at, from FindSubgoals(B,, 2c.4) with maximum value.
5: for t 1, 2,.... max do
6:
Get an action from the agent, apply it, and observe E E 2 2.
7:
Remember the old states. > Update the current set of states.
8:
Q. - {a' 3g Qo. (q, E
9:
if Qc + Q then
10:
break
> A new state set is reached; the subgoal should be updated.
11:
else if mmx then
12:
u - u ((,
( -F)
Di If q is not accepting, mark this subgoal as unsatisfiable.
13:
end if end for end while
14:
15:
16:
All subgoals are marked as unsatisfiable. Terminate.
B.2 Timeout & Subgoal-switching Mechanism
At the test time, given target LTL specification, convert it into Büchi automaton and apply depth-first search (DFS) to enumerate all possible paths to accepting states. However, not all of these paths, or in some cases, any, feasible in the physical environment, as some may include subgoals that are unsatisfiable. Although the labeling function is known, meaning we can determine which propositions are true for any given state, it does not necessarily imply that we can exhaustively iterate over the entire state space to identify unsatisfiable assignments.
For example, consider the specification -yellow U ((blue A green) V magenta). To satisfy this formula, the agent must eventually reach either a magenta region or a region where blue and green overlap. However, the latter becomes unsatisfiable if the blue and green regions are disjoint. In such cases, the agent must be able to adapt by pursuing an alternative subgoal, a capability that is essential for goal-conditioned policies, including our approach well existing baselines such as DeepLTL and GCRL-LTL. However, these baselines do not address this issue.
To address this, we implement timeout mechanism that allows the agent to revisit the automaton and search for alternative subgoals when the current one cannot be satisfied. We determine subgoal satisfiability by enforcing timcout threshold (1 + Escale) Msubgoa as discussed in Section 4.1 if the agent fails to achieve this subgoal within that timestep, is considered unsatisfiable, and the agent switches its subgoal. If no feasible subgoals remain, the episode terminates.
This timeout subgoal-switchin mechanism is explained in Algorithm 2 which outlines the general mode of operation during the test time. We use set L4 Q x E to store the transitions that are marked as unsatisfiable after timeout. These unsatisfiable transitions are ignored by the FindSubgoals function. Apart from this, the only difference between FindSubgoals and the DFS algorithm used in DeepL.TI. is that we separate the subgoals after identifying the paths with accepting cycles.
C Additional Experiments
Training curves. We first evaluate simple reach-only and reach-avoid specifications with sequence length of n every specific training interval, and the success and violation rates are shown in Figure We can observe that method outperforms the baselines in terms of achieving lower
18

---

violation rate (close to zero constraint violation) while maintaining a high success rate. The violation rates of the baselines also decrease over training because task progression and safety constraints are jointly encoded in the I.TI. specification, so optimizing for satisfaction of the specification implicitly improves safety performance. However, due to the inherent trade-off hetween these requirements, the baselines struggle to further reduce violation rates. In contrast, by formulating the problem using safe RL framework with reachability constraints, our method achieves stricter constraint satisfaction, thereby improving the overall probability of satisfying the full LTL specifications.
DoopLTL
GORL-LTL
LTLZAction
Genz-LTL(ours)
LetterWarld
ZoneEnv
75
62
12
23
24
Tra Training Steps
Figure 9: Evaluation curves on simple reach-only and reach-avoid specifications with n = 3. Each value is averaged over 5 seeds with 50 trajectories with randomly sampled tasks.
Partial observability. To satisfy arbitrary LTL specifications, we leverage the structure of the Büchi automaton to decompose each formula into a sequence of subgoals and handle one subgoal at a time, progressing through the sequence incrementally. While our method could be extended to condition on the full subgoal sequence, we argue that this introduces significant drawbacks that outweigh the potential benefits. Among the baselines, DeepLTL conditions its policy the full subgoal sequence to achieve non-myopic behavior. Intuitively, this "look-ahead" capability may help the agent satisfy the specification in fewer steps. However, subgoal sequences come with several disadvantages. First, policies trained on full sequences are more likely to encounter OOD issues at test time, as the sequence length can vary across specifications. Although one might limit the policy to observe most k subgoals, where kt is the maximum length seen during training, choosing & is nontrivial. A large & can lead exponential sample complexity due the combinatorial explosion of subgoal sequences, c.g., each subgoal is drawn from 2-1/5 while a small k limits the look-ahead benefit. Moreover, practice, the agent may not perceive all relevant subgoals once, rendering the subgoal sequence ineffective. To illustrate this, we conduct experiments where the agent's is observability is restricted half of the environment. We train both DeepLTL and our method in LetterWorld and ZoneEnv, and then evaluate them using specifications 11-P3 and reach-avois tasks with = 4. We report the average success rate 7/s and violation rate Yh. As shown in the left and middle plots of Figure TO our mingle-ubgooal-tt--a-a and violation rates, despite the latter using full subgoal sequences.
method outperforms DeepLTL in terms of both the success
fl
Fve
Partial observability (LetterVorid))
Partial observability (ZoneEnv)
Overlapoing
DocpLTL DespLTL
Ours
Ours (partiel)
DeepLTL DecpLTL
Ours
Ours (partial)
DecpLTL
OuTs
(pertial)
(pertial)
Figure 10: Evaluation results DeepLTL and our method in two settings: (1) partial observability (left two plots) and (2) overlapping areas (the rightmost plot).
Overlapping areas. We construct a variant of ZoneEnv to introduce a more challenging setting where multiple atomic propositions can be true simultancously, i.e., different colored regions may overlap in arbitrary configurations. Note that FlatWorld is an overly simplified case where the layout fixed. In ZoneEnv, overlapping areas can be handled in two ways: (1) by adding separate observations for each assignment involving multiple true propositions, or (2) by using observations only for individual atomic propositions (default setting for ZoneEnv) and learning policies through interaction with the environment, during which the agent implicitly discovers the relationships among propositions and observations. The first approach does not offer meaningful advantages over the second, as observation reduction technique can extract the relevant parts of the observation
19

---

for any target assignment and fuse them as needed. Thus, we adopt the second approach, which presents a more challenging generalization problem. To accommodate this scenario, we modify DeepI.TI.ss curriculum training to allow multiple atomic propositions to be true at the same time. The positions of both the agent and the regions are randomly sampled. We evaluate both methods 2: Φ2 -(magenta V yellow) U (blue A green), &3 -(blue magenta) (yellow A green), 04 (yylloo V blue) (green magenta), and Φs (green V magenta) V (yellow A blue). Trajectory illustrations the average rates and the results the rightmost plot in Figure TO show that our method achieves higher success rate and lower violation rate. Our method can better satisfy safety constraints due to the integration of reachability constraints.
using reach-avoid specifications with
shown in Figure [1] We report
Figure 11: Illustration of trajectories in ZoneEnv: (1) unsatisfiable subgoals (left two columns, Φ1) and (2) overlapping areas (right four columns, 0s). The top row shows trajectories generated by our method, while the bottom row shows those from DeepLTL.
Number of atomic propositions. We also evaluate performance the number of atomic propositions increases. In this experiment, we emphasize that the observations corresponding to the additional atomic propositions satisfy the conditions outlined in Section 4.2 It important note that when new atomic propositions are observed through modalities not encountered during training - such as those representing the agent's 's speed or heading - zero-shot adaptation remains an open challenge. The results are presented in Table and example trajectories are shown in Figure 12 Among the evaluated methods, only our method can generalize in a zero-shot manner new atomic propositions whose observations are produced by identical observation functions under output transformation, as the subgoal-induced observation reduction technique fuses these propositions into "reach" and "avoid", allowing the agent to make decisions without relying on their specific labels L(s).
Table 6: Performance in ZoneEnv with increasing number of atomic propositions. We evaluate the reach-avoid specifications with sequence length of n = 6, using an increasing number of atomic propositions as listed in Table 5 We report success rate 7/s, violation 7/., other rate 7oo and average steps to satisfy the specifications J..
Metrics
IAPI=
IAPI 6
IAP
IAPI= 10
No
0.96
0.94
0.93
0.02
0.02ao.01
0.03go.01
0.02
No
0.02
0.04go.02
0.
0.05
306.58 10.88
16..8
314.88_
313.10g10.a1
323.30
[AP]
[AP]
|API -
Figure Illustration of ZoneEnv with increasing number of atomic propositions. The trajectories shown correspond to the first specification for |AP| 4, 6, 8, 10 in Table
20

---

Deterministic v.s, stochastic policies. As discussed in Section we follow the standard practice of using a deterministic policy during evaluation. We also note that DeepLTL is evaluated using a stochastic policy in LetterWorld in its original paper. To provide a comprehensive comparison, we report results for both stochastic and deterministic policies LetterWorld, as shown in Figure [3] We observe that DeepL.TI. exhibits inconsistent behavior: while the success rate improves under stochastic policy, the violation rate also increases. This trade-off is unacceptable in safety-critical applications and indicates that DeepLTL struggles to maintain safety. In contrast, our method delivers consistent performance without compromising safety for task progression, since we explicitly model the violation of subgoals stochastic policies are not suitable for evaluation. For reach-only specifications, they contain no safety constraints; stochastic policy may satisfy them simply by randomly exploring the environment, thereby overstating performance. For reach-avoid specifications, stochasticity further introduces inconsistency: the mean action may be safe, while sampled action may lead to a violation, or vice versa. This randommess complicates evaluation and prevents a fair comparison between methods.
reachability constant in a safe RL formulation. In our view,
f7s
nl
stocheotic
<:
4:9s deterinnti
0:95-
0.5-
Rate
26
0.90
0.0
DeepLTL
Ours
DeepLTL
Ours
DeepLTL
Ours
DeepLTL Ours
Figure 13: Evaluation results of DeepLTL and our method in LetterWorld using stochastic and deterministic policies. Each value is averaged over 5 seeds, with 100 trajectories per seed.
Table 7: Performance in ZoneEnv with Ant agent. We report the success rate 17s, violation rate Te. and the average steps satisfy the specifications μ. Each value is averaged over 5 seeds, with 100 trajectories per seed.
GenZ-1.TL(ours))
Deepl.TI
Tj
7/4
0.97
0.02
305.32
0.00
0.23
865. 50.500mm.ss
(P10
0.00
202
202.00_53.33
0.03
0.30
588.58 2 as
Pa1
0.95
0.04guo2
182 88..88
0.07
0.27
604.87
ZoneEzzv
(P12
0.98 1o.m
0.96
0.00
0.04=nos
204.04-m7..
125.97 .35.00
0.24
0.00
0.05100:
0.23
568
302
164.0
15
0.30
0.00=000
459 119.90-.s..o
0.00
0.00=0000
P16
0.95
0.00=am
434.41
0.00
0.00
0.80
0.08-002
429.76..7.1
0.00
0.39
Figure 14:
Visualization of the Ant agent in ZoneEnv.
0.90
0.00=000
449 =9.200
0.00
0.00
P1
0.90
0.022004
448.51
0.00
0.10.o.1 18
Complex Dynamies. To evaluate the performance of our method in environments with more complex dynamics, we conduct additional experiments using the Ant agent (25), consisting of a torso and four legs connected by hinge joints, in the Zone environment. The state space includes the agent's ego-state (40 dimensions, compared to 12 for the Point agent used in our main experiments) and LiDAR observations of the regions. A visualization of the Ant agent is shown in Figure 14 The action space has 8 dimensions, corresponding to the torques applied to the Ant's joints to coordinate leg movements (compared to 2 dimensions for the Point agent). We train and evaluate our method against DeepLTL, the strongest baseline in our main results. For a fair comparison, all training procedures, training parameters, and neural network sizes were kept the same (note that the last one in particular could result in some performance drop as the state dimension and action dimension are bigger for the ant agent). Both methods are trained until convergence. The evaluation results are shown in Table 7 metrics, demonstrating an even larger performance gain in environments with more complex agent dynamics. Note that for the Ant agent, in addition to the LTL specifications, there is a built-in safety constraint that the agent should not fall headfirst, enforced as a hard constraint with immediate episode termination. Although negative reward is assigned in such cases, is done when specification is
We can observe that our method consistently outperforms the baseline across all
21

---

violated for DeepLTL, it does not explicitly model safety constraints as our method does through HJ reachability, making it less effective handling such cases. This impedes the learning coordinated locomotion and then the satisfaction of I.TL. specifications, leading to degraded performance.
Illustration of infinite-horizon tasks in ZoneEnv. The trajectories correspond to specifica- tions 1/1- shown from left to right (two columns per specification). The top row shows trajectories generated by our method, while the bottom row shows those from DeepLTL.
Figure 15:
Zone size 0.2
Zone size 0.3
Zone size 0.4
Zone size = 0.5
Zone size 0.6
Zone count
Zone count 2
Zone count
Zone count =
Zone count
Illustration of ZoneEnv under increasing environment complexity, including different zone sizes and different numbers of zones per atomic proposition. The default zone size is 0.4, and the default number zones per atomic proposition The trajectories are generated by our method and correspond to the evaluated specification (-blue A -green) U yellow.
Figure 16:
D Visualizations
We provide visualizations for the experiments in Section 5.1 and Section 5.2 including infinite- horizon tasks (Figure increasing environment complexity (Figure [6) and increasing numbers of atomic propositions (Figure 12p. For infinite-horizon tasks, our method exhibits clear recurring pattern that visits the specified regions in the correct order, while the baseline struggles to do so and suffers from safety constraint violations. For different environment complexities, we vary the zone size and zone count per atomic proposition. Importantly, we increase the zone count only for propositions the agent must avoid, since doing for propositions the agent need to satisfy would simplify the task. Larger zones or more zones proposition force the agent to navigate around constrained regions reach the target, and the resulting trajectories demonstrate that our method satisfies the safety constraints. For experiments with an increasing number of atomic propositions, new colored
we incrementally introduce new propositions, up to 10 in total, each corresponding region with associated lidar observations. This makes zero-shot generalization challenging for baseline methods, as they explicitly encode atomic propositions and cannot generalize to unseen ones without retraining. Even substituting one proposition for another, for example, replacing blue with red, causes these baselines to fail, due to their dependence on fixed encodings. In contrast, our method uses subgoal-induced induced observation reduction, which removes this dependency when atomic
22

---

propositions share the same property. This allows our method to focus on the semantics of the propositions, i.e., "reach" or "avoid", rather than the specific proposition symbols, enabling zero-shot generalization to unseen atomic propositions.
23

---

NeurIPS Paper Checklist
1. Claims
Question: Do the main claims made in the abstract and introduction accurately reflect the paper's contributions and scope?
Answer: [Yes]
Justification: The abstract and introduction clearly state the paper's goals, methods, and contributions, which are consistently supported and developed throughout the paper.
Guidelines:
The answer NA means that the abstract and introduction do not include the claims made the paper.
The abstract and/or introduction should clearly state the claims made, including the contributions made in the paper and important assumptions and limitations. A No or
NA answer to this question will not be perceived well by the reviewers.
The claims made should match theoretical and experimental results, and reflect how much the results can be expected to generalize to other settings.
is fine to include aspirational goals as motivation as long as is clear that these goals not attained by the paper.
2. Limitations
Question: Does the paper discuss the limitations the work performed by the authors?
Answer: [Yes]
Justification:
We include the limitations in the conclusion section and the Appendix.
Guidelines:
The answer NA means that the paper has no limitation while the answer No means that the paper has limitations, but those are not discussed in the paper.
The authors are encouraged to create a separate "Limitations" section their paper.
The paper should point out any strong assumptions and how robust the results are to violations of these assumptions (e.g., independence assumptions, noiseless settings, model well-specification, asymptotic approximations only holding locally). The authors should reflect how these assumptions might be violated in practice and what the implications would be.
The authors should reflect on the scope of the claims made, e.g., if the approach was only tested on few datasets or with few runs. In general, empirical results often depend on implicit assumptions, which should be articulated.
The authors should reflect on the factors that influence the performance of the approach. For example, facial recognition algorithm may perform poorly when image resolution is low images are taken in low lighting. Or speech-to-text system might not be used reliably to provide closed captions for online lectures because it fails to handle technical jargon.
The authors should discuss the computational efficiency of the proposed algorithms and how they scale with dataset size.
If applicable, the authors should discuss possible limitations of their approach to address problems of privacy and fairness.
While the authors might fear that complete honesty about limitations might used by reviewers as grounds for rejection, worse outcome might be that reviewers discover limitations that aren't 't acknowledged judgment and recognize that individual actions in favor of transparency play impor- tant role in developing norms that preserve the integrity of the community. Reviewers will be specifically instructed to not penalize honesty concerning limitations.
the paper. The authors should use their best
3. Theory assumptions and proofs
Question: For each theoretical result, does the paper provide the full set of assumptions and complete (and correct) proof?
Answer: [NA]

---

While the paper does not include theoretical results, it clearly states the necessary assumptions underlying the proposed method.
Justification:
Guidelines:
The answer NA means that the paper does not include theoretical results.
All the theorems, formulas, and proofs in the paper should be numbered and cross- referenced.
All assumptions should be clearly stated or referenced in the statement of any theorems.
The proofs can either appear in the main paper or the supplemental material, but if they appear in the supplemental material, the authors are encouraged to provide a short proof sketch provide intuition.
Inversely, any informal proof provided in the core of the paper should be complemented by formal proofs provided in appendix or supplemental material.
Theorems and Lemmas that the proof relies upon should be properly referenced.
4. Experimental result reproducibility
Question: Does the paper fully disclose all the information needed to reproduce the main ex- perimental results of the paper to the extent that affects the main claims and/or conclusions of the paper (regardless of whether the code and data are provided or not)?
Answer: [Yes]
Justification: The paper provides sufficient details about the experimental setup, including environment configurations, evaluation metrics, and baselines, support reproducibility of the main results.
Guidelines:
The answer NA means that the paper does not include experiments. If the paper includes experiments, a No answer this question will not perceived well by the reviewers: Making the paper reproducible is important, regardless of whether the code and data are provided or not.
the contribution is a dataset and/or model, the authors should describe the steps taken to make their results reproducible or verifiable.
Depending on the contribution, reproducibility can be accomplished in various ways. For example, if the contribution is a novel architecture, describing the architecture fully might suffice, or if the contribution a specific model and empirical evaluation, may be necessary to either make it possible for others to replicate the model with the same dataset, or provide access to the model. In general. releasing code and data often one good way to accomplish this, but reproducibility can also be provided via detailed instructions for how to replicate the results, access to a hosted model (e.g., in the case of large language model), releasing of a model checkpoint, or other means that are appropriate to the research performed.
While NeurIPS does not require releasing code, the conference does require submis- sions to provide some reasonable avenue for reproducibility, which may depend on the nature of the contribution. For example
(a) If the contribution is primarily a new algorithm, the paper should make it clear how reproduce that algorithm.
(b) If the contribution is primarily
model architecture, the paper should describe the architecture clearly and fully.
(c) the contribution is a new model (e.g., a large language model), then there should either be way access this model for reproducing the results way to reproduce the model (e.g., with an open-source dataset or instructions for how to construct the dataset).
(d) We recognize that reprodueibility may be tricky in some cases, in which authors are welcome to describe the particular way they provide for reproducibility. In the case of closed-source models, it may be that access to the model is limited in some way (e.g., to registered users), but it should be possible for other researchers have some path reproducing verifying the results.
5. Open access to data and code
25

---

Does the paper provide open access to the data and code, with sufficient instruc- tions faithfully reproduce the main experimental results, as described in supplemental material?
Question:
Answer: [Yes]
Justification: The code is provided in the supplementary materials, along with instructions sufficient to reproduce the main experimental results.
Guidelines:
The answer NA means that paper does not include experiments requiring code.
Please see the NeurIPS code and data submission guidelines (https://nips... cc/
for more details.
While encourage the release of code and data, we understand that this might not be possible, so "No" is an acceptable answer. Papers cannot be rejected simply for not including code, unless this is central to the contribution (e.g., for new open-source benchmark).
The instructions should contain the exact command and environment needed to rum to reproduce the results. See the NeurIPS code and data submission guidelines (https
//ips.cc/ppblicc wwtppbblcggggiiieecceeeeeoooeeee http//uidess/eee/
for more details.
The authors should provide instructions on data access and preparation, including how to access the raw data, preprocessed data, intermediate data, and generated data, etc.
The authors should provide scripts to reproduce all experimental results for the new proposed method and baselines. only subset of experiments are reproducible, they should state which ones are omitted from the script and why.
At submission time, to preserve anonymity, the authors should release anonymized versions (if applicable).
Providing much information possible in supplemental material (appended to the paper) is recommended, but including URLs to data and code permitted.
6. Experimental setting/details
Does the paper specify all the training and test details (c.g., data splits, hyper- parameters, how they were chosen, type of optimizer, etc.) necessary to understand the results?
Question:
Answer: [Yes]
The paper specifies key details of the experimental setup, including environ- ment settings, training and evaluation protocols, hyperparameters, and optimizer configura- tions in the Appendix.
Justification:
Guidelines:
The answer NA means that the paper does not include experiments.
The experimental setting should be presented in the core of the paper to a level of detail that is necessary appreciate the results and make sense of them.
The full details can be provided either with the code, appendix, or as supplemental material.
7. Experiment statistical significance
Question: Does the paper report error bars suitably and correctly defined or other appropriate information about the statistical significance of the experiments?
Answer: [Yes]
Justification: The paper reports the mean and variance of evaluation metrics across multiple runs to support the statistical reliability of the results.
Guidelines:
The answer NA means that the paper does not include experiments.
The authors should answer "Yes" if the results are accompanied by emor bars, confi- dence intervals, or statistical significance tests, least for the experiments that support the main claims of the paper.
26

---

The factors of variability that the error bars are capturing should be clearly stated (for example, train/test split, initialization, random drawing of some parameter, or overall run with given experimental conditions).
The method for calculating the error bars should be explained (closed form formula, call to a library function, bootstrap, etc.)
The assumptions made should be given (e.g., Normally distributed errors).
It should be clear whether the error bar is the standard deviation the standard error of the mean.
is OK to report 1-sigma error bars, but one should state it. The authors should preferably report a 2-sigma error bar than state that they have 96% CI, if the hypothesis of Normality of errors is not verified.
For asymmetric distributions, the authors should be careful not to show in tables or figures symmetric error bars that would yield results that are out range (e.g. negative error rates).
If error bars reported in tables or plots, The authors should explain in the text how they were calculated and reference the corresponding figures or tables in the text.
8. Experiments compute resources
For each experiment, does the paper provide sufficient information on the com- puter resources (type of compute workers, memory, time of execution) needed to reproduce the experiments?
Question:
Answer: [Yes]
Justification: The paper provides details on compute resources, including hardware specifi- cations and runtime, in the Appendix.
Guidelines:
The answer NA means that the paper does include experiments.
The paper should indicate the type of compute workers CPU or GPU, internal cluster, cloud provider, including relevant memory and storage.
The paper should provide the amount of compute required for each of the individual experimental rums as well as estimate the total compute.
The paper should disclose whether the full research project required more compute than the experiments reported in the paper (e.g., preliminary or failed experiments that didn't fidn't make it into the paper).
9. Code of ethics
Question: Does the research conducted in the paper conform, in every respect, with the NeurIPS Code of Ethics
Answer: [Yes]
Justification: We have reviewed the NeurlPS Code of Ethics and confirm that the research complies with guidelines.
Guidelines:
The answer NA means that the authors have reviewed the NeurIPS Code of Ethics.
the authors answer No, they should explain the special circumstances that require deviation from the Code of Ethics.
The authors should make to preserve anonymity (e.g., if there is special consid- eration due to laws or regulations their jurisdiction).
10. Broader impacts
Question: Does the paper discuss both potential positive societal impacts and negative societal impacts of the work performed?
Answer: [Yes]
Justification: The paper discusses potential positive and negative socictal impacts of the proposed work in section provided before the appendix.
Guidelines:
27

---

The answer NA means that there is no societal impact of the work performed.
If the authors answer NA or No. they should explain why their work has no societal impact or why the paper does not address societal impact.
Examples of negative societal impacts include potential malicious unintended uses (e.g., disinformation, generating fake profiles, surveillance), fairness considerations (e.g., deployment of technologies that could make decisions that unfairly impact specific groups), privacy considerations, and security considerations.
The conference expects that many papers will be foundational research and not tied to particular applications, let alone deployments. However, if there is direct path to any negative applications, the authors should point it out, For example, it is legitimate to point that improvement in the quality of generative models could be used to generate deepfakes for disinformation. On the other hand, it is not needed to point out that a generic algorithm for optimizing neural networks could enable people train models that generate Deepfakes faster.
The authors should consider possible harms that could arise when the technology is being used as intended and functioning correctly, harms that could arise when the technology is being used intended but gives incorrect results, and harms following from (intentional or unintentional) misuse of the technology.
If there are negative societal impacts, the authors could also discuss possible mitigation strategies (e.g., gated release of models, providing defenses in addition attacks, mechanisms for monitoring misuse, mechanisms to monitor how system learns from feedback over time, improving the efficiency and accessibility of ML).
11. Safeguards
Does the paper deseribe safeguards that have been put in place for responsible release of data or models that have a high risk for misuse (e.g., pretrained language models, image generators, scraped datasets)?
Question:
Answer: [Yes]
Justification: Our work does not involve the release of high-risk data models. However, we note that the potential risks stem from how users specify LTL tasks, and we emphasize in the broader impacts that careful specification design is essential to avoid unintended or unsafe behaviors.
Guidelines:
The answer NA means that the paper poses no such risks.
Released models that have a high risk for misuse or dual-use should be released with necessary safeguards to allow for controlled use of the model, for example requiring that users adhere to usage guidelines or restrictions to access the model or implementing safety filters.
Datasets that have been scraped from the Internet could pose safety risks. The authors should describe how they avoided releasing unsafe images.
We recognize that providing effective safeguards is challenging, and many papers do not require this, but we encourage authors to take this into account and make best faith effort.
12. Licenses for existing assets
Question: Are the creators or original owners of assets (e.g., code, data, models), used in the paper, properly credited and are the license and terms of use explicitly mentioned and properly respected?
Answer: [Yes]
Justification: All external assets used in this work, including code and environments, are properly cited in the paper. We respect the terms of use and licenses associated with these assets, and license information is provided where applicable.
Guidelines:
The answer NA means that the paper does not use existing assets.
The authors should cite the original paper that produced the code package dataset.
28

---

The authors should state which version of the asset is used and, if possible, include URL.
The name of the license (e.g.. CC-BY 4.0) should be included for each asset.
For scraped data from a particular source (e.g., website), the copyright and terms of service of that source should be provided.
If assets are released, the license, copyright information, and terms of use in the package should be provided. For popular datasets, pwwpsssipppsseeeee thcode com com/datasets has curated licenses for some datasets. Their licensing guide can help determine the license of dataset.
For existing datasets that are re-packaged, both the original license and the license of the derived asset (if it has changed) should be provided.
If this information not available online, the authors are encouraged to reach out to the asset's s creators.
13. New assets
Question: Are new assets introduced in the paper well documented and is the documentation provided alongside the assets?
Answer: [Yes]
We release new code assets as part of this work. The code is accompanied by documentation that describes usage, dependencies, training details, and environment integration.
Justification:
Guidelines:
The answer NA means that the paper does not release new assets.
Researchers should communicate the details of the dataset/code/moddl as part of their submissions via structured templates. This includes details about training, license, limitations, etc.
The paper should discuss whether and how consent obtained from people whose asset used.
At submission time, remember to anonymize your assets (if applicable). You can either create an anonymized URL or include an anonymized zip file.
Crowdsourcing and research with human subjects
Question: For crowdsourcing experiments and research with human subjects, does the paper include the full text of instructions given to participants and screenshots, if applicable, as well as details about compensation (if any)?
Answer: [NA]
Justification:
This work does not involve crowdsourcing or research with human subjects.
Guidelines:
The answer NA means that the paper does not involve crowdsourcing nor research with human subjects.
Including this information tion of the paper involves human subjects, then as much detail as possible should be included the main paper.
supplemental material is fine, but if the main contribu-
According to the NeurlPS Code of Ethics, workers involved in data collection, curation, or other labor should be paid at least the minimum wage in the country of the data collector.
15. Institutional review board (IRB) approvals or equivalent for research with human subjects
Question: Does the paper describe potential risks incurred by study participants, whether such risks were disclosed to the subjects, and whether Institutional Review Board (IRB) approvals (or an equivalent approval/review based on the requirements of your country or institution) were obtained?
Answer: [NA]
29

---

Justification:
This work does not involve research with human subjects and therefore does not require IRB approval or equivalent review.
Guidelines:
The answer NA means that the paper does not involve crowdsourcing nor research with
human subjects.
Depending on the country in which research is conducted, IRB approval (or equivalent) may be required for any human subjects research. If you obtained IRB approval, you should clearly state this in the paper.
We recognize that the procedures for this may vary significantly between institutions and locations, and we expect authors to adhere the NeurlPS Code of Ethics and the guidelines for their institution.
For initial submissions, do not include any information that would break anonymity (if applicable), such as the institution conducting the review.
Declaration LLM usage
Does the paper describe the usage of LLMs if it is an important, original, or non-standard component of the core methods in this research? Note that if the LLM is used only for writing, editing, formatting purposes and does not impact the core methodology, scientific rigorousness, or originality of the research, declaration is not required.
Question:
Answer: [NA]
Justification: LLMs were only used for writing and editing purposes and did not contribute to the core methodology scientific content of the research.
Guidelines:
The answer NA means that the core method development in this research does not involve LLMs as any important, original, non-standard components.
Please refer to our LLM policy (btppe//berrrpsccc/ooooerreeee// for what should or should not be described.
30


Reviews:
[{"review_id": "qmITUxXluX", "reviewer": "Reviewer_tAEC", "summary": "This paper introduces GenZ-LTL, a reinforcement learning (RL) method that achieves zero-shot generalization to unseen tasks defined by Linear Temporal Logic (LTL) specifications. The core approach is to decompose LTL goals into reach-avoid subgoals through Büchi automata and subgoal-induced observation reduction, and solve them sequentially using a safe RL framework guided by Hamilton-Jacobi (HJ) reachability constraints. The subgoal-induced observation reduction technique also mitigate exponential scaling with atomic propositions. To cope with this issue when a selected subgoal is unsatisfiable in the environment, there is a timeout-based subgoal-switching mechanism to identify unsatisfiable subgoals and allow the agent to switch to alternative ones. Empirical results across several environments demonstrate generalization, safety, and sample efficiency compared to the baselines.", "questions": "1. Is there any comparison that highlights the performance of GenZ-LTL versus the baselines on satisfiable LTL specifications that may admit sub-optimal solutions?\n2. How well does GenZ-LTL perform in scenarios that closely resemble real-world environment?\n3. See above in Weaknesses", "limitations": "yes", "rating": 5, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 3, "significance": 3, "originality": 3, "strengths_and_weaknesses": "Strengths:\n1. First method to combine state-wise safety constraints, HJ reachability, with goal-conditional RL on LTL tasks.\n2. The reach-avoid formulation and observation reduction technique enhance the generalization while keep the training efficiency.\n3. Comprehensive evaluations across finite and infinite-horizon tasks, with strong baselines (DeepLTL, LTL2Action, GCRL-LTL)\n4. The method and experiments are described clearly, with good figures and examples.\n\nWeaknesses:\n1. The method handles only one subgoal at a time, which could be suboptimal in tasks requiring global planning. The authors acknowledge this in their discussion, but it's still a core limitation.\n2. The Assumptions for observation reduction(e.g., decomposability of observations, monotonic sensor fusion) might not generalize to all real-world settings.\n3. It would be beneficial to include additional experimental results on benchmarks that closely resemble real-world scenarios and robot agents, such as robotic arms or quadrupeds in simulated environments in MuJoCo [1].\n\n[1] MuJoCo benchmark: https://github.com/google-deepmind/mujoco", "was_revised": true, "final_justification": "Most of my questions are resolved.", "rebuttal": "We thank the reviewer for their thoughtful comments and constructive feedback. We address each weakness and question below.\n\n## Weaknesses\n> 1. The method handles only one subgoal at a time, which could be suboptimal in tasks requiring global planning. The authors acknowledge this in their discussion, but it's still a core limitation.\n\nConsidering only one subgoal at a time indeed can be suboptimal. However, achieving globally optimal behavior across reach-avoid subgoal sequences requires full observability of the environment and all the subgoal states, a condition that is often unmet in practice. In addition, our goal is to zero-shot generalize to *arbitrary* LTL specifications, where their subgoal sequences may have very long length, making global planning intractable. \n\nThus, in this paper, we argue that it is actually better to consider one subgoal at a time in general. This approach has the advantage of avoiding out-of-distribution (OOD) generalization issues that arise when learning from subgoal sequences -- a limitation observed in the DeepLTL baseline (see Section 5.1 and 5.2, and Appendix C where DeepLTL's performance drops significantly under partial observability). In addition, conditioning a goal-conditioned policy on individual subgoals rather than subgoal sequences or automaton embeddings reduces the input dimensionality, thus improving sample efficiency. Lastly, it enables training a goal-conditioned policy where the avoid subgoal can be dealt with as a hard constraint.\n\nWe also provide additional evaluation results of RAD-embeddings [54], which can be viewed as having knowledge of the global plan as it learns policies conditioned on embeddings of the automata. As shown in our response to Reviewer VrZq (Weakness 1), our approach substantially outperforms RAD-embeddings in terms of both specification satisfaction rate and performance. \n\n> 2. The Assumptions for observation reduction (e.g., decomposability of observations, monotonic sensor fusion) might not generalize to all real-world settings.\n\nWe acknowledge that the assumptions underlying observation reduction may not generalize to all real-world settings. However, we would like to emphasize that the core idea behind this technique is broadly applicable. When solving the reach-avoid problem, what truly matters is whether a state satisfies the reach or avoid condition under the current subgoal, rather than its specific label $L(s)$ as we mentioned in Section 4.2. Moreover, our method can be extended to more realistic settings with some additional effort, but without requiring fundamental changes to the core approach. For example, in autonomous driving scenarios with multiple sensors such as cameras and LiDAR, observation reduction can be enabled through perception modules. Semantic segmentation can be applied to both image and point cloud data to extract relevant features based on the current reach-avoid subgoals. For instance, if the avoid subgoal involves avoiding other cars and pedestrians, and the reach subgoal involves staying within the current lane, then perception can be used to segment the scene accordingly. This allows the agent to focus on task-relevant information and use processed observations, rather than raw sensory data, to learn value functions and policies effectively.\n\n> 3. It would be beneficial to include additional experimental results on benchmarks that closely resemble real-world scenarios and robot agents, such as robotic arms or quadrupeds in simulated environments in MuJoCo.\n\nWe agree with the reviewer that additional experiments on robotic benchmarks could further strengthen the paper. We would like to point out that the notion of generalization spans multiple dimensions, such as unseen task specifications, novel environments, and varying robot platforms. This work focuses specifically on generalization to unseen task specifications. The environments used in our work are widely adopted in prior studies, such as [23, 39, 50], and were chosen to ensure fair and meaningful comparisons. While MuJoCo-based environments are valuable for studying complex dynamics, they are less suited for evaluating generalization to temporally extended or logic-based tasks. Nonetheless, we agree that broader benchmark coverage is important, and we would be enthusiastic to evaluate our method on future benchmarks that reflect the challenges of LTL task generalization.\n\n## Questions\n> 1. Is there any comparison that highlights the performance of GenZ-LTL versus the baselines on satisfiable LTL specifications that may admit sub-optimal solutions?\n\nAs shown in Table 1, for some specifications such as $\\varphi_4$ and $\\varphi_{9-12}$, the average number of steps $\\mu$ among successful trajectories is higher for our method (i.e. suboptimal) than for DeepLTL (a method that considers subgoal sequences). However, our method achieves a higher success rate $\\eta_s$ and a lower violation rate $\\eta_v$ across these specifications. As discussed in lines 279–284, $\\mu$ is a secondary metric as step count is less important when the agent struggles to satisfy the specifications. Also, our method achieves lesser number of steps (i.e. better performance) in all the other specifications in the paper. \n\n> 2. How well does GenZ-LTL perform in scenarios that closely resemble real-world environment?\n\nZoneEnv is representative of real-world navigation environments where tasks involve spatial, temporal, and logical constraints, thus suitable for evaluating LTL task generalization. It also features a high-dimensional state space (e.g., LiDAR observations) and realistic robot dynamics (e.g., differential-drive robots), providing a challenging testbed. As noted in our response to Weakness 1, we would be enthusiastic to evaluate our method in future benchmarks that reflect the challenges of LTL task generalization. For further discussion on how our method applies to broader applications, please see our responses to Weaknesses 2 and 3."}, {"review_id": "Wxesn0t8dZ", "reviewer": "Reviewer_NmCA", "summary": "This paper proposes GenZ-LTL, a reinforcement learning (RL) framework that enables zero-shot generalization to arbitrary Linear Temporal Logic (LTL) specifications. In its proposed method, the LTL task is first decomposed into a sequence of reach-avoid subgoals using the corresponding Büchi automaton. Instead of conditioning on full subgoal sequences, GenZ-LTL processes subgoals one at a time to better generalize to unseen tasks. Besides, the method treats avoid conditions as hard constraints and incorporates Hamilton-Jacobi reachability to enforce safety.", "questions": "Please address the novelty concerns I raised in Weakness section.\t\n\nIn the last paragraph of section 3, it says “q and q' are consecutive states along some accepting run, and q≠q' if q'∉ F”. Why q≠q' if q'∉ F? When the agent is going back and forth between two different accepting states, this statement is not correct.\n\n\tAuthors use reach-avoid subgoals throughout the paper. Is this same as sub-task? If it is about reach-avoid, “sub-task” should be used, not subgoal.\n\n\tI don’t quite understand the observation reduction part. It says the original size of proposition-dependent part is k×2^(|AP|). The lidar observation has an independent component for every proposition. So, is the original size k×|AP|?\n\n\tWhat do you mean by this sentence “For simplicity of deriving a fusion operator that preserves task-relevant semantics such as distances to avoid zones, we assume that the os are coordinate-wise monotonic” in section 4.2?\n\tIn section 5.3, authors evaluate the effects of the observation reduction and safe RL approach. However, training a separate Q and V function for safety constraints can cost a lot of environmental samples. Could you evaluate the increase of environmental samples used to train Q and V functions for safety constraints?", "limitations": "Authors need to include sufficient discussion about the scalability of the proposed method.", "rating": 2, "confidence": 5, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 1, "clarity": 1, "significance": 2, "originality": 1, "strengths_and_weaknesses": "Strengths: This paper proposes to solve the generalization of temporal logic tasks, which is an important topic in many applications.\n\nWeakness:\n1. The major concern of this paper is its novelty. The main idea of this paper, i.e., solving or generalizing LTL tasks by decomposing LTL tasks into reach-avoid sub-tasks, has been proposed and investigated by many previous works [1,2,3,4]. Especially in [2,4], generalizing temporal logic tasks by training goal-conditioned RL policies to solving arbitrary reach-avoid sub-tasks has been proposed. \n\nAuthors say that safety constraints were not modeled in [4]. However, both target and safety constraints of sub-tasks/subgoals are clearly modeled in [2]. The method proposed in [2] also trains a general value function for arbitrary reach-avoid sub-tasks composed of propositions, but authors claim this as their innovation. \n\nIn [3], authors even derive the probability lower-bound for solving reach-avoid sub-tasks. Although [3] didn’t mention generalization, RAMS in [3] can be trivially applied into the generalization of LTL tasks. \n\nIn addition, the subgoal-induced observation reduction just trivially extracts components about propositions to reach and to avoid from LIDAR observations, since every proposition already has an independent component in the LIDAR observation. \n\n2. The writing of this paper needs to be improved a lot. \n\nThe introduction part does not present some key concepts clearly, e.g., subgoal-induced observation reduction, which makes it difficult for people to understand the author's contribution. \n\nIn the method section, a concise algorithm table should be provided, summarizing key steps of the proposed framework. Authors only introduce the algorithm in text and diagram, but these are not enough. Besides, there are a lot of redundant sentences in the method section, making people confused when reading this part. In section 4.2, a diagram should be provided to describe the process of observation reduction.\n\n3. Authors propose to use the constrained policy optimization [5] to solve the reach-avoid sub-task. However, there are many other safe RL approaches to achieve the same goal. Authors did not clearly explain why they chose the method in [5] and not use others. RASM in [3] is another method with probabilistic guarantee. Authors could compare their method with RASM for solving any reach-avoid sub-tasks.\n\n[1] Wang, Yuning, and He Zhu. \"Deductive Synthesis of Reinforcement Learning Agents for Infinite Horizon Tasks.\" 37th International Conference on Computer Aided Verification (CAV), 2025.\n\n[2] Xu, Duo, and Faramarz Fekri. \"Generalization of Compositional Tasks with Logical Specification via Implicit Planning.\" arXiv preprint arXiv:2410.09686 (2024).\n\n[3] Žikelić, Đorđe, et al. \"Compositional policy learning in stochastic control systems with formal guarantees.\" Advances in Neural Information Processing Systems 36 (2023): 47849-47873.\n\n[4] Qiu, Wenjie, Wensen Mao, and He Zhu. \"Instructing goal-conditioned reinforcement learning agents with temporal logic objectives.\" Advances in Neural Information Processing Systems 36 (2023): 39147-39175.\n\n[5] Yu, Dongjie, et al. \"Reachability constrained reinforcement learning.\" International conference on machine learning. PMLR, 2022.", "was_revised": true, "final_justification": "As I explained to authors during exchange of messages in rebuttal , and through my private message to the area chair, I do not see sufficient contribution to merit for publication. I stand my initial rating.", "rebuttal": "We appreciate the feedback from the reviewer. Below, we detail our responses to each of the weaknesses, questions, and limitations.\n\n### Weaknesses\n>1.1. The major concern of this paper is its novelty, with additional points raised in comparison to prior work [1, 2, 3, 4].\n\nOur paper does not claim decomposing an LTL specification into reach-avoid subgoal sequences as a contribution. As discussed in lines 58–65, existing literature can be categorized into subgoal decomposition and direct specification encoding methods. Our work follows the subgoal decomposition paradigm, but as emphasized in lines 65–67 and 151–153, our contribution lies in how the reach-avoid subgoals are solved, which differs significantly from prior works.\n\nThe main novelty and contributions of our paper, as stated in the introduction, are (1) showing that solving one subgoal at a time is in general better than conditioning on subgoal sequences, as done in the state-of-the-art method [DeepLTL]; (2) the first safe RL formulation with state-wise constraints for LTL satisfaction; and (3) subgoal-induced observation reduction for mitigating the exponential complexity of subgoal-state combinations.\n\nRegarding the treatment of safety constraints in prior works, we are very careful in our choice of language when describing them in our paper. In line 267, we state that \"[4] does not model safety constraints explicitly within its RL formulation.\" [4] uses an ad hoc threshold over the value function to identify safe actions, which is not a principled mechanism for enforcing constraint satisfaction. [DeepLTL] uses a similar threshold-based technique, which is ineffective in achieving safety, as we discussed in lines 74-77 and Sections 5.1 and 5.2. \n\n[DeepLTL] Jackermeier and Abate. \"DeepLTL: Learning to Efficiently Satisfy Complex LTL Specifications for Multi-Task RL,\" ICLR 2025 (oral).\n\nRegarding [2], although it takes as input the encoding of state, the reach and avoid subgoals (i.e., $p_{+}$ and $p_{-}$ in [2]), and a GNN-based embedding of the remaining sub-tasks, it still learns a single value function. As discussed earlier, using a single value function without explicit constraint modeling is insufficient for ensuring safety. In contrast, our approach is novel in how we solve the reach-avoid problem as we formulate the reach-avoid subgoals as constrained optimization problems and incorporate Hamilton-Jacobi (HJ) reachability for modeling safe actions explicitly (see Section 4.3). Such formulation contributes to the substantially lower violation rates observed in our results (see Section 5, especially the ablation study in Section 5.3). Besides, our version of HJ reachability also extends [5] to the LTL specification generalization setting, while [5] only considers a fixed task and safety constraint.\n\nWe also respectfully disagree with the reviewer that [3] can be trivially applied to our setting. The probability lower bounds of [3] hinges on the following conditions:\n- Known Lipschitz constant of the system's dynamics. \n- Known reach (target) and avoid (unsafe) sets.\n- Full state space access and discretization.\n- An in-the-loop verifier, which, at each iteration, needs to perform interval bound propagation on neural networks and enumerate the discretized states.\n\nThese assumptions and requirements are incompatible with our setting, where we can have partial observability, unknown dynamics and reach/avoid sets, and a high-dimensional and continuous state space that makes discretization intractable. Furthermore, [3] essentially uses PPO to learn the control policy and thus lacks a principled mechanism for enforcing hard safety constraints (similar to [2, 4, DeepLTL] that all learn a single value function). \n\n>1.2. \"In addition, the subgoal-induced observation reduction just trivially extracts components ...\"\n\nThe actual implementation of the observation reduction may appear straightforward, as the fusion operator is environment/sensor-specific (see lines 190–193). However, the idea behind this technique is to circumvent the exponential complexity of state-subgoal combinations, a problem that has not received much attention in existing literature. As the number of atomic proposition grows, learning a goal-conditioned policy quickly becomes intractable. While various dimensionality reduction techniques have been proposed in the RL literature, they usually do not consider the state-subgoal combination (see lines 157-169). Our observation reduction provides a step toward more efficient policy learning to address this challenge. In the Conclusion section, we state that \"We posit that the real complexity of LTL task generalization does not lie in the structure of the LTL formula or the corresponding automata, but rather in the combinatorial nature of the atomic propositions associated with the MDP states.\" We hope our work can inform and inspire future work in this direction.\n\n>2.1. “The introduction part does not present some key concepts clearly …”\n\nWe thank the reviewer for pointing this out. We will add the following sentence in the introduction to convey the high-level idea of subgoal-induced observation reduction:\n\"The idea of subgoal-induced observation reduction is to exploit symmetry in the state observations and extract information only relevant to the current subgoals.\"\n\n>2.2. “In the method section, a concise algorithm table should be provided, summarizing key steps of the proposed framework …”\n\nDue to the page limit, the formal algorithm and observation reduction details are placed in Appendix B/B.1. If space permits in a future version, we will move them to the main text.\n\n>3. Why did the authors choose [5] for safe RL, and why was RASM or other alternatives not considered for comparison?\n\nAs stated in Section 4.3, \"A key difference between our approach and existing subgoal-based approaches lies in the treatment of the avoid subgoal. We treat an avoid subgoal as a hard constraint, since whenever a violation occurs, satisfying the LTL formula becomes impossible...To enforce these hard constraints, we leverage the notion of HJ reachability as introduced in Section 3 and formulate our RL objective as follows.\" In Section 3 (lines 86-96), we introduce state-wise safety constraints and its connection to HJ reachability in the context of RL. Regarding [3], as we explain in our response to Weaknesses 1.1, RASM is not suitable for our setting due to its underlying assumptions and requirements.\n\n### Questions\n>1. Why $q \\neq q'$ if $q'\\notin F$? When the agent is going back and forth between two different accepting states, this statement is not correct.\n\nWe specify the condition $q \\neq q'$ if $q' \\notin F$ to filter out self-loops on non-accepting states in an accepting run. The case mentioned by the reviewer does not conflict with this condition. Our experiments on infinite-horizon tasks also include such case where the agent transitions back and forth between multiple accepting states (specifications listed in Table 4), and our method is able to satisfy those specifications effectively.\n\n>2. Terminology of reach-avoid subgoals or sub-tasks.\n\nWe would like to clarify that we use the term reach-avoid subgoal consistently throughout the paper. While sub-task may also be appropriate, we chose subgoal to reflect the goal-conditioned nature of our policy and to maintain consistent terminology. In the literature, the two terms are used interchangeably; for example, [23, 50] use sub-task, and [39] uses subgoal to describe the same concept.\n\n>3. Size of the proposition-dependent part, $k \\times 2^{|AP|}$or $k \\times |AP|$?\n\nIn general, the original size of the proposition-dependent part is $k\\times 2^{|AP|}$ since the finite alphabet is $2^{AP}$ as noted in line 111. For instance, consider $AP$ = {blue, green}. The lidar observation may include two separate channels for the blue and green regions. However, these channels cannot cover the proposition blue $\\land$ green (overlapping blue and green region).\n\n>4. What do you mean by this sentence “For simplicity of deriving a fusion operator ... we assume that the os are coordinate-wise monotonic” in section 4.2?\n\nThe sentence refers to the difficulty of defining a general fusion operator that preserves meaningful task semantics (e.g., distance to avoid states) for arbitrary observation functions, which may be nonlinear and non-monotonic. Thus, for simplicity, we assume the observation functions are coordinate-wise monotonic. It is also possible to derive the fusion operator if we know what the observation functions are. \n\n>5. Training a separate Q and V function for safety constraints can cost a lot of environmental samples. Could you evaluate the increase of environmental samples used to train Q and V functions for safety constraints?\n\nDuring training, our method uses the same number of interactions (15M, as stated in Section 5) as all baselines. Each interaction yields a transition of the form $(s^\\sigma_t, a_t, r_t, h_t)$, where $r_t$ and $h_t$ are used to learn the reward value function $V_r$ and the reachability value function $V_h$, respectively. Therefore, our method does not require additional environment samples.\n\n### Limitations\n>1. Authors need to include sufficient discussion about the scalability of the proposed method.\n\nWe would like to emphasize that we focus primarily on the zero-shot generalization of LTL specifications, which directly relates to scalability with respect to specification complexity. Our method scales linearly with the length of the subgoal sequences by completing the subgoals one at a time. In addition, our observation reduction technique improves scalability with respect to state/observation dimensions by extracting observations only relevant to the current subgoal.\n\nWe hope that our responses sufficiently address the reviewer’s questions and concerns and kindly ask the reviewer to consider raising their score."}, {"review_id": "Zto98nfk6o", "reviewer": "Reviewer_VrZq", "summary": "The paper introduces a multi-task RL framework for tasks given as LTL specifications, combining goal-conditioned RL and safe RL. Specifically, for a given LTL task, they perform a DFS search to identify accepting cycles on the induced Buchi automaton and extract reach and avoid subgoals; then, if applicable, apply their proposed subgoal-induced observation reduction method to reduce the state size; and finally, they sequentially (and myopically) pass individual reach-avoid problems to a goal conditioned policy. They incorporate Hamilton-Jacobi reachability to their goal-conditioned policy by simultaneously learning a value function estimating the feasible set and using this value function with a state-dependent Lagrangian multiplier to select the subgoal that achieves the best trade-off between the task progression and the safety constraint. To account for the fact that some subgoals might be unsatisfiable, they implement a subgoal switching mechanism that is triggered if the current subgoal is not reached within a timeout threshold; if the current subgoal times out, then they switch to the next best subgoal, selected based on the value functions. During these attempts, they make sure that the current reach-avoid problem does not violate another reach-avoid problem by respecting all avoid subgoals of the current automaton state. An experimental evaluation of the method is presented, comparing the proposed framework against a selected set of previous work and showing its efficacy.", "questions": "1. Have you tried comparing against [54]? I think this empirical comparison is needed, as [54] is a newer technique that outperforms [50]. Also, do you agree with my comment that LTL formula embeddings [50] and automata embeddings [54] can be incorporated into your technique to overcome the myopia issue? If so, I think the paper can benefit from a discussion highlighting how these different approaches are orthogonal and can be incorporated to get the best of both worlds, i.e., overcome myopia via embeddings and the benefits of your safe RL formulation.\n2. In Figure 6, what were the network sizes and number of training steps for \"Ours (w/o s^\\sigma)\" and \"Ours\"? Were they the same? If so, then do you think that given more compute, \"Ours (w/o s^\\sigma)\" could perform as well as \"Ours\"?\n3. Does the benefit of the state reduction technique stem from the compression it provides through exploiting the symmetries in the observation? Is it possible to get the same performance with more compute when this state reduction technique is not used? I think a discussion or an experiment on this matter might be helpful to further highlight what this state reduction technique provides. Especially given the fact that it is an environment-specific approach that cannot be used in any environment, it would be good to have a further discussion of how to make the overall method work as well in cases where this state reduction technique cannot be used.", "limitations": "yes", "rating": 5, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 3, "significance": 3, "originality": 3, "strengths_and_weaknesses": "The paper combines the existing approaches for multi-task RL with LTL objectives and Hamilton-Jacobi-based safe RL in an intuitive and clear manner. Their extensive experimental evaluation demonstrates the benefits of their proposed approach compared to the previous work. Their subgoal-induced observation reduction technique is a novel contribution that stems from a simple observation about the local reach-avoid nature of LTL specifications; however, I found the explanation given in Sec 4.2 a bit too complicated. I wonder if that explanation can be simplified, or the authors might even consider adding a figure to assist the reader with the intuition that they are trying to communicate. Also, an experimental comparison with [54] is needed, as that work outperforms [50]. Furthermore, as also mentioned in the paper, the proposed approach is myopic since the goal-conditioned policy doesn't know what the future subgoals are. So, the authors might consider including an experimental evaluation (at least in the appendix) tailored to show this limitation to demonstrate how the proposed approach behaves compared to [50, 54] and DeepLTL in terms of its myopia. That being said, I think the approach presented in this paper is orthogonal to techniques given in [50, 54], in the sense that one can also include LTL formula embeddings [50] or automaton embeddings [54] in the product state and overcome myopia while still leveraging the benefits of the proposed framework. Overall, this is a well-written paper with good experimental evaluation, and such additional experiments and/or further discussion on these issues could make it a stronger contribution and help better position it in the literature.", "was_revised": true, "final_justification": "The authors have adequately addressed my concerns in their rebuttal. I am maintaining my rating (5) and think that this is a good paper worthy of acceptance.", "rebuttal": "We are grateful for the thoughtful comments provided by the reviewer. In the following, we address the weaknesses and questions in detail.\n\n## Weaknesses and Questions\n> 1. Have you tried comparing against [54]? I think this empirical comparison is needed, as [54] is a newer technique that outperforms [50]. Also, do you agree with my comment that LTL formula embeddings [50] and automata embeddings [54] can be incorporated into your technique to overcome the myopia issue? If so, I think the paper can benefit from a discussion highlighting how these different approaches are orthogonal and can be incorporated to get the best of both worlds, i.e., overcome myopia via embeddings and the benefits of your safe RL formulation.\n\nThe evaluation results of [54] and our method (as in Table 1) are shown in the table below. We can see that our method achieves higher success rates in all instances. In addition, our method needs fewer steps to satisfy the specifications in all but two cases ($\\varphi_{11}$ and $\\varphi_{12}$), demonstrating that solving one subgoal at a time is effective also from a performance perspective compared with the state-of-the-art automata embedding-based approach. Moreover, achieving globally optimal behavior requires full observability of the environment states in general, a condition that is often unmet in practice. We elaborate on the performance difference below.\n\n[54] pre-trains the automaton embeddings by sampling from a fixed distribution. As a result, it struggles with out-of-distribution (OOD) generalization when faced with unseen automata. This issue is reflected in its performance degradation under more complex LTL specifications: the success rate $\\eta_s$ drops from 0.9 on $\\varphi_{1-4}$ to 0.82 on $\\varphi_{5-8}$ and 0.94 on $\\varphi_{9-12}$ to 0.7 on $\\varphi_{13-16}$. Additionally, [54] has higher violation rates as it does not model the safety constraint explicitly. \n\nWhile it is possible to integrate automata embeddings with our method (e.g., via state augmentation), whether this will help mitigate the issue of myopic behavior requires further investigation, as it depends heavily on what the agent can observe (as we explain above), and conditioning a policy on information that is not observable can degrade its performance. Besides, integrating such embeddings introduces the additional challenge of OOD generalization (as we explain above and in Sections 5.1 and 5.2).\n\n|                   | ours $\\eta_s$ | ours $\\eta_v$ |    ours $\\mu$    | RAD-embeddings $\\eta_s$ | RAD-embeddings $\\eta_v$ | RAD-embeddings $\\mu$ |\n|:-----------------:|:-------------:|:-------------:|:----------------:|:-----------------------:|:-----------------------:|:--------------------:|\n|    $\\varphi_1$    | $0.98\\pm0.02$ | $0.00\\pm0.00$ |   $7.38\\pm0.13$  |      $0.96\\pm0.04$      |      $0.00\\pm0.00$      |    $18.71\\pm2.06$    |\n|    $\\varphi_2$    | $1.00\\pm0.00$ | $0.00\\pm0.00$ |   $5.48\\pm0.09$  |      $0.90\\pm0.07$      |      $0.07\\pm0.04$      |    $13.64\\pm2.71$    |\n|    $\\varphi_3$    | $0.96\\pm0.01$ | $0.00\\pm0.00$ |   $8.61\\pm0.46$  |      $0.86\\pm0.05$      |      $0.08\\pm0.03$      |    $20.02\\pm2.05$    |\n|    $\\varphi_4$    | $0.98\\pm0.01$ | $0.00\\pm0.00$ |   $7.41\\pm0.37$  |      $0.89\\pm0.04$      |      $0.00\\pm0.00$      |    $18.78\\pm2.82$    |\n|  $\\varphi_{1-4}$  | $0.98\\pm0.02$ | $0.00\\pm0.00$ |   $7.22\\pm1.18$  |      $0.90\\pm0.06$      |      $0.04\\pm0.04$      |    $17.79\\pm3.37$    |\n|    $\\varphi_5$    | $0.99\\pm0.00$ | $0.00\\pm0.00$ |  $10.60\\pm0.12$  |      $0.88\\pm0.05$      |      $0.00\\pm0.00$      |    $26.02\\pm1.62$    |\n|    $\\varphi_6$    | $0.95\\pm0.01$ | $0.00\\pm0.00$ |   $7.48\\pm0.06$  |      $0.90\\pm0.04$      |      $0.00\\pm0.00$      |    $19.48\\pm1.96$    |\n|    $\\varphi_7$    | $0.94\\pm0.01$ | $0.00\\pm0.00$ |  $10.97\\pm0.08$  |      $0.73\\pm0.05$      |      $0.17\\pm0.05$      |    $26.07\\pm3.73$    |\n|    $\\varphi_8$    | $0.93\\pm0.01$ | $0.00\\pm0.00$ |  $10.24\\pm0.08$  |      $0.76\\pm0.11$      |      $0.13\\pm0.05$      |    $25.60\\pm2.89$    |\n|  $\\varphi_{5-8}$  | $0.95\\pm0.03$ | $0.00\\pm0.00$ |   $9.82\\pm1.42$  |      $0.82\\pm0.10$      |      $0.07\\pm0.08$      |    $24.29\\pm3.77$    |\n|    $\\varphi_9$    | $0.99\\pm0.01$ | $0.01\\pm0.01$ |  $380.15\\pm5.17$ |      $0.90\\pm0.07$      |      $0.08\\pm0.07$      |   $423.11\\pm51.08$   |\n|    $\\varphi_{10}$   | $0.97\\pm0.01$ | $0.02\\pm0.02$ | $253.44\\pm10.22$ |      $0.92\\pm0.02$      |      $0.06\\pm0.02$      |   $301.21\\pm101.99$  |\n|    $\\varphi_{11}$   | $0.99\\pm0.01$ | $0.01\\pm0.01$ | $249.57\\pm11.85$ |      $0.93\\pm0.06$      |      $0.04\\pm0.02$      |   $247.83\\pm42.98$   |\n|    $\\varphi_{12}$   | $1.00\\pm0.00$ | $0.00\\pm0.00$ |  $135.60\\pm8.06$ |      $1.00\\pm0.01$      |      $0.00\\pm0.00$      |   $105.97\\pm17.31$   |\n|  $\\varphi_{9-12}$ | $0.99\\pm0.01$ | $0.01\\pm0.01$ | $254.69\\pm89.18$ |      $0.94\\pm0.05$      |      $0.04\\pm0.05$      |   $269.53\\pm129.95$  |\n|    $\\varphi_{13}$   | $0.98\\pm0.02$ | $0.00\\pm0.00$ | $436.25\\pm18.35$ |      $0.69\\pm0.17$      |      $0.00\\pm0.00$      |   $664.59\\pm29.91$   |\n|    $\\varphi_{14}$   | $0.98\\pm0.01$ | $0.00\\pm0.00$ | $434.45\\pm14.61$ |      $0.77\\pm0.21$      |      $0.00\\pm0.00$      |   $628.57\\pm22.89$   |\n|    $\\varphi_{15}$   | $0.97\\pm0.01$ | $0.01\\pm0.00$ | $388.01\\pm15.47$ |      $0.62\\pm0.09$      |      $0.02\\pm0.01$      |    $680.11\\pm9.51$   |\n|    $\\varphi_{16}$   | $0.99\\pm0.01$ | $0.00\\pm0.00$ | $396.83\\pm20.39$ |      $0.70\\pm0.18$      |      $0.00\\pm0.00$      |   $616.28\\pm59.88$   |\n| $\\varphi_{13-16}$ | $0.98\\pm0.02$ | $0.01\\pm0.01$ | $408.71\\pm27.47$ |      $0.70\\pm0.15$      |      $0.00\\pm0.01$      |   $647.39\\pm40.74$   |\n\n> 2. In Figure 6, what were the network sizes and number of training steps for \"Ours (w/o s^\\sigma)\" and \"Ours\"? Were they the same? If so, then do you think that given more compute, \"Ours (w/o s^\\sigma)\" could perform as well as \"Ours\"?\n\nFor fair comparison, the network size and number of training steps for \"Ours (w/o $s^\\sigma$)\" and \"Ours\" are the same. While it is possible that additional compute, such as more training steps or a larger network, could improve the performance of \"Ours (w/o $s^\\sigma$)\", the underlying challenge remains. In the case of \"w/o $s^\\sigma$\", the agent must learn over a much larger space that grows exponentially with the number of atomic propositions. This significantly increases sample complexity which is an issue that cannot be easily overcome by scaling compute alone.\n\n> 3. Does the benefit of the state reduction technique stem from the compression it provides through exploiting the symmetries in the observation? Is it possible to get the same performance with more compute when this state reduction technique is not used? I think a discussion or an experiment on this matter might be helpful to further highlight what this state reduction technique provides. Especially given the fact that it is an environment-specific approach that cannot be used in any environment, it would be good to have a further discussion of how to make the overall method work as well in cases where this state reduction technique cannot be used.\n\nThe state reduction technique indeed exploits the symmetries in the obervation. When this technique is not applicable, we encode the subgoal using the bitvector encoding described in Section 4.1, and it still outperforms the baselines in terms of success and violation rates of the specifications, as shown in the ablation study in Section 5.3. However, it is important to note that due to the exponential complexity, i.e., $2^{|AP|}$, of the state-subgoal combinations (as discussed in lines 157-169), it would be very difficult to achieve comparable performance by simply adding compute when the number of atomic propositions is large."}, {"review_id": "O9ZfJlXhk7", "reviewer": "Reviewer_bwRF", "summary": "This paper introduces GenZ-LTL, a method enabling RL agents to achieve zero-shot generalization for tasks specified in Linear Temporal Logic formulas. The algorithm decomposes LTL requirements into a series of subgoals derived from Buchi automata, which are then solved sequentially using safe RL. The authors confirm that GenZ-LTL works well in simulated navigation environments.", "questions": "1. Suggestion: a more in-depth explanation of the environments, starting in line 250, would be helpful. What is the goal of the agent in these environments? Figure 7 in the Appendix was helpful.\n2. Line 54 oversells slightly, in that the environments are focused on navigation. \n3. Line 239: Did you ever observe the greedy assumption to be an issue? I suppose if the agent were in an environment where it had to actively plan, then this assumption might be?\n4. Line 180: Moving some detail up from appendix or having an algorithm block in the main text might be helpful for understanding here.\n\nThank you for your time!", "limitations": "I think the paper would benefit from an explicit limitations section. Talking points that comes to mind:\n1. The two environments tested both are fairly programmatic, and thus map cleanly onto the LTL specification. How do the authors envision this work generalizing to more realistic settings? \n2. Can one have a perfect LTL specification? We assume here that the agent receives an LTL formula, if I understand correctly, but achieving this formula or description of the environment in the first place seems like a challenge. \n3. How does this method interact with soft constraints or preferences? Do these come up in the intended use case, or can we assume clean alignment with LTL?", "rating": 5, "confidence": 2, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 4, "clarity": 4, "significance": 3, "originality": 4, "strengths_and_weaknesses": "## Strengths\n- The paper's core idea of solving LTL tasks from a goal-conditioned RL perspective is novel, and the results align with the expected benefits of goal-conditioned RL: better zero-shot and OOD generalization.\n- Treating avoid subgoals as hard constraints is also technically impressive.\n- Clear and high-quality writing.\n\n## Weaknesses\nThe primary weakness I find is that the experimental validation, while extensive, is limited to programmatic navigation-style environments. These environments are particularly favorable for LTL, because tasks map cleanly onto rule-based constraints (go here, don't go here). However, one cannot do everything in one paper, so I simply recommend the authors acknowledge and address this in an explicit limitations section, separate from conclusion or broader impacts (more below).", "was_revised": true, "final_justification": "The authors adequately address the limitations I brought up, centering around the toyness of the evaluation and how the method might be applied in real life. Reviewer NmCA brought up concerns about novelty, which I am unqualified to decide, since I am not familiar with the papers cited by NmCA. Accordingly, I have maintained my score and decreased my confidence from 3 to 2.", "rebuttal": "We thank the reviewer for their thoughtful comments and constructive feedback. We address each weakness, question, and limitation below.\n\n## Weaknesess\n> 1. The primary weakness I find is that the experimental validation, while extensive, is limited to programmatic navigation-style environments. These environments are particularly favorable for LTL, because tasks map cleanly onto rule-based constraints (go here, don't go here). However, one cannot do everything in one paper, so I simply recommend the authors acknowledge and address this in an explicit limitations section, separate from conclusion or broader impacts (more below).\n\nWe consider these navigation-style environments as they are also used as benchmarks in prior works [23, 29, 50], thus allowing us to conduct fair comparisons with state-of-the-art methods. We agree with the reviewer that more diverse experimental domains would further strengthen the evaluation. At present, suitable benchmarks for more complex LTL-guided tasks are limited, but we plan to evaluate our method in broader settings as such environments become available (we also have ongoing efforts focusing on creating additional benchmarks). We will explicitly note this in a dedicated limitations section in the next version of the paper.\n\n## Questions\n> 1. Suggestion: a more in-depth explanation of the environments, starting in line 250, would be helpful. What is the goal of the agent in these environments? Figure 7 in the Appendix was helpful.\n\nWe thank the reviewer for the suggestion. Due to page limit, we provide the environment details in Appendix A. In the revision, we will add a brief explanation in the main text to clarify the agent's goal in these environments, such as \"the agent must reach certain regions and avoid others in some order based on the given LTL specification.\"\n\n> 2. Line 54 oversells slightly, in that the environments are focused on navigation.\n\nWe will revise it as \"we conduct comprehensive experiments across a set of navigation-style environments and diverse task specifications, demonstrating that our method consistently outperforms state-of-the-art baselines in zero-shot generalization to arbitrary LTL specifications.\"\n\n> 3. Line 239: Did you ever observe the greedy assumption to be an issue? I suppose if the agent were in an environment where it had to actively plan, then this assumption might be?\n\nFirst, we would like to emphasize that our subgoal-switching mechanism serves as a form of active planning, which is absent in baselines such as [23, 39, 50]. As demonstrated in the evaluation in Section 5.2, these baselines lack the ability to escape from deadlocks caused by unsatisfiable subgoals. Second, we highlight that the presence of unsatisfiable subgoals adds significant complexity to the problem. Consider the specification $(\\mathbf{F}(a \\land \\mathbf{F} b)) \\lor (\\neg a \\mathbf{U} c)$: the agent can either visit $a$ followed by $b$, or avoid $a$ until reaching $c$. Our method may choose the first strategy, visiting $a$ and then attempting $b$. However, if $b$ turns out to be unsatisfiable, the trajectory fails to satisfy the specification since visiting $a$ is irreversible, thus invalidating the second option. This issue is not unique to our method, it also affects baselines with global planning capabilities, such as DeepLTL, because the satisfiability of subgoals cannot generally be determined a priori as we discuss in lines 237-242. \n\n> 4. Line 180: Moving some detail up from appendix or having an algorithm block in the main text might be helpful for understanding here.\n\nWe will move some details from the appendix to the main text, specifically, Appendix B.1, which explains how observation reduction is implemented under different observation settings, and place it after Section 4.2 to improve clarity and understanding of our method.\n\n## Limitations\n> 1. The two environments tested both are fairly programmatic, and thus map cleanly onto the LTL specification. How do the authors envision this work generalizing to more realistic settings?\n\nWe believe that our method can be extended to more realistic settings with some additional effort, but without requiring fundamental changes to the core approach. For example, in autonomous driving scenarios with multiple sensors such as cameras and LiDAR, observation reduction can be enabled through perception modules. Semantic segmentation can be applied to both image and point cloud data to extract relevant features based on the current reach-avoid subgoals. For instance, if the avoid subgoal involves avoiding other cars and pedestrians, and the reach subgoal involves staying within the current lane, then perception can be used to segment the scene accordingly. This allows the agent to focus on task-relevant information and use processed observations, rather than raw sensory data, to learn value functions and policies effectively.  \n\n> 2. Can one have a perfect LTL specification? We assume here that the agent receives an LTL formula, if I understand correctly, but achieving this formula or description of the environment in the first place seems like a challenge.\n\nThis is a very interesting and relevant question. Our work and also prior works on LTL task generalization consider the setting where a formal LTL specification is given as input. In practice, coming up with accurate, formal LTL specifications for complex task requirements can indeed be a challenge. There are many ongoing efforts in the formal methods community to address this challenge, such as automatically converting natural language specifications to formal specifications, designing domain-specific languages to facilitate such specifications, and mining formal specifications from system executions or user demonstrations. These efforts are orthogonal and complementary to LTL task generalization, which is the problem we focus on in this paper.\n\n> 3. How does this method interact with soft constraints or preferences? Do these come up in the intended use case, or can we assume clean alignment with LTL?\n\nIn this paper, we consider problems that require clean alignment with the given LTL specification, i.e., either the LTL specification is satisfied or not satisfied. The semantics of LTL do not support soft constraints, but there are extensions such as Signal Temporal Logic (STL) that incorporate quantitative semantics and enable reasoning about robust satisfaction. There are some works on training RL policies to be aligned with different robustness values of a given STL specification [1, 2, 3]. However, they do not consider generalization to unseen specifications, and STL does not naturally admit an automaton-based representation, which is used for subgoal decomposition in our setting. It would be interesting future work to consider soft constraints or even preferences, but they do not reflect the intended use cases in this paper. \n\n[1] Leung, Karen, Nikos Aréchiga, and Marco Pavone. \"Backpropagation through Signal Temporal Logic Specifications: Infusing Logical Structure into Gradient-based Methods.\" The International Journal of Robotics Research 2023.\n[2] Guo, Zijian, Weichao Zhou, and Wenchao Li. \"Temporal Logic Specification-Conditioned Decision Transformer for Offline Safe Reinforcement Learning.\" International Conference on Machine Learning. PMLR, 2024.\n[3] Meng, Yue, and Chuchu Fan. \"Signal Temporal Logic Neural Predictive Control.\" IEEE Robotics and Automation Letters 2023."}]

Author rebuttal:

Meta-review: This paper presents GenZ-LTL, a framework for zero-shot generalization to LTL tasks by sequentially solving reach-avoid subgoals with state-wise constraints and observation reduction. The method is clearly described and empirically validated, showing consistent improvements over baselines. While the contributions are somewhat incremental and the framing as a safe RL method may be overstated, the work still offers a useful contribution to specification-guided RL.
Decision: Accept (poster)