Automaton Constrained Q-Learning
Authors: Anastasios Manganaris
Vittorio Giammarino
Ahmed H Qureshi
Venue: NeurIPS 2025 poster ()
Keywords: Reinforcement Learning
Safe Reinforcement Learning
Temporal Logic
Automata
Primary area: reinforcement_learning
TL;DR: A novel automaton-based constrained MDP formulation and reinforcement learning algorithm for robot control under task and safety constraints specified via temporal logic.

Abstract: Real-world robotic tasks often require agents to achieve sequences of goals while respecting time-varying safety constraints. However, standard Reinforcement Learning (RL) paradigms are fundamentally limited in these settings. A natural approach to these problems is to combine RL with Linear-time Temporal Logic (LTL), a formal language for specifying complex, temporally extended tasks and safety constraints. Yet, existing RL methods for LTL objectives exhibit poor empirical performance in complex and continuous environments. As a result, no scalable methods support both temporally ordered goals and safety simultaneously, making them ill-suited for realistic robotics scenarios. We propose Automaton Constrained Q-Learning (ACQL), an algorithm that addresses this gap by combining goal-conditioned value learning with automaton-guided reinforcement. ACQL supports most LTL task specifications and leverages their automaton representation to explicitly encode stage-wise goal progression and both stationary and non-stationary safety constraints. We show that ACQL outperforms existing methods across a range of continuous control tasks, including cases where prior methods fail to satisfy either goal-reaching or safety constraints. We further validate its real-world applicability by deploying ACQL on a 6-DOF robotic arm performing a goal-reaching task in a cluttered, cabinet-like space with safety constraints. Our results demonstrate that ACQL is a robust and scalable solution for learning robotic behaviors according to rich temporal specifications.

Automaton Constrained Q-Learning
Anastasios Manganaris, Vittorio Giammarino, and Ahmed H. Qureshi Department of Computer Science Purdue University
(amangana, vgiammar,
Shquureshi)qpurdue.cem /
Abstract
Real-worke robotic tasks often require agents to achieve sequences of goals while respecting time-varying safety constraints. However, standard Reinforcement Learning (RL) paradigms are fundamentally limited in these settings. A natural ap- proach to these problems is to combine RL with Linear-time Temporal Logic (LTL), formal language for specifying complex, temporally extended tasks and safety constraints. Yet, existing RL methods for LTL objectives exhibit poor empirical performance in complex and continuous environments. As result, no scalable methods support both temporally ordered goals and safety simultancously. making them ill-suited for realistic robotics scenarios. We propose Automaton Constrained Q-Learning (ACQL), an algorithm that addresses this gap by combining goal- conditioned value learning with automaton-gum guided reinforcement. ACQL supports most LTL task specifications and leverages their automaton representation to ex- plicitly encode stage-wiss goal progression and both stationary and non-stationary safety constraints. We show that ACQL outperforms existing methods across a range of continuous control tasks, including cases where prior methods fail satisfy either goal-reaching or safety constraints. We further validate its real- world applicability by deploying ACQL on a 6-DOF robotic arm performing a goal-reaching task in cluttered, cabinet-like space with safety constraints. Our results demonstrate that ACQL is robust and scalable solution for learning robotic behaviors according to rich temporal specifications.
Introduction
Achieving desirable robot behavior in real-world applications often requires managing long and complex sequences of subgoals while adhering strict safety constraints. For instance, autonomous mobile robots in warehouse settings must navigate to restock shelves, all while avoiding obstacles and remaining within reachable distance from the recharging station for their current battery level. Similarly, nursing robot must routinely complete its rounds in given sequence, unless notified of an emergency situation.
Despite the success of Goal-Conditioned Reinforcement Learning (GCRL) 4, these approaches fall short in addressing the combined challenges of sequential goals and dynamic safety constraints. GCRL is effective for reaching individual goals but lacks mechanisms for reasoning over goal sequences or ensuring safety. Safe RL enforces fixed safety constraints, but typically assumes they remain static throughout the task, limiting its applicability to temporally evolving tasks.
and Safe RL
Formal languages such as LTL 5 provide an expressive framework for specifying complex tasks involving multiple interdependent goals and non-stationary safety constraints. However, reward functions defined directly from LTL specifications are inherently non-Markovian, since temporal properties refer entire trajectories rather than individual transitions. This violates the Markov assumption-a fundamental premise of standard RL-which assumes that transitions and rewards
39th Conference on Neural Information Processing Systems (NcurIPS 2025).

---

depend only on the current state and action. As a result, RL algorithms built on the Markov Decision Process (MDP) formalism 7 are ill-suited for direct application to LTL--dfined objectives.
To overcome this, some studies 8-10 have proposed to translate the L.TL formula into an automation that tracks temporal progress toward task completion and enables defining Markovian rewards corresponding to temporal specifications. While this approach allows for potentially handling arbitrary LTL formulas, its generality is tied to the use of sparse binary rewards derived from the Boolean evaluation of the specification. In complex environments, however, such sparse signals are encountered too infrequently to effectively guide behavior, and designing denser rewards typically requires additional domain knowledge not readily available in many robotics tasks. Furthermore, these methods only implicitly deal with ensuring safety, as safety properties are fundamental components of many LTL specifications [T] and typically rely on ad-hoc mechanisms, such as halting rollouts 13 both of which tend to be brittle and ineffective in complex domains. Other approaches seek to improve scalability by employing hierarchical [13] or goal-conditioned [4] policies but sacrifice generality, particularly with respect to safety constraints.
12 and reward shaping
To bridge the gap between LTL-capable algorithms that scale poorly and scalable RL algorithms that lack support for most LTL tasks, we propose ACQL, which lifts Safe RL and GCRL the class of problems expressible as LTL formulae in the recurrence class [15]. This algorithm, which we consider
our primary contribution, built on top of two technical novelties that address distinct challenges associated with LTL problems. First, to overcome the poor scalability of sparse rewards, we encode automaton states with their associated goals, enabling the use of goal-conditioned techniques such as Hindsight Experience Replay (HER) 2 to densify reward signals. Second, inspired by Hamilton- product Constrained Markov Decision Process (CMDP) formulation that enforces compliance with arbitrary LTL safety constraints at optimality. We demonstrate these technical contributions are necessary in enabling our ACQL algorithm to significantly outperform other algorithms for solving LTL tasks. Additionally, we demonstrate its effectiveness in learning warl-oddddpplyaabbee policies for a 6-DOF robot arm operating in storage cabinet environment.
Jacobi (HJ) reachability analysis [6. 17, we employ
2 Related Work
The use of LTL specifications with RL algorithms has been a popular topic in recent years 10 One approach to this topic has been directly defining non-Markovian reward functions based on overall task satisfaction, but this only supports LTL formulae that are satisfiable over finite prefixes
13
18
28].
20 In restricted cases where task satisfaction is differentiable with respect to policy's actions, it is also possible to directly train sequence models that satisfy the specification (23) The most popular and general methods, however, convert LTL tasks into automata to use in conjunction with standard deep RL techniques for MDPs 80 I9 22
18
24 28 32 Within these works, there are two subcategories including methods for learning policies that can perform well across a set of multiple LTL tasks
27 and methods that focus on optimally satisfying a single LTL 37 We specifically aim to improve on the scalability of these latter methods in high- nigh-dimensional environments. Of these techniques, we specifically highlight Reward Machines (RMs) (37] as a framework with similar generality to our method and the first baseline we compare against.
20
22
25
task 18-00 12
9
28
32
36
Our work utilizes techniques from GCRL
38 39
to accelerate learning for LTL tasks. Other methods
have taken related approach by learning or re-using goal-conditioned policies that hierarchically
guided by I.TI. expression to enable zero-shot generalization to new tasks [1] 22 26 27 Using
discrete skills as opposed to goal-conditioned policy has also been explored in 13 21). All
these approaches require the user to train a different skill for every automaton edge or different coal-conditioned policy for every safety constraint that appears in the task, except for limited classes of safety constraints. This is impractical for most real-world tasks and, in particular, when safety constraints are changing throughout a task. Conversely, our method learns a single coal-conditioned policy for all goals in a particular LTL expression while still accounting for arbitrary, potentially non- stationary safety constraints. While ACQL has been developed for online RL rather than zero-shot generalization, there is a significant overlap in the tasks that both can ultimately solve. Therefore, we include the Logical Options Framework (L.OF) [3] as a representative for these methods in our experiments.
2

---

Our work is also focused on solving LTL tasks that feature safety constraints. Safety constraints are often indirectly addressed in the methods discussed above. They primarily focus on making unsafe actions suboptimal by either terminating rollouts g
applying negative reward shaping when an unsafe automaton transition oceurs. Other approaches based on formal methods, such as shielding [40] 41] and runtime model-checking [42], can more robustly enforce safety requirements but typically rely on additional assumptions such as access to discrete abstraction of the environment known system dynamics. In contrast, techniques from the Safe RL literature can still robustly enforce stationary safety constraints in complex environments without such assumptions Our approach builds these Safe RL methods to address non-stationary safety constraints induced by LTL specifications.
12
36
13 20
B. 4 43 477.
3 Preliminaries
Constrained Reinforcement Learning RL problems with constraints are typically modeled as discounted CMDPs, which are defined by a tuple (S. T, do, c, C) This tuple consists of a state space S, an action space A, a transition function T: : A + P(S) (where P(S) represents the space of probability measures over S), an initial state distribution do E P(S), reward and constraint functions r, S x A - IR, discount factor y and a limit for constraint violation L E IR (3]. Given a CMDP, the standard objective is find the stationary policy л : - P(A) satisfying the constrained maximization
max J+(IT) s.t.
Je(T) < C.
(1)
where (TT) = Er - "rr, at) and Jo(T) = Er Et= 7 c(ss, at)] are respectively the expected total discounted return and cost of the policy x over trajectories = (so, ag, $1, (1,...... induced by ı through interactions with the environment of the CMDP. We denote the state value at)lsu s) and the state-action value function by
function of by Vi = E, Er 7'r(s,,
(s, = E, t 7 7r((s,, at) 80 8, up a).
Temporal Logic LTL [5] is an extension of propositional logic for reasoning about systems over time. LTL formulae @ E & consist of atomic propositions from a set AP, the standard boolean operators "not" (-), "and" (A), and "or" (V), and temporal operators that reference the value of propositions in the future. These operators are "next" (o), "eventually" (0), and "always" (O). We use Signal Temporal
follow the definitions for these operators given in 488, In our algorithm, Logic (STL), which further extends LTT with quantitative semantics and requires that every atomic proposition p E AP is defined semantics is defined by a function p S x + -> TR that produces a robustness value representing how much a sequence of states w 8 satisfies or violates the property specified by an STL formula á E Q. Our exact implementation of these quantitative semantics is based on [4]] Every temporal logic constraint can be expressed as the conjunction of a "safety" and "liveness" constraint (50), where safety constraint is informally defined as requirement that something must never happen for the task to succeed, and a liveness constraint is defined as a requirement that something must happen for the task to succeed. We take advantage of this dichotomy in our method.
real-valued function of the system state. The quantitative
Automata The robotics tasks discussed so far can be expressed more specifically as STL formulae in the recurrence class, as defined in (15), and all such formulae can be translated into abstract machines called Deterministic Büchi Automata (DBAs) 48. A DBA is formally defined by the tuple A (,, 2, 8, qo, F), consisting of an alphabet Σ, set of internal states Q, transition function 5: Q x + Q, an initial state So E 2, and a set of accepting states C Q. An automaton is used to process an infinite sequence of arbitrary symbols from the alphabet Σ and determine whether the sequence satisfies or does not satisfy the original logical expression. In our setting, a symbol processed by the automaton is subset of atomic propositions / 2 that are true in some MDP state E S. This symbol is referred to as the state's ' labeling and the mapping of states to their labeling is denoted by a labeling function : S + 2AP. The automaton A is always in some state q E Q, and starts in the state qu- Each element a E Σ of an input sequence causes some change in the automaton's 's internal state according to the transition function For convenience, we will refer to edges in the automaton with transition predicates. A transition predicate is propositional formula that holds for all a E which induce a transition between two states gi, q E Q according to 8 ( By processing each state while an agent interacts with an MDP, the internal automaton state provides
3

---

Augmented CMDP
Training
S
G
{
Q5
as
+ 14,2
3
HER
BY
R
(a,9), (8,9) "9nn
Figure 1: The ACQL algorithm relies on novel augmented formulation of CMDPs (left). An input task specification Φ is converted into the DBA A, from which safety constraints and subgoals are collected into mappings S and G respectively. The learning agent receives subgoals 91. : In at every stage in the task from G and safety constraint feedback in e from S. Trajectories induced by the policy πy are collected into replay buffer R, from which batches B3 sampled and modified using HER 22. From these modified trajectories, mini-batches B; of transitions (sg² Ot; r? .et sft1) are used to compute the targets y in (3) and yf in 4 for training models of the state-action value function and safety function, Q7 and Q from which an updated policy æJ+1 is derived.
information to the agent about its current progress in the task. This is the fundamental idea behind a Product MDP, which combines any MDP with a deterministic automaton and is a standard technique in model checking for probabilistic systems [48] A complete definition for a product MDP in an RL context can be found in previous work such [10 37).
Method
This section introduces our ACQL algorithm along with a novel augmented product CMDP on which it is based. An overview is provided in Figure First, detail the construction of the augmented product CMDP derived from task specification. Observations in this CMDP include the set of subgoals associated with the current automaton state q. as described in Section 3 This CMDP also uses safety conditions obtained from the task automaton to provide separate constraint feedback that the learning agent
determine safe actions. Unlike the standard CMDP constraint in ( argue for the use of a constraint on the minimum safety that is easier to learn. We finally present an overview and brief analysis of ACQL, which is tailored to utilize the information provided by our augmented product CMDP to scale beyond existing algorithms for learning in product MDPs.
4.1 Augmented Product CMDP Formulation
Obtaining the Automaton, Safety, and Liveness Constraints To construct the augmented product CMDP used by our algorithm, we begin by translating the input STL task specification é into DBA A = (E,, 2, ö, go, F') using the SPOT library [51]. As described in Section 3] this automaton represents the structure the task. To better guide learning, we extract from this automaton additional structure that captures the task's s safety and liveness requirements. Intuitively, these represent conditions that must always hold avoid failure (safety) and conditions that must eventually hold to make progress toward task completion (liveness) [11, 50]. This information is summarized in two mappings: a safety condition mapping S: Q +, which assigns to each automaton state proposition that must remain true, and a liveness condition mapping O Q + &, which assigns to each automaton state a proposition that must eventually satisfied to proceed in the task. Based
on O we define G: Q + G+ to explicitly link automaton states subgoals, where G = =U"=, g

---

represents the full space of possible subgoal lists up to a task-dependent length n and G' is the i-fold cartesian product of G with itself.
First, to obtain safety constraints, we determine the non-accepting sink-components of the automation A; i.e., the automaton states Q F from which there is no path to any state in F. For each automaton state we then examine the outgoing transitions from q that lead into these sink components. The predicates guarding these transitions describe conditions under which a transition into an unsafe state would occur, so negating these predicates provides the conditions that must hold in order to stay safe while in state q. We can then define S(q) as the conjunction of all such negated predicates for state q.
Second, to obtain liveness constraints, we ignore the above transitions for safety conditions and examine the remaining predicates guarding outgoing transitions from each state g. These can only specify the conditions necessary to make progress in the task. Therefore, we can take the disjunction of these transition predicates obtain the formula ((g) that must be satisfied in order to transition beyond q. Following prior work on learning LTT. tasks 13 [4], we assume that a subset of the atomic propositions, A. subgoal C AP, represent subgoal propositions and are parameterized by values g within a subgoal space G C S. Note that we consider only a subset since not all the propositions in our modified DBA are necessarily related achieving subgoals. Using this fact, we filter the predicates in (g) to retain only those associated with these subgoal propositions, which in turn provides a list of subgoals G(g) g1...... In that are relevant to the logical formula given by (gq). An illustrative example for these two steps is provided in the appendix.
Defining the Augmented Product CMDP Now, let M = (S*A AAA,AAA dd, r cA, 7, L) be new CMDP formed by augmenting the original MDP M (8, T,
with the DBA A = (Σ, 2, 5, go. P). The new state space S S x G x Q is the Cartesian product of the original state space S. the space for every possible list of subgoals G+. and the set of automaton states Q. A state S E S can be written as (s.g*, q). where s E S. gt E g+, and g E Q are the constituent MDP state, goal-list and automaton state of sA. The action space A A unmodified. The new transition dynamics T are defined so that transition to ,',g"', t1 .g") E S from (s,gt, .q) E S is impossible if the automaton does not support transition from q to q when entering the state s'; i.e.
{0000 [(s))ss,))
if if = 5(g, L(s')),  = =((d),
TA "'''"""'lls""...... .)
otherwise.
Likewise, the initial state distribution do ((s gt .q)) do(s) if qo and g G(go), and is zero otherwise. The reward function r ((s g" ". = =r((), where 1(-) is an indicator function, is defined to provide sparse reward of when the task is finished and the agent is near the goal associated with any accepting state of the automaton. Reward sparsity was a central shortcoming of prior work, often resulting in poor performance in realistic scenarios. However, our augmented product CMDP specifically includes the subgoal list g+ to facilitate the use of modern GCRL algorithms to mitigate this sparsity in many relevant tasks. In particular, ACQL retroactively assigns rewards based on achieved subgoals using HER, and the benefit of this strategy for LTL-specified tasks is validated in our ablations (Section 5.3). Lastly, we define the constraint function e along with the constrained objective used with our CMDP formulation.
Minimum LTL Safety Constraint Although the sum-ot sum-of-costs formulation in I conveniently leverages the standard Bellman equation, it presents practical challenges in learning. Specifically, predicting the cumulative sum of future costs requires accurately modeling long-term dependencies, which increases variance and slows down convergence. This can be appropriate for maximizing reward but unnecessarily complicated for safety. When dealing with safety. and in particular hard- safety [52]. we are interesting in knowing whether the generated trajectory becomes unsafe least once. Hence, this can be reformulated as a classification task. This approach bypasses the need for accurate regression by directly learning the decision boundary for state-action pairs leading to safety violations. To achieve this, we define a constraint function e such that it takes negative values if a safety constraint is violated and positive values otherwise, and we apply a constraint based on the minimum over all future values of c (s/ a.). Then, we simply learn to classify this minimum value as being either positive or negative. This formulation allows us to determine safety violations in single step, avoiding the complexity of cumulatíve cost prediction. A major advantage of this formulation is that removes the need for manual tuning of the violation limit L E RR which depends on the range of possible costs. Instead, by directly classifying actions leading to a safety violation,
5

---

end for Algorithm Automaton Constrained Q-Learning
Require: An MDP M = (S, A, ,,,,,,,,o,. do 7),
) an STL specificaato & E t, safety limit L E 1-1,1] learning rate a, an interpolation factor X
1: A <- TRANSLATE(())
2: G + PARTITION(A) (A)
3: .MA < (8A "A,AAAA T dē r end ()
4: Qg O + MMAKENETWORKS
5: 0 <- 0,
6: 4- MATERPLNNUUFFRR
7: for 1, .......N. N do No < SAAETTGGIIMMMSSHHIURRRRR
8:
9:
(s()) arg MIx o)>C 2 (5
10:
T T GETTRAJECTORY
11:
R RUT.
12:
BY ~ R
13:
BJ < RELABEL(B))
14:
for 1.... M do
15:
Bi < {(8) Ut, p A (4,8441 B3 3 + 0 - (V
16:
17:
s + & - aV (1b5,,(bb))
18:
0 + (1 2)0 + 10, f 1
19:
end for
20:
we reduce the range of C to [1, This normalization ensures robustness across tasks and allows for simple, task-agnostic choice L = 0. Directly defining (A((sgg" 9) a) = p(s, S(4)) using the robustness function for S'q) (see Section 3) satisfies this formulation and corresponds to the safety constraints for any STL.-pecified task.
Now, we can define our new objective as finding the optimal stationary policy π² S + P(A) that maximizes the expected total discounted return, as defined in ( while keeping the expected minimum safety above the safety limit C:
min A (i) L, [E(00,0)
where r = (s6- a1, stt ....... is a trajectory within our augmented CMDP induced by the policy π. We denote this expected minimum safety for policy æ by its state-action safety function Q (s, a) = E (min, A (sA as) 8, 0g = a).
4.2 Automaton Constrained Q-Learning (ACQL)
Overview In what follows, we provide an overview of the ACQL algorithm, whose pseudocode is shown Algorithm First, the input STL specification ø translated into an automaton (Line that is partitioned to produce the mappings& S and G (Line 2). These mappings and the automaton are combined with the input MDP M create the augmented CMDP in Line Using the augmented CMDP, ACQL can proceed to learn the optimal policy
π (s
arg max a (a*((*"
Q (**(s4, a),
by learning the optimal state-action value function Q** = Q=- and the optimal state-action safety function Q² = i In order learn these optimal functions, we define the models Q S x R and Q S x A + 1-1, 1] parameterized by ub and 0 (Line 4). Their initial parameters are copied to initialize the target parameters and & in Line 5, and an empty replay buffer is initialized in Line 6.
The algorithm proceeds to iterate for N epochs indexed by j. each epoch, we obtain a value for the safety discount factor yo in Equation which asymptotically approaches 1.0 training progresses

---

(Line 8). The policy T, for the epoch is defined to select the most-rewarding action according to Q constrained by Q6 (Line 9). A trajectory is collected according to an epsilon-greedy version of this policy (Line 10), and this trajectory is added to the replay buffer (Line 11). From this replay buffer, batch of trajectories 33 is sampled every epoch (Line 12). The inclusion of subgoals in the states se of the sampled mini-batch B, allows to further accelerate learning using relabeling techniques such as HER [2]. which allows Q3 to improve from failed attempts at progressing through the task. Mini-batches of transitions B, are subsequently sampled from the relabeled trajectories (Line 15) and used to update Q for minimizing the loss
[WE
- -o ai)) with vi = rf + m
E (n)
(3)
Similarly, Q is trained with the target
uf = mi ar),
++54))))++++++++ (1- (sA,
(4)
which is derived from the Bellman principle of optimality for expected minimum cost objectives given in [16). The targets, yf and y", are computed using target parameters, & and 8, which are updated towards their corresponding main parameters each step with an interpolation factor À (Line 18). Crucially, we schedule the discount factor %e. throughout training to asymptotically approach 1.0. which is necessary for convergence to Q Additional details for the subroutines used in Algorithm are provided in the appendix.
Analysis Under mild assumptions, ACQL is guaranteed to asymptotically converge to the optimal solution. We summarize this in the following proposition:
Let MA be augmented CMDP with |SA| < sc, |A| co, and 7 E [0, 1), and let Qn and Q" be models for the state scte-action safety and value functions indexed by n. Assume they are updated using Robbins-Monne step sizes a(n) and b(n), respectively, with b(n) o(a(n)) according to (3) and (4). Assume that "oo. is also updated with step sizes c(n) such Yo. Yoa - 1 and c(n) E o(b(n)). Then Qú and Qú, converge Q and Q** almost surely n + 00.
Proposition 1.
Proof Sketch. The step sizes a(n). b(n2, and c(n) create a stochastic approximation algorithm on three timescales [53]. Based on the contraction property of (4), the fastest updating Q; asymptotically tracks the correct safety function for the policy determined by Q and Te,, On the slower timescale ensured by the definition of b(n) and a(n), Q converges the fixed point as determined by the
relatively static Ye., due to the contraction property of (3). Finally, as converges on the slowest timescale, the fixed points for the two faster timescales approach Q** and Q at %
In Proposition the notation b(n) E o(a(n)) means that b(n)/a(n) + 0 asymptotically. The assumption of finite MDP is standard in the literature, but relaxing this assumption is possible by applying fixed point theorems for infinite dimensional spaces [54]. After convergence, the final policy will behave optimally for the reward r and (if possible) never incur any cost, thereby respecting the
LTL safety constraint. A complete description of our algorithm, model implementation details, and
full proof of convergence, with reference to similar arguments used in prior work 43 55 56 are
provided in the appendix.
5 Experiments
In this section, we justify the design of ACQL and evaluate its effectiveness. We conducted a comparative analysis of ACQL against established basclines in RL from LTL specifications, including RMs [22 and the LOF [3]. We demonstrate our method's real-world applicability by solving more complex LTL tasks with 6-DOF robot arm in storage cabinet environment. Lastly, performed an ablation study to clarify how our gubgoal-including product CMDP, in combination with HER (2) and our minimum-safety constraint formulation contribute ACQL's performance.
5.1 Comparative Analysis
Baselines In selecting our baselines, we chose to not compare against standard Safe RL methods, offline policy learning methods, and multi-task LTL methods. Safe RL methods, without significant
7

---

(a) PointMass Field
(b) Quadcopter Room
(c) Ant Field
(d) URSe Shelf
Figure 2:
We conducted experiments in simulated environments for navigation tasks using a point mass, quadcopter, and ant quadruped. We also trained policies for end-effector control of a URSe manipulator in a simulated shelf-environment for our real-world experiments.
Table Results from policies trained for five task types in three different environments with 5 million environment interactions and 5 seeds. We report mean and one standard deviation of total reward and success rate in 16 evaluation episodes lasting 1000 steps over seeds for policies the end of training.
ACQL
LOF B
CRM-RS ST
Robet
Task
Reward
S.R.(%) f
Reward 1
S.R.(%)
Reward 1
8.8.(%)
(gu o(0gz))
829.6 9.6
83.8 26.4
11.0 3:00::3.0
98.8 2.6
91.2
0.0 0.0
9,1 A Ou2
841.1 1: 54.1
96.8 18.8::2..
470.7 + 397.5
1.0.0
61.3 61.3.:1 38.6
PM.
A nm-a
868.7 8.2
100.0 0.0
0.0 0.0
0.0
6.0
3.8
1012 o0ga
+
0.0
[g1 A o0g2) mmo1
2.2
62.5 41.8
0.0
0.0 0.0
0.0 0.0
0.0
(gn a(0g2))
100.0 9.7
32.0
98.8
0.0 0.0
0.0
091 A O92 A n-
762.6 167.0
92.5 16.8
161.7 287.6
92.5
6.0
0.0
Q-C.
822.7 + 107.4
05.0111.2
3.5
15.0 20.5
4.1
2.6
Mo14an oOga
726.6
9..4
0.0
0.0
6.0
0.0
O0(91 6092) Lim1
2.4
82.5 36.0
0.0
D.0
6.0
(g1 o(0gz))
091 A Ouz
687.2 19.3
98.8 2.88
168.0
180.6
76.2::4..7
4.6
2.5 2.5 3.4
Ant
0.1 A D
683.7 + 31.1
8..0
38.3
28.8
8.1
6.0
3.8
3.4
36.2
87.5
0.0
0.0
0.0
0.0:::.00
O0 A 6092) mmm
0.9 =
77.5
0.0
0.0 D.0
0.0 0.0
0.0
modification, cannot directly apply LTL tasks and instead only address tasks with stationary safety constraints. Offline methods assume access to a fixed dataset and are not designed for the online learning setting we address. Multi-task methods 200 22
25 27 take special measures to generalize across a distribution of LTL specifications. Comparisons to these methods in a single-task context would therefore require removing significant components from them and would yield strong conclusions regarding their relative merit. We instead compared our algorithm against two methods for online RL with singular LTL specifications: Counterfactual Experiences for Reward Machines with Reward Shaping (CRM-RS) (37 and the LOF [3). CRM-RS employs an RM to define the task and dispense shaped rewards that incentivize task completion. RM states in non-accepting sink components are treated as terminal states, implementing safety constraints. The LOF a framework for learning hierarchical policies satisfy LTL tasks. It learns separate policy, referred to logical option, for satisfying every the task. When training each logical option, each step that violates the task's safety propositions receives large reward penalty (set to R. - 1000 based on their implementation) to discourage unsafe behavior. These policies are then composed with a higher-level policy obtained using value iteration over a discrete state space derived from the task automaton and all the subgoal states of the environment. Both these approaches can handle general LTL specifications and, to our knowledge, represent the most relevant baselines compare our algorithm against. Furthermore, RMs and the LOF cannot be easily enhanced with gegh-performing GCRL and Safe RL techniques without adopting substantial modifications to their learning algorithms and product MDP formulation. Our method effectively integrates these components in a single framework that enables learning from general logical objectives in complex settings, as demonstrated in the following tasks.
strategy to enforce
note that
We chose five distinct LTL tasks and three different agents to facilitate thorough comparison between our algorithm and the two baseline methods. All environment simulation was done within the [57]. The agents used in our experiments are 2D PointMass, Quadcopter, and an 8-DOF Ant quadruped. Additional details for these environments are given in the appendix. We used open environments without physical obstacles for experiments. Instead, obstacles were
Tasks
Brax physics simulator

---

introduced solely through the task specification. This was done to demonstrate the effectiveness of our algorithm avoiding obstacles based purely on feedback from the task specifications, without confounding effects such as physically restricted motion. The L.TI. tasks used in the evaluation include: (1) a two-subgoal sequential navigation task between opposite corners of the environment (o(g) A ()g2))). (2) a two-subgoal branching navigation task between opposite corners of the environment (9g) A (g2), (3) a single-goal navigation task constrained by an unsafe region (Ógı A 1- (4) two-subgoal navigation task with disappearing safety constraint (-o,Ugı A 0g2)), and (5) an infinitely-oooping navigation task with persistent safety constraint (g0(g) A <Ogs) A A The starting position, obstacle and subgoal configurations for each environment are shown in Figure
Results The results for our three simulated environments and five task types are shown in Table All results are reported for the final policy obtained after 5 million environment interactions with five different seeds. For LOF, each individual logical option was afforded its own million training steps for fairness. For each seed, we evaluated the final policy in 16 randomly initialized episodes lasting 1000 steps. We report the reward, which corresponds to the number of steps spent near the final goal of the task automaton, and the success rate (S.R.), which is the proportion of policy rollouts that completely satisfied the task specification for all 1000 steps. Because the robustness of rollouts for the final "Loop" task cannot be meaningfully evaluated over finite trajectory (58), instead compute the success rate by examining the proportion of rollouts that are never unsafe and successfully complete at least 1 full loop within the episode.
We find that these environments, stably reaching subgoals with any non-goal-conditooeed method is unreliable, especially when rewards are delayed based on the task structure. As result, CRM-RS fails for almost all environments and task types. The LOF is able to more easily scale to handle multiple goals due its hierarchical structure and achieves high robustness for most rollouts. However, it also doesn't 't typically obtain high rewards due to only learning to apply options for reaching subgoals, as opposed to remaining
the final goal once the task is satisfied. Furthermore, the tasks with safety constraints clearly demonstrate that rollout termination in CRM-RS and the reward shaping used by LOF is insufficient for reliably preventing the agent from entering obstacle regions. Our method obtained significantly more reward than the baselines, while remaining consistently safe, in all five tasks and environments.
5.2 Real-World Experiments
As first step in determining our algorithm's ap- plicability to controlling robots in the real world for LTL specified tasks, we trained policy us- ing ACQL for controlling 6-DOF manipulator storage cabinet workspace. We trained this policy in the simulated environment pictured in Figure [d] a complex navigation task involy- ing 3 subgoals and 2 obstacles: (p1 Ae(O A (((())))) A (--(in wall V in table)).. The policy trained over 6 actions corresponding to translating the end-effector in the 6 cardinal directions. The geometry of the simulated envi- romment perfectly aligned with the real cabinet workspace, that policy actions based on the state of the simulation could be feasibly executed on the real robot. The resulting policy achieved a mean reward of 908.4 4 and a 100% success rate across 16 simulated rollouts, and we successfully deployed this same policy the real UR5e robot arm and storage cabinet environment visualized in Figure 3 To support reproducibility. all relevant details for the task definition and environment setup are provided in our Supplementary Material. In future work, we intend to support a wider sim-to-real gap and train policies for LTL objectives in partially observable environments. Nonetheless, these initial results demonstrate that our algorithm can effectively leverage feedback from STL tasks in simulation to produce performant and safe policies for real robotic systems.
Figure 3: ACQL, policies trained with safety con- straints based a cabinet's geometry can be success- fully deployed for URSe manipulator operating in the real cabinet environment.
5.3 Ablative Analysis
We conducted an additional ablative analysis to justify two key components of our algorithm. The results are reported in Table In the first ablation, we removed the use of HER from ACQL, requiring

---

Table 2: Results for our algorithm when ablating HER and substituting our minimum-safety CMDP formulation with the standard CMDP formulation. We report mean and standard deviation of the re- ward and success rate collected over all environ- ments, tasks (except the loop task), and seeds from the policy at the end of training in 16 evaluation episodes lasting 1000 steps. For the ablation affect- ing safety constraints, we only report mean perfor- mance in tasks that include safety constraints.
Min. CMDP (Ours)
Sum CMDP
Reward
S.R.%
ACQL
682.5 232.1
91.5 + 20.3
All Tasks
Figure 4: Contour plots for both Q3 and Q trained with ACQL with our CMDP formula- tion in and the standard formulation in
No HER
95.7 = 220.1
12.9 + 29.2
ACQL
545.8 + 365.5
75.4 + 39.1
Safery Tacks
CMDP
8.0 = 24.9
4.6 11.0
the agent learn exclusively from the sparse reward given upon reaching an accepting automaton state. This ablation isolates the effect of our Lubgoal-including product CMDP formulation that enables applying GCRL methods in the context of LTL tasks, and our results show that removing leads to significantly degraded performance.
Our second ablation demonstrates the benefit of our minimum safety constraint ( over the discounted sum-of-cost framework (1) for accurately learning the state-action safety function. We modified our CMDP provide positive costs when there was safety violation, trained Qg to predict discounted sums of costs, and constrained π to choose actions below an upper limit on total cost C. This limit was chosen based on the best performing value L E {0, 10, 40, 60). We report the difference in performance over only the tasks that involved safety constraints and observe that our CMDP formulation is critical the performance of our algorithm. We also show a visualization of the policy differences that result from this ablation in Figure We observe that in our formulation (left), ACQL can more effectively learn the safety constraint, which substantially improves the quality of 2% (bottom). Note that the differing scale for Q5 in our formulation (top left) results in yellow safe region, while the standard formulation depicts low-cost, safe regions in blue.
6 Conclusion
Limitations Although our method outperforms baseline methods in training policies to solve several fundamental types of LTL tasks, there remain few limitations that we aim to address in future work. First, like many approaches leveraging product MDPs [3] 21 32 37]. our method is restricted to logical tasks representable by DBAs. To overcome this, we plan investigate more expressive types of automata for RL, such as fooddfs Non-Deterministi Büchi Automata [59] Second, our current approach approximates the state-action value function without fully capturing task requirements beyond the current set of subgoals. We aim explore more sophisticated goal-conditioned RL methods that can effectively condition a policy on future subgoals provided by our product CMDP. Finally, while our real-world deployment demonstrates the feasibility of applying our algorithm to robot control outside simulation, there are open challenges related to partial observability and sim-to-real mismatch in real-world learning with LTL objectives that aim to address in future work.
We present a novel RL algorithm to tackle complex and high-dimensional LTL-specified tasks, enabled by a novel augmented product CMDP formulation that provides feedback for enforcing arbitrary safety constraints and subgoals for efficiently learning to achieve liveness constraints. By significantly outperforming comparable baselines for learning from LTL specifications, our approach demonstrates promising trajectory toward learning in increasingly complex and realistic environments, without sacrificing generality supporting the full expressiveness of L.T. and other formal languages.
10

---

Acknowledgments
This material is based upon work supported by the Air Force Office of Scientific Research under award number FA9550-24-1-0233. Any opinions, findings, and conclusions recommendations expressed this material are those of the author(s) and do not necessarily reflect the views of the United States Air Force.
References
[1] Tom Schaul, Daniel Horgan, Karol Gregor, and David Silver. Universal value function ap- proximators. In Francis Bach and David Blei, editors, International Conference on Machine Learning (ICML), volume 37 of Proceedings of Machine Learning Research, pages 1312-1320, Lille, France, 07-09 Jul 2015. PMLR.
[2] Marcin Andrychowicz, Filip Wolski, Alex Ray, Jonas Schneider, Rachel Fong, Peter Welinder, Bob McGrew, Josh Tobin, OpenAl Pieter Abheel, and Wojciech Zaremba. Hindsight experience replay. In I. Guyon, U. Von Luxburg, S. Bengio, H. Wallach, R. Fergus, S. Vishwanathan, and R. Garnett, editors, Advances in Neural Information Processing Systems (NeurIPS), volume 30. Curran Associates, Inc., 2017.
[3] E. Altman. Constrained Markov Decision Processes. Stochastic Modeling Series. Taylor & Francis, 1999.
[4] Joshua Achiam, David Held, Aviv Tamar, and Pieter Abheel. Constrained policy optimization. In Doina Precup and Yee Whye Teh, editors, International Conference Machine Learning (ICML), volume 70 of Proceedings of Machine Learning Research, pages 22-31. PMLR, 06-11 Aug 2017.
[5] Amir Pnueli. The temporal logic of programs. In Symposium on Foundations of Computer Science (SFCS), pages 46-57, 1977.
[6] Tuomas Haarnoja, Aurick Zhou, Picter Abbeel, and Sergey Levine. Soft actor-critic: Off-policy maximum entropy deep reinforcement learning with stochastic actor. International Conference on Machine Learning (ICML), 2018.
[7] John Schulman, Filip Wolski, Prafulla Dhariwal, Alec Radford, and Oleg Klimov. Proximal policy optimization algorithms, 2017.
[8] Alberto Camacho, Rodrigo Toro Icarte, Toryn Q. Klassen, Richard Valenzano, and Sheila A. Mcllraith, LTL and beyond: Formal languages for reward function specification in reinforcement learning. In International Joint Conference Artificial Intelligence (IJCAI), pages 6065-6073, International Joint Conferences on Artificial Intelligence Organization, July 2019.
[9] Mohammadhosein Hasanbeig, Alessandro Abate, and Daniel Kroening, Cautious reinforcement learning with logical constraints. In International Conference on Autonomous Agents and MultiAgent Systems (AAMAS), pages 483-491 Richland, SC, 2020. International Foundation for Autonomous Agents and Multiagent Systems.
[10] Mohammadhosein Hasanbeig, Daniel Kroening, and Alessandro Abate. Deep reinforcement learning with temporal logics. In Nathalie Bertrand and Nils Jansen, editors, Formal Modeling and Analysis of Timed Systems (FORMATS), pages 1-22, Cham, 2020. Springer International Publishing.
[11] Bowen Alper and Fred B. Schneider. Recognizing safety and liveness. Distributed Computing, 17-):1 September 1987.
[12] Rodrigo Toro Icarte, Toryn Klassen, Richard Valenzano, and Sheila Mcllraith. Using reward machines for high-level task specification and decomposition in reinforcement learning. In Jennifer Dy and Andreas Krause, editors, International Conference on Machine Learning (ICML), volume 80 of Proceedings of Machine Learning Research, pages 2107-21 16. PMLR, 10-15 Jul 2018.
11

---

[13] Brandon Araki, Xiao Li, Kiran Vodrahalli, Jonathan Decastro, Micah Fry, and Daniela Rus. The logical options framework. In Marina Meila and Tong Zhang, editors, International Conference on Machine Learning (ICML), volume 139 of Proceedings of Machine Learning Research, pages 307-317. PMI.R, 18- 28-244/0 Jul 2021.
[14] Wenjie Qiu, Wensen Mao, and He Zhu. Instructing goal-conditioned reinforcement learning agents with temporal logic objectives. In A. Oh, Naumann, A. Globerson, Saenko, M. Hardt, and S. Levine, editors, Advances in Neural Information Processing Systems (NeurIPS), volume 36, pages 39147-39177 Curran Associates, Inc., 2023.
[15] Zohar Manna and Amir Pnueli. A hierarchy of temporal properties. In ACM Symposium on Principles of Distributed Computing (PODC), pages 377-410, New York, NY, USA, 1990. Association for Computing Machinery.
[16] Jaime F. Fisac, Neil F. Lugovoy, Vicenç Rubies-Royo, Shromona Ghosh, and Claire J. Tomlin. Bridging jamilton-jacobi safety analysis and reinforcement learning. In IEEE International Conference Robotics and Automation (ICRA), pages 5550-8556, 2019.
[17] Kai-Chich Hsu, Vicenç Rubies- Royo, Claire J. Tomlin, and Jaime F. Fisac. Safety and liveness guarantees through reach-avoid reinforcement learning. In Robotics: Science and Systems (RSS), Held Virtually, July 2021.
[18] Xiao Li, Cristian-loan Vasile, and Calin Belta. Reinforcement learning with temporal logic rewards. In JEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), pages 3834-3839, 2017.
[19] Xiao Li, Zachary Serlin, Guang Yang, and Calin Belta. formal methods approach to in- terpretable reinforcement learning for robotic planning. Science Robotics, 4(37):eaay6276, 2019.
[20] Pashootan Vaezipoor, Andrew CLi, Rodrigo A Toro Icarte, and Sheila A. Mcilraith. LTL2Action: Generalizing L.TL instructions for multi-task RL. Marina Meila and Tong Zhang, editors, International Conference on Machine Learning (ICML), volume 139 of Proceedings of Machine Learning Research, pages 10497-10508. PMLR, 18-24 Jul 2021.
[21] Geraud Nangue Tasse, Devon Jarvis, Steven James, and Benjamin Rosman. Skill machines: Temporal logic skill composition in reinforcement learning. In B. Kim, Y. Yue, S. Chaudhuri, K. Fragkiadaki, M. Khan, and Y. Sun, editors, International Conference on Representation Learning (ICLR), volume 2024, pages 05937-36956 2024.
[22] Beyazit Yalcinkaya, Niklas Lauffer, Marcell Vazquez-Chanlatte, and Sanjit Seshia. Automata conditioned reinforcement learning with experience replay. In NeurIPS 2023 Workshop on Goal-Conditionel Reinforcement Learning, 2023.
[23] Zikang Xiong, Daniel Lawson, Joe Eappen, Ahmed H. Qureshi, and Suresh Jagannathan. Co- learning planning and control policies constrained by differentiable logic specifications. In IEEE International Conference on Robotics and Automation (ICRA), pages 14272-14278 2024.
[24] Duo Xu and Faramarz Fekri. Generalization of temporal logic tasks via future dependent options. Machine Learning, 113(10):5509-754) October 2024.
[25] Beyazit Yalcinkaya, Niklas Lauffer, Marcell Vazquez- Chanlatte, and Sanjit A. Seshia. Compo- sitional automata embeddings for goal-conditioned reinforcement learning. In A. Globerson, L. Mackey, D. Belgrave, A. Fan, U. Paquet, Tomezak, and C. Zhang, editors, Advances in Neural Information Processing Systems (NeurIPS), volume 37, pages 72933-72963. Curran Associates, Inc., 2024.
[26] Beyazit Yalcinkaya, Niklas Lauffer, Marcell Vazquez-Chanlatte, and Sanjit A. Seshia. Provably correct automata embeddings for optimal automata-conditioned reinforcement learning. In George Pappas, Pradeep Ravikumar, and Sanjit A. Seshia, editors, International Conference on Neuro-symbolic Systems (NeuS), volume 288 of Proceedings of Machine Learning Research, pages 661-675. PMLR, 28-30 May 2025.
12

---

[27] Mathias Jackermeier and Alessandro Abate. DeepLTL: Learning to efficiently satisfy complex LTL specifications for multi-task RL. In International Conference on Learning Representations (ICI.R, 2025.
[28] Ameesh Shah, Cameron Voloshin, Chenxi Yang. Abhinav Verma, Swarat Chaudhuri, and San- jit A. Seshia. L.IL-constrained policy optimization with eycle experience replay. Transactions on Machine Learning Research, 2025.
[29] Xiao Li, Yao Ma, and Calin Belta. A policy search method for temporal logic specified reinforcement learning tasks. In Annual American Control Conference (ACC), pages 240-245, 2018.
[30] Derya Aksaray, Austin Jones, Zhaodan Kong, Mac Schwager, and Calin Belta. Q-learning for robust satisfaction of signal temporal logic specifications. In IEEE Conference on Decision and Control (CDC), pages 6565-65700 2016.
[31] Anand Balakrishnan and Jyotirmoy V. Deshmukh. Structured reward shaping using signal temporal logic specifications. In IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), pages 3481-3486, 2019.
[32] Eleanor Quint, Dong Xu, Samuel W Flint, Stephen D Scott, and Matthew Dwyer. Formal language constrained Markov decision processes, 2021.
[33] Xiao Li, Yao Ma, and Calin Belta. Automata-guide hierarchical reinforcement learning for skill composition, 2018
[34] Geraud Nangue Tasse, Steven James, and Benjamin Rosman. A boolean task algebra for reinforcement learning. In H. Larochelle, M. Ranzato, R. Hadsell, M.F. Balcan, and H. Lin, editors, Advances in Neural Information Processing Systems (NeurIPS), volume 33, pages 9497-9507. Curran Associates, Inc., 2020.
[35] Kishor Jothimurugan, Suguman Bansal, Osbert Bastani, and Rajeev Alur. Compositional reinforcement learning from logical specifications. Advances in Neural Information Processing Systems, 14:10996-10039 2021.
[36] Mohammadhosein Hasanbeig, Alessandro Abate, and Daniel Kroening. Logically-coostraineed reinforcement learning, 2019.
[37] Rodrigo Toro Iearte, Toryn Q. Klassen, Richard Valenzano, and Sheila A. Mcllraith. Reward machines: Exploiting reward function structure in reinforcement learning. Journal of Artificial Intelligence Research, 73:173-2033 January 2022.
[38] Leslie Pack Kaelbling. Learning to achieve goals. In International Joint Conference on Artificial Intelligence (IJCAI), volume 2. pages 1094-8. Citeseer, 1993.
[39] Tom Schaul, Daniel Horgan, Karol Gregor, and David Silver. Universal value function approxi- mators. In International Conference on Machine Learning (ICML), pages 1312-1320. PMLR, 2015.
[40] Mohammed Alshiekh, Roderick Bloem, Rüdiger Ehlers, Bettina Könighofer, Scott Niekum, and Ufuk Topcu. Safe reinforcement learning via shielding. AAAI Conference on Artificial Intelligence (AAAI), 32(1), April 2018
[41] Bettina Könighofer, Julian Rudolf, Alexander Palmisano, Martin Tappler, and Roderick Bloem. Online shielding for reinforcement learning. Innovations in Systems and Software Engineering, 19(4):3793994 394, December 2023.
[42] Ankush Desai, Tommaso Dreossi, and Sanjit A. Seshia. Combining model checking and runtime verification for safe robotics. In Shuvendu Lahiri and Giles Reger, editors, International Conference on Runtime Verification (RV), pages 172-189, Cham, 2017. Springer International Publishing.
13

---

[43] Dongjie Yu, Haitong Ma, Shengbo Li, and Jianyu Chen. Reachability constrained reinforcement learning. In Kamalika Chaudhuri, Stefanie Jegelka, Le Song, Csaba Szepesvari, Gang Niu, and Sivan Sabato, editors, International Conference on Machine Learning (ICML), volume 162 of Proceedings of Machine Learning Research, pages
PMLR, 17-23 Jul 2022.
[44] Gabriel Kalweit, Maria Huegle, Moritz Werling, and Joschka Boedecker. Deep constrained Q-learning, 2020.
[45] Adam Stooke, Joshua Achiam, and Pieter Abbeel. Responsive safety in reinforcement learning by PID Lagrangian methods. In International Conference on Machine Learning (ICML). JMLR.org, 2020.
[46] Sehoon Ha, Peng Xu, Zhenyu Tan, Sergey Levine, and Jie Tan. Learning to walk in the real world with minimal human effort. In Jens Kober, Fabio Ramos, and Claire Tomlin, editors, Conference on Robot Learning (CoRL), volume 155 of Proceedings of Machine Learning Research, pages 1110-1120, PMLR, 16-18 Nov 2021.
[47] Yongshuai Liu, Jiaxin Ding, and Xin Liu. IPO: Interior-poin policy optimization under constraints. Proceedings of the AAAI Conference on Artificial Intelligence, 34(04):4940-4947, April 2020.
[48] Christel Baier, Joost-Pieter Katoen, and Kim Guldstrand Larsen. Principles of Model Checking. MIT Press, 2008.
[49] Charles Dawson and Chuchu Fan. Robust counterexample-guue optimization for planning from differentiable temporal logic. In IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), pages 7205-7212, 2022.
[50] Bowen Alpem and Fred Schneider. Defining liveness. Information Processing Letters, 21(4):181-185, 1985.
[51] Alexandre Duret-Luuz, Etienne Renault, Maximilien Colange, Florian Renkin, Alexan- dre Ghaguidi Aisse, Philipp Schlehuher-Caissier, Thomas Medioni, Antoine Martin, Jérôme Dubois, Clément Gillard, and Henrich Lauko. From Spot 2.0 to Spot 2. 10: What's new? In International Conference on Computer Aided Verification (CAV), volume 13372 of Lecture Notes in Computer Science, pages 174-187. Springer, August 2022.
[52] Yixuan Wang, Simon Sinong Zhan, Ruochen Jiao, Zhilu Wang, Wanxin Jin, Zhuoran Yang, Zhaoran Wang, Chao Huang, and Qi Zhu. Enforeing hard constraints with soft barriers: safe reinforcement learning in unknown stochastic environments. In International Conference on Machine Learning (ICML). JMLR.org. 2023.
[53] Vivek S. Borkar. Stochastic Approximation: Dynamical Systems Viewpoint. Hindustan Book Agency Gurgaon, 2008.
[54] Andrzej Granas and James Dugundji. Fixed Point Theory. Monographs in Mathematics. Springer, 2003.
[55] Haitong Ma, Changliu Liu, Shengbo Eben Li, Sifa Zheng, and Jianyu Chen. Joint synthesis of safety certificate and safe control policy using constrained reinforcement learning. In Roya Firoozi, Negar Mehr, Esen Yel, Rika Antonova, Jeannette Bohg, Mac Schwager, and Mykel Kochenderfer, editors, Learning for Dynamics and Control Conference (L4DC), volume 168 of Proceedings of Muchine Learning Reseurch, pages 97-109, PMLR, 23-24 Jun 2022.
[56] Yinlam Chow, Mohammad Ghavamzadeh, Lueas Janson, and Marco Pavone. Rist-constrained reinforcement learning with percentile risk criteria, 2017.
[57] C. Daniel Freeman, Erik Frey, Anton Raichuk, Sertan Girgin, Igor Mordatch, and Olivier Bachem. Brax differentiable physics engine for large scale rigid body simulation, 2021.
[58] Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, and Dominik Wojtezak. Omega-regular objectives in model-free reinforcement learning. In Tomás Vojnar and Lijun Zhang, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 395-412 Cham, 2019. Springer International Publishing.
14

---

[59] Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, and Dominik Wojtezak. Good-for- Mor-for-MDDs automata for probabilistic analysis and reinforcement learning. In Armin Biere and David Parker, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 306-323, Cham, 2020. Springer International Publishing.
[60] John N. Tsitsiklis. Asynchronous stochastic approximation and Q-learning Machine Learning, 16(3):185-202: September 1994.
[61] Dimitri P. Bertsekas and John N. Tsitsiklis. Parallel and Distributed Computation: Numerical Methods. Athena Scientific, 2015.
[62] Michal Bortkiewicz, Wladek Palucki, Vivek Myers, Tadeusz Dziarmaga, Tomasz Arezewski, tukasz Kuciński, and Benjamin Bysenbach. Accelerating goal-conditioned RL algorithms and research. arXiv preprint arXiv: 2408. 1005, 2024.
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 that we contribute a novel algorithm for learning tasks specified with LTL formulae (in the recurrence class) that scales to high-dimensional environments better than similarly general existing algorithms. Our experimental results support this claim.
Guidelines:
The answer NA means that the abstract and introduction do not include the claims made in 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
be expected to generalize other settings.
is fine to include aspirational goals as motivation as long is clear that these goals are not attained by the paper.
2. Limitations
Question:
Does the paper discuss the limitations of the work performed by the authors?
Answer: [Yes]
Justification: In Paragraph formulae in the recurrence class (representable as DBAs). We also describe in the paper that these formulae defined over set of atomic propositions with non-safety-related propositions being tied to specific goals goal space G C S. We also state that our policy is only conditioned the current set of subgoals, and therefore limited optimal decision decision-making only for those subgoals without accounting for future subgoal requirements.
clearly describe that our algorithm is limited to STL
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 well-specification, asymptotic approximations only holding locally). The authors should reflect on how these assumptions might be violated in practice and what the implications would be.
15

---

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 the factors that influence the performance of the approach. For example, facial recognition algorithm may perform poorly when image resolution low or images are taken in low lighting. Or speech-to-tex. 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 fairesss.
While the authors might fear that complete honesty about limitations might be used by reviewers as grounds for rejection, worse outcome might be that reviewers discover limitations that aren't 't acknowledged in the paper. The authors should use their best judgment and recognize that individual actions in favor of transparency play an impor- tant role in developing norms that preserve the integrity of the community, Reviewers penalize honesty concerning limitations.
will be specifically instructed
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: [Yes]
Justification: All assumptions are provided for our one (informal) theoretical claim in Section 4.2 and complete and correct proof is included in the appendix.
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 they appear in the supplemental material, the authors are encouraged to provide 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 supplemental material.
Theorems and Lemmas that the proof relies upon should properly referenced.
4. Experimental result reproducibility
Question: Does the paper fully disclose all the information needed to reproduce the main perimental results 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 not)?
Answer: [Yes]
Justification: Algorithm and environment implementation details, including relevant hyper parameters, disclosed in the paper extent that should allow reproduction of the experiments. Additional resources to facilitate reproducibility are provided in code which is included link in the paper.
Guidelines:
The answer NA means that the paper does not include experiments.
If the paper includes experiments, a No answer to this question will not be perceived well by the reviewers: Making the paper reproducible is important, regardless of whether the code and data provided or not.
the contribution is dataset and/or model, the authors should describe the steps taken to make their results reproducible or verifiable.
16

---

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 is specific model and empirical evaluation, it may be necessary to either make possible for others to replicate the model with the same dataset, or provide access to the model. In general. releasing code and data is 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 a large language model), releasing of a model checkpoint, or other means that are appropriate to the research performed.
While NeurlPS does not require releasing code, the conference does require all submis- sions to provide some reasonable avenue for reproducibility, which may depend on the nature of the contribution. For example
(a) the contribution is primarily a new algorithm, the paper should make it clear how reproduce that algorithm. (b) If the contribution is primarily the architecture clearly and fully.
model architecture, the paper should describe
(c) the contribution is a new model (c.g., a large language model), then there should either be way access this model for reproducing the results or way to reproduce the model (e.g., with an open-source dataset or instructions for how to construct the dataset).
(d) We recognize that reproducibility may be tricky in some cases, in which authors are welcome to deseribe 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
Question: Does the paper provide open access to the data and code, with sufficient instruc- tions to faithfully reproduce the main experimental results, as described in supplemental material?
Answer: [Yes]
Justification: We provide open access to anonymized code, along with scripts and an exact description of all required dependencies with version information, needed for running all of our experiments.
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 run to reproduce the results. See the NeurlPS code and data submission guidelines (https http://gnnddeee/eeeeeeeeee
//nips
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. If 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 as much information as possible in supplemental material (appended the paper) is recommended, but including URLs to data and code is permitted.
6. Experimental setting/details
17

---

Does the paper specify all the training and test details (e.g., data splits, hyper- parameters, how they were chosen, type of optimizer, etc.) necessary understand the results?
Question:
Answer: [Yes)
Justification: All training and test information is included in the paper to understand the results, and additional information is included in our supplementary material.
Guidelines:
The answer NA means that the paper does include experiments.
The experimental setting should be presented the core the paper to level of detail that is necessary to appreciate the results and make sense of them.
The full details can be provided either with the code, in appendix, supplemental material.
7. Experiment statistical significance
Does the paper report error bars suitably and correctly defined or other appropriate information about the statistical significance of the experiments?
Question:
Answer: [Yes]
Justification: In Sections 5.1 and 5.3 deviation.
report the variance across trials using standard
Guidelines:
The answer NA that the paper does not include experiments.
The authors should answer "Yes" if the results are accompanied by error bars, confi- dence intervals, or statistical significance tests, at least for the experiments that support the main claims of the paper.
The factors of variability that the error bars are capturing should 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).
should be clear whether the error bar is the standard deviation the standard error of the mean.
It 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 (c.g. negative error rates).
If error bars are 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 the com- puter resources (type of compute workers, memory, time of execution) needed to reproduce the experiments?
Question:
Answer: [Yes]
Justification: In the appendix, we report the total computer resources needed for our experiments.
Guidelines:
The answer NA means that the paper does not include experiments.
The paper should indicate the type of compute workers CPU or GPU, internal cluster, or cloud provider, including relevant memory and storage.
The paper should provide the amount of compute required for each of the individual experimental runs well estimate the total compute.
18

---

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 make it into the paper).
9. Code of ethics
Question: Does the research conducted the paper conform, in every respect, with the NeurlPS Code of Ethics https: bictps://neurip:: http/ppblic/Ethccccieeeeee
Answer: [Yes]
This research (I) does not involve human subjects or participants, (2) does not involve any datasets, (3) has negligible foreseeable societal impact with regard to human safety, security, discrimination, surveillance, deception, harassment, the environment, or human rights issues, (4) does not contain exacerbate biases against groups of people, and (5) includes in its supplementary material conrectly documented, licensed, and anonymized code hase that is sufficient for reproducing the results.
Justification:
Guidelines:
The answer NA means that the authors have not reviewed the NeurIPS Code of Ethics.
If the authors answer No, they should explain the special circumstances that require deviation from the Code of Ethics.
The authors should make sure to preserve anonymity (e.g.. there a special consid- eration due to laws or regulations in 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: We include a discussion of the foreseeable societal consequences this work in appendix.
Guidelines:
The answer NA means that there no societal impact of the work performed.
If the authors answer NA or No, they should explain why their work has no societal impact 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 a direct path to any negative applications, the authors should point it out. For example, it is legitimate to point out that an 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 that a generic algorithm for optimizing neural networks could enable people to 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 being used as intended but gives incorrect results, and harms following from (intentional unintentional) misuse of the technology.
If there negative socictal impacts, the authors could also discuss possible mitigation strategies (c.g., gated release models, providing defenses in addition to attacks, mechanisms for monitoring misuse, mechanisms monitor how system learns from feedback over time, improving the efficiency and accessibility ML).
11. Safeguards
Does the paper describe 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, or scraped datasets)?
Question:
Answer: [NA]
19

---

Justification:
This work has not produced artifacts that pose such risks.
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 by 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
Are the creators or original owners of assets (c.g., code, data, models), used in the paper, properly credited and the license and terms of use explicitly mentioned and properly respected?
Question:
Answer: [Yes]
Our code uses the following libraries: (1) Brax (Apache License 2.0), (2) Mujoco Menagerie (MIT), (3) JaxGCRL (Apache 2.0), (4) Spot (GPLv3). Our paper cites these when discussing implementation details in the appendix. Our code abides by these and other licenses and is itself licensed with the GPLv3 license.
Justification:
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 or dataset.
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.
assets are released, the license, copyright information, and terms use in the package should be provided. For popular datasets, snperswithcode com/ datasete 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 is not available online, the authors are encouraged to reach out to asset's s creators.
13. New assets
Question: Are assets introduced in the paper well documented and is the documentation provided alongside the assets?
Answer: [Yes]
Justification: We include our anonymized code base as one asset and provide alongside the necessary documentation.
Guidelines:
The answer NA means that the paper does not release new assets.
Researchers should communicate the details the dataset/code/model as part of their submissions via structured templates. This includes details about training, license, limitations, etc.
The paper should discuss whether and how consent was obtained from people whose asset used.
At submission time, remember to anonymize your assets (if applicable). You can either create anonymized URL or include an anonymized zip file.
20

---

14. 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 participants and screenshots, if applicable, as well as details about compensation (if any)?
Answer: [NA]
Justification:
This research did not involve crowdsourcing nor research with human subjects.
Guidelines:
The answer NA means that the paper does not involve crowdsourcing nor research with human subjects.
Including this information the supplemental material is fine, but if the main contribu- tion of the paper involves human subjects, then much detail as possible should be included the main paper.
According to the NeurIPS 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 equivalent approval/teview based on the requirements of your country institution) were obtained?
Answer: [NA]
Justification: This research did involve crowdsourcing nor research with human subjects.
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 NeurIPS 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.
16. Declaration of LLM usage
Question: Does the paper describe the usage of LLMs if it is 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.
Answer: [NA]
Justification:
The method developed in this research does not involve LLMs.
Guidelines:
The answer NA means that the method development in this research does not involve LLMs as any important, original, or non-standard components.
Please refer to our L.LM for what should or should not be described.
21

---

A Proof of Proposition
In what follows, we formally prove and restate Proposition]] 1 which shows that ACQL, under mild conditions, is guaranteed to return the optimal policy. Our proof is based on the proof of convergence for Q-learning using stochastic approximation theory in [60), extended with the theory of stochastic approximation under multiple timescales described in Chapter of [53]. Refer also to 43 55 56
for similar analyses. The outline of the section is follows:
1. Express ACQL as a stochastic approximation algorithm
53
60
2. Show that Q and Q" converge to an optimal fixed point for any fixed safety discount factor
To E (0, 1).
3. Restate Proposition I and prove it by showing that as "e + 1, Q" and Q converge to the optimal state-action value function Q** and its corresponding optimal (undiscounted) state-action safety function Q
A.1 Setup
Assumption 1. The augmented CMDP M = (SA, (SA,,,,, .gg, (, ACQL is defined on finite state space S and action space A. For every state E SAA and action a E A, there an associated bounded deterministic reward rea =s a) and bounded constraint feedback = c a.) observed if action a is applied at state
Under Assumption 1. Q and Q" are vectors in Rd where 18 Al is finite. The ACQL algorithm can be modeled as distributed, asynchronous series of noisy updates to components of Qf and Q"
Assumption 2. For each state-action pair (s, E S x A, there are an infinite number of updates applied to the components Qaaa and Qa
The updates to these components are given by
(n + 1) (n) + a(n) [ (11 -c)coa + min(Cas 23 (0))))))))))))) - Qi (n.((n) and
(5)
()) 10= (2) + b(n) (feee + 7Q (()) (T,a((1)) (mn)
(6)
where s¹ is a randomly sampled next state following the state & and action a. The elements of ("(n) and ("(n) are potentially taken from older iterations (V=,o and Q (Vs.a(n) where Va,a(n) (n) is an integer satisfying 0 < (n) I Recall that the policy here is defined as arg @a,,:Q;,.>> Q% in terms of Q" and Q". However, we assume that old information is eventually discarded as n 20.
Assumption 3. For all (s,a), lim (n) co.
Assumption is necessary to prove the convergence distributed asynchronous stochastic approxi- mation algorithms using outdated values (Q" and Q") 160 61). Using Q is additionally necessary to define the operator in (8) such that fixed policy æ can be used to prove the contraction property in L
We also update Ye infinitely often with
Te(n + 1) 7e(n) + c(n) [11 (n)) 7e(n))
and assume that its updates are synchronized with the index for the updates the components of Q' and Q". Assumption 4. The step sizes a(n), b(n), and c(n) for the above updates satisfy
00
a(n)
b(n) = Σ c(n) = 00
n=0
n=0
n=0
8
Σ a(n)², Σ b(n)2 Σ c(n)) 30,
m=0
b(n)) o(a(n)), and c(n) o(b(n)).
22

---

Now, let R XR x - RR and h Rd x R XR- - R be operators defined for each component
(s, a) as
Is.a (0.(QQ" ,0" (e) = 0 To)cso + Vo m 02 (Z
(8)
(Q" - Tc) rsa + + Q [7(7)]
Define a third mapping /'" 0- -,) 1 Without loss of generality, we express the operators as mappings from I2 x Fd E consider them as a coupled mapping from R2d-1 to R2d+1 Finally, define two martingale difference sequences
M (n 1) V/c minfcra, 0z mt(s) (n)) Ve B minfcsas Q
2 (m) and
(10)
Mr s,a (n + 1) >0= ( (n) - 7 BB @5 ((o)
(11)
The updates to y are deterministic. Using the above, we can express the three ACQL updates (5)
6
and 7 as
Pa.a (n +) 22,a (n) + a(n) (Qr.) (=()) (2a(n) + Mg (n + 1)] (12)
Vna + 1) = Q2 (n) + b(n) (Qr (m). (m))) - (m) + My (n + 1)],
(13)
Jo(n +) = (o(m) + c(n) [](Q (m), ro(m)) - 70())]
(14)
Under the above assumptions and formulation, ACQL can now be analyzed as a distributed stochastic approximation algorithm under three timescales.
A.2
Convergence Q" and Q under fixed %
Since the update % happens much more slowly than the updates Q' and Qr-formally, the step size e(n) for % shrinks faster than both 6(n) and a(n)-we can treat Yo as approximately fixed while analyzing the behavior of Q" and Q This allows to study the convergence of Q" and Q assuming that Yo is constant value the interval 1).
Lemma 1. The mapping gf = g(Q", , ..))) Rd - Rd, for some fixed Q", some fixed feasible policy (e.g., a policy based on Q and Q" as in ACQL), and 7 (0, 1), is a contraction mapping.
Proof.
1g"((") -
min Csaa s1 Vo IE o' 1he
min Oz +
%o E
minn 2s (g.
min(csa: ((
S No E
12 Q
( (Iminfa,b) -inffa
Canffa.)] ctl $ 1b -0--)) cl)
S vol110 ve 19
Therefore, ((g) - (2 S %e le 191
Lemma 2. + xc, (n) converges a fixed point A (Q", Ne). for some fixed Q" and Nle-
Proof. The convergence of Q for fixed Q" and %o follows from Theorem 3 (convergence of
distributed stochastic approximation algorithms for a contraction mapping) in [60]. Assumptions 1,
2, and 3 in (60) are satisfied due our Assumptions 3. and the definitions of M M in (TO)
and (TT). Furthermore, the contraction property of g (Lemma I is enough to satisfy Assumption
in [60]. Under these conditions, Theorem in [60 holds true.
Lemma 3. As - Q" (n) updated with using fixed Q*(n) Ai (Q"(()) (n), To), such that there is feasible action in every state, converges the optimal value function Q
23

---

Proof. The mapping h" = h(c, (% : R - Rd for a fixed Q - x(Q", operator for a fixed policy using only actions from a constant non-empty subset of A for each state s. As result, Theorem 4 (convergence of standard Q-learning) in [60] applies.
Te) is a typical Bellman
n
Lemma 4. Q" (1) and (n) asymptotically approach Q and 0% (1 76) as n - Do.
Proof. Lemmas and serve satisfy Assumptions I and in Chapter 6 of [3 The boundedness
of our rewards and constraint signals also result in bounded Q" (n) and (n),, which satisfies
Assumption 3 in Chapter of (53). The proof follows from Theorem 2 (convergence of two-timescale coupled stochastic approximation algorithms) in the same chapter.
A.3 Convergence of (Q", Q9) and
We can apply a similar two-timescale argument now using Yr on the slower timescale and (n), (n))) on the faster timescale. The condition that the faster timescale converges to a fixed point (2(7 for a static Te is shown in Lemma For the condition that the slower timescale converges to fixed point with (Q*(n) (*()) = x2(1))) is true trivially because Ye converges without depending on (Q"(). (n)) at all.
Lemma 5. Y/ converges to as n + oC.
Proof. The update in (14 is discretization of the ODE +i(() = -1--(() The solution this ODE is (1) = 1 - (1 Tal (0( (0)) )e= which asymptotically approaches 1 as - co.
Finally, similar to Proposition 1 in 16. we observe that lim I2.0 (Q") = min(can E. S³ (ss)))
yields a fixed point at Q Er<r [i |so
8, ag al matching the undiscounted in our main paper). Using this fact and another application
minimum-safety constraint (Equation of Theorem 2 in [53] we can prove our Proposition 2
Proposition 2. Let MA be an augmented CMDP with |SA| 00, |A| < co, and y [0, 1), and let (n) and ("(n) be models for the state-action safety and value functions indexed by n. Assume they are updated using Robbins-Monro step sizes a(n) and b(n), respectively, with b(n) o(a(n)) according to (5) and (6). Assume that 7c(n) is also updated with step sizes c(n) such that (n) + 1 and c(n) E o(b(n)). Then (n) and Q" (n) converge to Q and Q** almost surely as + 0c.
Proof. By Theorem 2 from Chapter 6 of [53], whose conditions are satisfied by Lemmas 4 and 5 the coupled iterates (n), Q" (n),,
(n)) converge almost surely to a fixed point (1, A2 (1) with
A2(7)) = (Q% (Q %0' (e)) as n + co. As 7 1, (n) = X1 (Q% 7o) also converges to Erax m 20 Csa, Is0 = s, ag = a) with the policy æ determined by lim (n) = Q"
Therefore, the algorithm attains the optimal state-action value function and the corresponding optimal (undiscounted) state-action safety function Q**
B Additional ACQL Details and Pseudocode
Automaton Analysis To better illustrate the initial automaton analysis in ACQL (Line 2), consider
the automaton in Figure There is only one non-accepting sink-components of this automaton, and is the component consisting of the single node y3. For qo. there is only one transition into this component via the edge labeled by p4, so the safety for go condition is S(40)
-p4. For qi and q2, there are no transitions to a non-accepting sink-component and so their safety conditions are S(gi)= = S(22) = 1, meaning that the safety condition is trivially satisfied at all times in those states. For completeness, we also consider the unsafe states themselves as having safety conditions equal to the conjunction of their negated incoming transitions. Therefore, gs also has the safety condition S(gs) = PP1-
Now we can obtain the liveness constraints, which are summarized in the liveness condition mapping O: Q + + (See Section in our main paper). For go. the only remaining outgoing edge is the one labeled -(p V p2) A pa. Since S(go) = -74, we can eliminate it from this transition predicate to obtain O(m) = (pi V p2). For qt, one can simply obtain O(g) = Py from its only outgoing edge. For completeness, also set O(gz) Pa using the incoming edges for q2 since it is an
24

---

(p1 Vp2) A -4
PB
1
(p) Vpz)A -p
ps
start
90
91
42
P4
43 D
Figure 5: Automaton for the task "Reach goal 9I or 92 while never entering an unsafe-region ui- Then reach 93.", where achieving the goal 9: corresponds to the atomic proposition p; and entering U1 corresponds to Pt. The full LTL expression -p, U ((p) V p2) A oQps). The proposition pa is only relevant to the task's 's safety constraint, and the propositions Pl. P2, and P3 are only relevant to the task's liveness constraints.
accepting state, This is purely to inform the agent of the goal associated with an accepting state once it has reached it. From the above values for O, the mapping G can be defined by G(go) {gr } G(qi)= = {ga} and G(q2)= = {g3).
Subroutines Algorithms
and present the pseudo-code for collecting trajectories in MA. relabeling them with achieved goals, and computing the safety discount factor Ye-
The GetTrajectory function, in Algorithm begins by sampling an initial state from the distribution dg We also randomly sample positions from the environment to associate with each subgoal proposition p E s This task randomization promotes collecting trajectories that explore greater portion the state space through a variety of subgoal sequences, and we found that this was necessary to stabilize training while using HER. We speculate that the greater variety of state and subgoal combinations is needed to train a robust subgoal- -ebgoal-reaching policy. The agent proceeds to interact with the environment for a total of T steps. In a loop indexed by t, actions are selected from an resilon-greedy version of the input policy и (Line 5). The reward, constraint feedback, and next state are observed (Lines 6-8) and stored in the trajectory T (Line 9). After T steps have executed, the trajectory is returned.
The Relabel function, in Algorithm 3 takes batch of trajectories B,, For each trajectory in the batch, the function determines the final achieved state o' and overwrites a single subgoal for every step in the entire trajectory with g'. It also overwrites the reward for each step with for steps that were sufficiently close to g' and 0 for steps that were not. We found that this relatively simple strategy, despite the fact that trajectories were collected with multiple-subgodae subgoals in-mind, was sufficient train reliable goal-reach realhrea policies.
The Safety GreeynaaaaSeeeuleer function, in Algorithm generates values for Yc, starting from initial value and gradually increasing toward 1.0 with exponential decay. To ensure accurate learning of state-action safety function models, it was necessary to cap Yo value slightly below 1.0.
C Model Architectures, Environment Implementation Details, and Hyper-Parameters
Model Architecture and Policy Our method trains two models: the state-action value function, Q and the state-action safety function, Qū. Both models employ twin neural networks and use the minimum of their predicted values mitigate overestimation value and safety estimation. For the ablation study using state-action sum-of-costs function, we likewise use twin networks, but instead take the maximum of the two predictions maintain a conservative (i.e., pessimistic) estimate.
To simplify handling multiple goals, Q" is defined using a goal-conditioned state-action value function model, Q&C, S x G A E. parameterized by t. At runtime, QCC is called for
25

---

Algorithm 2 GerTrajectory
1: function GETTRAAECTOYY
2:
86 ~ do 91 P(g) for pi E Pasagoals
3:
+ 0, + ()
4:
while < do
5:
Te-pooly(st (s(*)
6:
7: - 1 as)
7:
q (st ,as)
8:
A ~ T Ts
+ r (st , Ce,
10:
1 +-t+]
11:
end while
12: return
13:
end function
Algorithm 3 Relabel
function RELABEL(B,)
2:
for 7 E B, do
3:
g' 4 the final goal state achieved in de Replace gi in st with g'
4:
for f
5:
rt + g achieved s/² and 0 otherwise.
7: end for
8:
end for
9:
return B.
10:
end function
each subgoal g E gt This approach exploits the fact that goal condicondi value functions form a Boolean algebra under the min and max operators [21 34 For example, consider two subgoal propositions P1: P2 A sungeul- In the simplest case, when (44) = p1, we compute (7,(s, 91, q). a)) as compute the value the minimum of Q (s. (1, q,a) a) and QCC (s, 92, 9, a). Conversely, when O(4) = p1 Vp (i.e., achieving either subgoal suffices), the value is the maximum Q (s. I1 q, a) and Q&C(2 9,.29.4)) (s,92,424 a.. This pattern generalizes arbitrarily complex Boolean formulae, allowing us to efficiently approximate Q using single goal- conditiod network.
Q (s, 11.91.9900 a). When O(g)= = Pı A P2 (i.e., both subgoals must be achieved to progress), we
We also observed that, because liveness constraints are separated into the goal input, conditioning behavior on the automaton state is only necessary when safety constraints differ between automaton states. As a result, we do not require distinct "mode" for every automaton state E Q, but only for each unique safety condition in the mapping S. To encode this, we train 0 using multi-headed neural network, where each output head corresponds to distinct safety condition. For example, in the automaton shown Figure the mapping S assigns states to one of two safety conditions: -p4 or 1. Accordingly, QCC has two output heads, selected based on the currently active safety condition. In all ACQL experiments, QCC shared hidden layer of 256 neurons across all heads; each head then had an additional hidden layer of 256 neurons. All layers used ReLU activations, and the final output layer had [A] neurons with no activation function.
The model Qi follows the same architecture as Q" with goal-conditioned, multi-headed neural network, but differs in two key respects. First, for disjunctive goal conditions (p1 V P2), the output defined as the minimum of Q (s, 91.9. a) and Q (s. 92. 9, a), to ensure conservative safety by taking the worst-case estimate across disjunctive paths. Second, Q uses a different network architecture; it has two shared hidden layers of 64 neurons each, and each output head includes two additional hidden layers with 64 and 32 neurons, respectively. All layers use ReLU activations. The final output layer consists of [A| neurons with a tanh activation function.
The policy was implemented in terms of these two value functions according to the constrained maximization (s)) = arg max.:Qq (s.)> Q a). In the case that no action was deemed feasible by Qū the safest action max, (* (s, a) was chosen. The exploration policy Te-groody would behave
26

---

Algorithm 4 SaferyGammaScheduler
I: function 3AFETTGAMAASCEEDUERR)
2:
X < J update_period
3: y 4- 1.0 (1.0 init value). decay_ raaee
max value
if max value
4: return
5: end function
above with probability 1 1- c, and with probability select random action without considering Q" or Q'
Environment Implementation For our simulated experiment environments, used the Brax physics simulator [57] and assets provided in JaxGCRL [62] for the PointMass, Quadcopter, and Ant environments. Acting in these environments was facilitated by set of discrete actions corresponding to movement in the cardinal directions. Specifically, the actions in the PointMass and Quadcopter environments output constant low-level action to accelerate directions for 5 consecutive steps. The actions for our UR5e environment, which we used to train our hell-word-deplooee policies, similarly moved the robot's end effector in the 6 cardinal directions for single time step. The actions in the AntMaze environment were policies trained separately using Proximal Policy Optimization (PPO) 7 for 50000000 environment interactions with the objective of maximizing velocity in each of the four cardinal directions and would run for 4 consecutive steps when executed. All further details regarding environment geometry and task definitions for our simulated and real-world experiments are included in our Code Repository!
one of the four or six available
Prree-Parameter Table reports the hyperparameter values most commonly used in our experi- ments, including hyperparameters for the safety gamma (7x) scheduler described in Appendix For a complete account of hyperparameters, as well as ACQL,, baseline, and environment implementation details, refer our Code Repository
Table 3: Hyperparameter values used for experiments in Tables and in our main paper
Hyperparameter Name
Value
Episode length (T'
1000
Discount factor (7)
0.99
Learning rate (a:
1 10
e-greedy factor (e)
0.1
Safety limit (C)
0.0
Safety Gamma Init Value
0.80
Safety Gamma Update Period
250, 000
Safety Gamma Decay Rate
0.15
Safety Gamma Max. Value
0.98
Target parameter interpolation factor (A)
0.005
Compute Resource Requirements All experiments were conducted on a single NVIDIA RTX 3090 GPU (24 GB VRAM), using local workstation equipped with 12th Gen Intel 17-12700F CPU, 32 GB RAM. No cloud services or compute clusters were used. Each individual experimental required approximately 30 minutes of compute time on the GPU. The full experiment grid consists of 225 runs for the comparative analysis and 90 runs for the ablations, amounting to approximately 315 GPU-hours. Minor additional compute used for initial hyperparameter tuning and development.
D Expanded Experimental Results
Figures 6 and 7 show the average reward and success rate throughout training for the baseline comparison experiments summarized in Table T
The LOF baseline cannot be depicted on these
bbaps//gittubbcom///ssssmmaa
27

---

plots as it does not learn a single policy in the same MDP as the other methods, and instead learns policy that chooses -ubeoal-ppecific options for an abstracted state space Q x Sg constructed from the automaton states Q and the finite set of states Sg C S corresponding to task subgoals. Figures and show the average reward and success rate throughout training for the experiments summarized in T in our main paper. The differences in amount of training steps depicted by the figures is due to the different design and training pipelines that the two algorithms observe. ACQL collects complete trajectories to store in the Replay Buffer and CRM-RS just collects individual transitions. We want to highlight that our algorithm converges earlier during the training and this difference does not play significant role in the performance gap reported in Table 1.
28

---

Quadlpper Sequence
S0que000
M
Pairthorrs Branch
Quadooster Sranmh
AAEMAze SONIOS
M
Safolt
Safety
www.
0.0
M
222
PoirtHauss- Unt
Quadecpter
Auchiazn U1tl
033
PURIMMos Lona
Quadcesttrr LOOD
AUVMaze L30G
3.
Awtrage Roward
mi
Timestops
Timesteps
Timesteps
ACOL
CRM-RS
Figure 6: Average and one standard deviation of episode reward throughout training for the five runs method that are summarized in Table I in our main paper.
29

---

Saquence
Sequetcs
24-
M
4.2
Quvecopper Scane
Artiaaee Branch
M
Ouackspie Safecy
Paittaac: Unti
Quadropter Untt
Artiblan Libb1
2/M
Phi-tMooss Laog
QUATEcuptor Loog
A1titaze Loop
W
Timesteps
Timestops
Timestops
ACOL
CRM-RS
Figure 7: Average and one standard deviation of episode success rate throughout training for the five runs per method that are summarized in Table I in our main paper.
30

---

000
Auerage Reward
600
409
200
-200
Quadcopter
1000
300
800
furerage
400
miMaaa Safery
Quedcogtter Swiety
AniiWaze -Salety
fuerage
PointMass Uniil
Quedkopter Until
Averege Reward
200
-200
Timesteps
306
Timesteps
106
Timesleps
145
ACQL
No HER
Min. Safety Critic
Figure 8: Average and one standard deviation of episode reward throughout training for the five runs per ablation group that summarized in Table in our main paper.
31

---

PainkMass Seauence
0.8
02
Quadcopter
1.0
Success Rate
0.4
0.2
-02
PaintMass Salety
Quidd nober Safeety
And Mazee Safery
66-
0.-
Parr Unti
Quadcopier Until
AncMace- USLL
1.2
02-
Timesteps
105
Timesteps
303
Timesteps
145
ACQL
No
Min. Safety Critic
Figure 9: Average and one standard deviation of episode success rate throughout training for the five runs per ablation group that summarized in Table 2 in our main paper.
32


Reviews:
[{"review_id": "iVCca33Ggx", "reviewer": "Reviewer_X2Fi", "summary": "The paper introduces Automaton Constrained Q-Learning (ACQL), a RL algorithm to learn policy that satisfies LTL objectives in continuous domains. The method addresses the challenges of sparse rewards and limited scalability by formulating an augmented constrained MDP that incorporates both safety and liveness constraints extracted from the automaton structure. ACQL leverages goal-conditioned Q-learning with Hindsight Experience Replay (HER) to densify rewards and introduces a minimum-safety constraint formulation to enforce safety without relying on brittle reward shaping or rollout termination.", "questions": "I do not have any specific questions. However, I would like the authors to comment on my concerns mentioned in weaknesses part.", "limitations": "yes.", "rating": 5, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 4, "clarity": 4, "significance": 4, "originality": 4, "strengths_and_weaknesses": "Strengths\n=========\n\nThe paper makes important advancements in the area of learning policies to satisfy LTL specifications. In particular, it nicely combines the decomposition properties of DBA-expressible LTL formulas with CMDP formulation to enable learning LTL-compliant policies. Such a compositional approach is known to be non-trivial, in general. The idea is well motivated, formal proofs are sound, and results are promising. I believe it could have good impact in design of trustworthy RL agents. \n\n\nWeaknesses\n==========\n\nI do not have major concerns.  \n\n1. Given the main content (my pdf doesn't have appendix), it's unclear whether experimental setup considers deterministic or stochastic environments. \n\n2. In obtaining the Automaton... paragraph, it appears that proposition identification is manual. If so, how would misidentification of these subgoals affect the results?", "was_revised": true, "final_justification": "The authors have addressed my minor concerns.", "rebuttal": "Thank you very much for taking the time to review our work and for your positive evaluation. We have addressed the points you raised below and would be happy to provide any additional clarifications if needed. We sincerely appreciate your feedback and support.\n\n## Weaknesses\n\n> It's unclear whether experimental setup considers deterministic or stochastic environments.\n\nThank you for highlighting this point. Our current experiments are indeed implemented using a deterministic simulator, and we agree that this detail should be clarified more explicitly in the final version of the paper. That said, we would like to emphasize that our algorithm is formulated without any assumption on deterministic dynamics and is fully compatible with stochastic environments.\n\n> In obtaining the Automaton... paragraph, it appears that proposition identification is manual. If so, how would misidentification of these subgoals affect the results?\n\nWe confirm that identification of subgoal propositions is currently performed manually, as described in lines 176-178. However, this process is straightforward and involves selecting atomic propositions that correspond to goal-reaching behaviors specified in the given temporal logic formula.  These are typically the propositions that encode states the agent must eventually reach.\n\nWhile it is possible to automate this step in general, we found that manual identification is reliable and poses a minimal one-time overhead in practice. Misidentification would only occur in the case of a malformed or ambiguous specification, in which case any high-level reasoning algorithm would likely fail to generate meaningful goals. In our experiments, we encountered no such issues."}, {"review_id": "uedvN9Sa4N", "reviewer": "Reviewer_58ip", "summary": "The authors propose ACQL (Automaton-Constrained Reinforcement Learning), a RL algorithm leveraging LTL task specifications and their automaton representation to guide the learning of a safe policy while leveraging goal conditioned learning techniques. Specifically, the ACQL method converts a given LTL formula into an automaton, from which safety and liveness constraints are extracted. It distinguishes itself from previous similar methods by the following contributions:\n1. The use of Hindsight Experience Replay to help deal with sparse rewards. ACQL computes subgoals based on the automaton structure. Satisfaction of any of the subgoal provides a learning signal.\n2. Incorporation of safety constraints. The method learns whether a current policy will violate a safety constraint for each state-action pair. This function, in turn, prevents the agent from choosing undesirable actions.", "questions": "The authors state that the minimal safety constraint is better over the discounted sum of cost. Is this always the case? Is the approach only appropriate for hard safety?\n\nWhy would you think of comparing the method against offline policy learning? It is a fundamentally different problem?\n\nThe function that relates propositions set of propositions currently true in the environment, referred to [8] as labeling function might be undefined. Both baselines require such a construct. It seems related to the use of Signal Temporal Logic and function $\\rho$, which is unmotivated. Why would one prefer to use it over the labelling function?", "limitations": "Yes, the authors have addressed the limitation of the proposed method.", "rating": 4, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 2, "clarity": 2, "significance": 2, "originality": 2, "strengths_and_weaknesses": "The paper has the following strengths and weaknesses: \n\nStrengths: \n+ The paper is well-written. \n+ The motivation for safety incorporation is novel.\n+ The use of HER with goals derived from an LTL specification is interesting and is a nice trick to help address the challenge around designing reward functions.\n+ The theoretical analysis of the proposed method is sound and clearly detailed in the appendix\n+ Evaluation is extensive, includes relevant ablations. The use of a real-world experiments is a nice touch and refreshing compared to typical simulation environments.\n\nWeaknesses: \n- While there is value in the proposed approach, in its current form the overall contribution is not substantial enough to constitute a full paper at a conference. Trying to address some of the limitations highlighted in the end would benefit the overall impact of the paper.\n- An analysis of the effect of the complexity of the task (large automaton) on the sample complexity is missing. It is particularly important as the observation space is expanded with the set of sub-goals (potentially quite large in complex tasks).\n- The authors state that the minimal safety constraint is better over the discounted sum of cost. Is this always the case? Is the approach only appropriate for hard safety? I think it should be clarified.\n- Another issue is in their choice of baselines. The authors position the paper as combining GCRL and Safe RL, yet the authors decided to not use any of the Safe RL methods as baseline with the justification that \"Safe RL methods typically address stationary safety constraints\". Only one of the tasks presented in the Experimental section feature such non-stationarity.\n- It is not entirely clear to me whether extending CRM-RS with HER will not achieve the same result.\n- The baseline results seem incorrect. I find it hard to believe that RMs, especially on 1st and 2nd task in the table, almost never solve the tasks. They are designed for these kinds of problems.\n\nMinor writing issues to fix in future versions:\n1. wrong citation for GCRL [1]:\n2. line 232: should it not be in $\\mathcal{S}^A$\n3. formula (3) - elements such as $r_t$ seem to come from the batch but it is not explicitly specified", "was_revised": true, "final_justification": "Based on the authors responses to my questions. I have reviewed my final score.", "rebuttal": "Thank you for taking the time to review our work and for your detailed feedback. We have addressed each of your comments and clarified the points that may have been unclear in the original submission. If our responses resolve your concerns, we would sincerely appreciate your consideration in updating your score. If there are any remaining questions, we would be glad to provide further clarification.\n\n## Weaknesses\n\n> While there is value in the proposed approach, the overall contribution is not substantial enough to constitute a full paper at a conference. Trying to address some of the limitations highlighted in the end would benefit the overall impact of the paper.\n\nThank you for recognizing the value of our approach and for raising this point.\nWe want to emphasize that the contributions of our work lie not only in the technical components, such as the integration of HER with a goal-providing product MDP and Temporal Logic-derived minimum-safety constraints, but also in the accompanying theoretical analysis and practical performance.\n\nThese elements together offer a principled and scalable framework for learning to satisfy singular temporal logic specifications in high-dimensional continuous state spaces.\nWe agree that addressing the remaining limitations would represent an important next step. However, these challenges are not unique to our method and are common to many approaches in the field. Our work takes meaningful steps in this direction and, in our view, provides a valuable foundation that the community can build upon.\n\n> An analysis of the effect of the complexity of the task on the sample complexity is missing. It is particularly important as the observation space is expanded with the set of sub-goals.\n\nWe would like to clarify that the observation space is not necessarily expanded as the number of subgoals increases. As described in lines 172-176, our algorithm augments the observation only with the goal corresponding to the next relevant automaton state. When the automaton includes branching, we concatenate all possible successor automaton states to capture the multiple paths forward. However, in the absence of branching, only a single goal is included. This design keeps the observation space compact in the majority of practical scenarios.\n\nWhile it is theoretically possible for the observation space to grow with automaton size in tasks with extreme branching, we believe this is rare in the types of robotic applications and temporal objectives we are targeting. \n\nWe agree that a deeper investigation into the connection between automaton complexity and sample complexity would be valuable. However, given our current scope, we believe the most immediate contributions lie in demonstrating the practical feasibility of Temporal-Logic-based learning in continuous, high-dimensional environments.\n\n> The authors state that the minimal safety constraint is better over the discounted sum of cost. \n\nThank you for the question. We believe that using the minimal safety constraint provides advantages over the discounted sum of costs in almost all cases. We interpret hard safety as referring to constraints that cannot tolerate any violation, while soft safety allows for partial violations. Our approach can accommodate both by adjusting the threshold $L$ in Equation 2, in much the same way as one would tune $L$ in Equation 1 for the discounted cost formulation. \n\nThe key benefit of our approach lies in the learning feasibility. Training a network to directly classify safety (i.e., learning the sign of $\\min_{t \\in [0, \\infty]} c^A_t$) is significantly easier and more stable than learning to predict a discounted sum of costs and then thresholding the result. For evidence, consider the lower-bounds on sample-complexity for learning a Probably-Approximately Correct binary classifier given in Theorem 6.8 of [1] and for a real-valued regression model given in Theorem 2.1 in [2]. Additionally, the threshold $L$ in Equation 2 has a more direct interpretation as the maximum allowable safety violation, rather than the total accumulated cost, which is harder to reason about in safety-critical applications.\n\nWe will make sure to clarify these points in the final version of the paper.\n\n[1] Shalev-Shwartz, Shai, and Shai Ben-David. Understanding machine learning: From theory to algorithms. Cambridge university press, 2014.\n\n[2] Morgenstern, Jamie H., and Tim Roughgarden. \"On the pseudo-dimension of nearly optimal auctions.\" Advances in Neural Information Processing Systems 28 (2015).\n\n> The authors decided to not use any of the Safe RL methods as baseline with the justification that \"Safe RL methods typically address stationary safety constraints\". Only one of the tasks features such non-stationarity.\n\nWe agree that the current justification in the paper is not sufficiently clear, and we will revise the quoted sentence to provide a more explicit and well-motivated explanation.\n\nSpecifically, while Safe RL methods typically focus on stationary constraints, their scope is also fundamentally different from ours. They are not designed to satisfy general Temporal Logic specifications.\n\nWe will clarify this reasoning in the final version of the paper, around lines 268 to 270.\n\n> It is not entirely clear to me whether extending CRM-RS with HER will not achieve the same result.\n\nWe would like to clarify that simply extending CRM-RS with HER would not achieve the same result as our proposed method. While it is possible in principle to augment CRM-RS with HER, doing so is not straightforward. HER requires a goal-conditioned agent, and adapting CRM-RS to support this would require explicitly constructing a goal-providing product MDP. \n\nEven if such a combination were implemented, it would still rely on rollout termination to enforce safety constraints. Our experimental results show that this approach is significantly less effective than the minimum-safety constraint we introduce.\n\n\n> It is hard to believe that RMs, especially on 1st and 2nd task in the table, almost never solve the tasks.\n\nWhile reward machines are indeed well-suited for representing temporal logic tasks, their effectiveness has primarily been demonstrated in relatively small or discrete environments where rewards are encountered frequently and value function learning progresses more easily. In contrast, the environments we consider are significantly more challenging. They involve high-dimensional continuous state spaces and require long sequences of actions to reach even a single reward, resulting in extremely sparse reward signals.\n\nIn such settings, standard reward-machine-based methods struggle to make meaningful progress, as the agent rarely observes positive feedback. This motivates our proposed approach using goal relabeling and safety-aware learning. Our results reflect this difficulty and highlight the necessity of the design choices made in our method.\n\n### Writing Issues\n\n> Wrong citation for GCRL [1]\n\nWe believe the Universal Value Function Approximators work is an appropriate citation, as it represents a starting point for the field of deep goal-conditioned RL. \n\n> line 232: should it not be in $\\mathcal{S}^A$\n\n\n> formula (3) - elements such as $r_t$ seem to come from the batch but it is not explicitly specified\n\nWhile the states $s_t^A$ in Line 232 are also members of $\\mathcal{S}^A$, we meant by writing $s_t^A \\in \\mathcal{B}_i$ that these are the states included in the batch of sampled transitions $\\mathcal{B}_i$ used for computing the loss in Equation 3. We will further clarify this notation near Equation 3 in the final version of the paper. \n\n## Questions:\n\n> What would you think of comparing the method against offline policy learning? It is a fundamentally different problem?\n\nWe agree that combining offline policy learning with temporal logic objectives is an interesting and promising direction for future research. For instance, one could imagine collecting offline data using policies that satisfy certain LTL specifications and then training new policies to generalize to unseen temporal tasks. However, this would involve a different problem formulation, with different assumptions, training regimes, and evaluation goals.\n\nOur focus in this work is on online policy learning with sparse feedback and safety constraints, where the agent must learn from limited, task-driven interaction in high-dimensional continuous spaces. Exploring how offline learning techniques could complement or extend our framework is a natural and exciting next step, but beyond the scope of the current study.\n\n> The labeling function might be undefined. The use of Signal Temporal Logic and $\\rho$ is unmotivated.\n\nIn our formalism, we chose to define the automaton transition function directly as $\\delta: \\mathcal{Q} \\times \\Sigma \\to \\mathcal{Q}$ with $\\Sigma = \\mathcal{S}$, rather than introducing an explicit labeling function. This can be equivalently viewed as the composition of a labeling function $L: \\mathcal{S} \\to 2^{AP}$ and a transition function defined over $2^{AP}$. While this choice simplifies notation in our setting, we agree that including the labeling function explicitly would improve consistency with standard treatments of automata-based RL and with prior work such as [8]. We are considering adding this to the final version of the paper for completeness and clarity.\n\nThe use of Signal Temporal Logic (STL) in our framework is still compatible with a labeling function. Each atomic proposition $p \\in AP$ is associated with a function over states, and the labeling can be constructed based on their truth values. The robustness function $\\rho$ provided by STL offers an additional advantage by enabling a principled and differentiable way to define our safety constraint function $c^A$, as introduced in line 217."}, {"review_id": "XQR97NyiaZ", "reviewer": "Reviewer_Lw5u", "summary": "The paper introduces ACQL, a reinforcement learning algorithm that integrates goal-conditioned RL with tasks representable as deterministic Buchi automata (this corresponds to a sub-fragment of LTL properties). ACQL addresses scenarios where an agent must achieve temporally ordered sub-goals while respecting time-varying (dynamic) safety constraints – a setting that classical RL struggles with. The key idea is to translate an LTL task specification into a corresponding deterministic Büchi automaton (DBA) and augment the standard Markov Decision Process (MDP) into a product Constrained MDP (CMDP). In this augmented CMDP, each state is a tuple combining the original environment state, the automaton state, and a list of pending sub-goals extracted from the automaton. This construction yields a Markovian representation of the temporal task: the automaton state tracks progress toward task completion, and the sub-goal list encodes the next objectives required by the LTL formula. By encoding automaton-derived sub-goals into the state, ACQL can leverage goal-conditioned techniques (notably Hindsight Experience Replay, HER) to densify sparse rewards. To enforce dynamic safety constraints, the authors propose a novel constraint formulation: ACQL imposes a constraint on the minimum safety value along a trajectory, rather than the usual cumulative cost constraint.", "questions": "1.  Could the authors compare ACQL conceptually to approaches that use shielding or model-checking at runtime (to prevent unsafe actions), or to other LTL-guided RL methods (for instance, those by Hasanbeig et al. on deep LTL RL)?\n\n2. Conceptually it makes sense $\\gamma_c \\to 1$ since you're taking a minimum over the infinite time horizon, in practice does this introduce instability issues? How sensitive is ACQL to the scheduling of the safety discount factor $\\gamma_c$ and the learning rates on the two timescales? I am not familiar with [16] but could you explain how the contraction property can still be shown as $\\gamma_c \\to 1$? Further, did you have to tune the rate at which $\\gamma_c$ approaches 1, or did a simple schedule (e.g., linear annealing) work out-of-the-box?\n\n3. Does the training process itself ever cause safety violations in the environment? For example, in the simulation, if the agent takes an unsafe action, is the episode terminated or is it allowed to continue with a cost? In real-robot experiments, how were safety violations handled to protect the hardware?\n\n4. How do the authors envision extending their approach to more general STL/LTL classes or more complex automata?\n\n5. How can ACQL be adapted to partially observable settings?", "limitations": "The authors explicitly discuss the limitations of their work in the conclusion section. They acknowledge three main limitations: expressiveness of tasks, value function approximation, and real-world partial observability.\n\n### Societal Impact\n\nThe authors state that their research has negligible foreseeable societal impact regarding common concerns like human safety, security, discrimination, I tend to agree with their sentiment.", "rating": 5, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 4, "clarity": 3, "significance": 3, "originality": 3, "strengths_and_weaknesses": "### Strengths\n\n- This work offers a fresh perspective on the integration of formal methods with deep RL, by combining deterministic automata (from LTL/STL) with goal conditioned RL.\n\n- The idea of an augmented product CMDP with sub-goals is novel and addresses the reward sparsity problem in a principled way, in addition, the minimum-safety constraint is an innovative adaptation of reachability analysis to the RL setting, and much more appropriate for safe RL than the usual expected cumulative cost constraint.\n\n- The paper's methodology is solid and well-founded. The augmented CMDP construction is logically sound – by incorporating the automaton state, the LTL-defined reward becomes Markovian, which justifies applying Q-learning, in addition, the use of sub-goal lists for HER has empirical grounding in goal-conditioned value function theory.\n\n- Importantly, the authors include a convergence proof (under mild conditions) for ACQL’s learning algorithm, showing that the two-timescale Q-learning scheme for reward and safety values will converge to the optimal solution with probability 1.\n\n- Clarity is generally ok.\n\n- The experimental evaluation is reasonable, particularly the extension to the real-world robot is interesting.\n\n\n### Weaknesses \n\n-  A notable limitation is that ACQL (like many automaton-based RL methods) is currently restricted to tasks that can be captured by a Deterministic Büchi Automaton (DBA), i.e., belong to the recurrence class. \n\n- The authors choose not to compare to standard Safe RL methods, this is justified by the statement \"Safe RL methods typically address stationary safety constraints\", it is not clear what they mean by stationary safety constraints (see Questions), do they mean temporally extended safety constraints, I am assuming the safety constraints (encoded in the LTL formula) don't change during learning/execution thus they are stationary, in theory one could apply CMDP methods to the product CMDP, I imagine they wouldn't do well as they can't effectively deal with reward sparsity. It would be nice if the authors could address this caveat.\n\n- Most of the gains seem to come from integration of HER (for more efficient learning of sub goals) and CMDP/safe RL (for biasing the class of policies), generally separating reward and safety is more efficient because it divides and conquers the different objectives, the authors claim that the baselines \"RMs and the LOF cannot be easily enhanced with high-performing GCRL and Safe RL techniques without adopting substantial modifications to their learning algorithms and product MDP formulation\" its not clear to me why this is the case, I could imagine extending RMs with HER and some Lagrange relaxation of CMDP for the Bellman update step, this might be non-trivial but I imagine the performance would be much closer to ACQL. While I believe it would be unreasonable to ask the author's to setup such an experiment it might be nice to elaborate on this claim.\n\n- The author's mention STL, although all the formulas are provided with LTL notation, it is unclear how STL is used here, is it used in the goal-oriented learning or something else?", "was_revised": false, "final_justification": "", "rebuttal": "We greatly appreciate your thoughtful and positive review of our work. We have addressed the points you raised below and would be happy to provide any additional clarifications if needed. Thank you for your support.\n\n## Weaknesses\n\n>ACQL is currently restricted to Deterministic Büchi Automaton (DBA).\n\n> How do the authors envision extending their approach to more general STL/LTL classes or more complex automata?\n\nWe acknowledge that ACQL, like many automaton-based RL methods, currently focuses on tasks expressible by DBAs. However, we note that the majority of practically useful tasks, like those involving goal recurrence and safety, fall within this class. This is further supported by the fact that the most recent methods that are capable of handling more general specifications (e.g., those with persistence requirements) often do not demonstrate such tasks in their experiments [1]. This suggests the additional complexity they introduce remains a barrier in practice, and extending our approach to broader temporal logic classes remains a promising direction for future work.\n\nWe expect the first step in extending our approach will, similar to other methods, involve using non-deterministic Good-for-MDPs automata [2] (e.g., Limit-Deterministic Büchi Automata) to define our product CMDP and augmenting the action-space so that the policy may choose how to optimally resolve the resulting non-deterministic choices [3]. We are also interested in investigating how these non-deterministic choices are resolved in the presence of other reward signals and constraints.\n\n> it is not clear what they mean by stationary safety constraints.\n\n> in theory one could apply CMDP methods to the product CMDP\n\nThank you for raising this point. In this context, we mean by non-stationary that the safety constraints can change throughout a task as the agent progresses, as opposed to changing between learning and execution. It is possible to overcome this initial limitation by applying standard CMDP methods to the product CMDP, but we show in our second ablation (row 4 of Table 2) that standard sum-of-cost CMDP constraints struggle to address the safety requirements of our tasks compared to the minimum-safety formulation we propose.\n\n> the authors claim that the baselines \"RMs and the LOF cannot be easily enhanced with high-performing GCRL and Safe RL techniques without adopting substantial modifications to their learning algorithms and product MDP formulation\" \n\nThank you for the question. To clarify, applying HER to CRM-RS is not directly feasible, as HER requires a goal-conditioned agent, whereas CRM-RS operates in a standard product MDP that lacks an explicit goal representation for relabeling. Introducing goal-conditioning in such a way that does not modify the original temporal logic task is non-trivial; in our case, we achieve this by encoding each automaton state with its associated set of goals.\n\nSimilarly, LOF relies on a single product MDP and could, in principle, use HER to train a goal-conditioned policy in place of subgoal-specific options. However, this would then require adopting a different strategy for addressing the dynamic safety constraints imposed by the LTL specification, as each LOF option is trained both for reaching its associated goal and adhering to safety constraints relevant to that goal.\n\n> The author's mention STL, although all the formulas are provided with LTL notation, it is unclear how STL is used here\n\nThank you for raising this point. We specifically use the quantitative semantics (i.e., the robustness function) provided by STL in lines 216 - 219 to define the safety feedback function $c^A$. The remaining formulae are still expressed in STL notation, but without explicitly writing the default timing parameters ($[0, \\infty]$) for each temporal operator.\n\n## Questions:\n\n> Could the authors compare ACQL conceptually to approaches that use shielding or model-checking at runtime (to prevent unsafe actions), or to other LTL-guided RL methods [6]?\n\nThese comparisons could be made as well. To summarize, shielding and model-checking for RL are, relative to our method, significantly more based on classic formal synthesis and verification techniques, and they consequently are more dependent on discrete models of the environment dynamics. Shielding specifically uses reactive synthesis to obtain, from a safety LTL specification and an abstraction of the system dynamics, a reactive system that can be used to minimally modify an arbitrary RL agent so that unsafe actions are never chosen. Runtime model checking approaches in general also rely on environment models to verify the overall safety of a policy and continuously check that runtime behavior matches the prediction of the model used in verification in order to ensure the policy remains safe. In contrast, our method does not rely on a model and supports more than just the safety fragment of LTL specifications.\n\nWorks such as [4] by Hasanbeig et al. on deep LTL RL are more comparable to our method, as they are model-free RL approaches relying on rewards from an automaton. However, we include the Reward Machines baseline as a similar algorithm that is slightly simpler and more appropriate for our fully-observable setting.\n\n> In practice does $\\gamma_c \\to 1$ introduce instability issues? How sensitive is ACQL to the scheduling of the safety discount factor and the learning rates on the two timescales? Could you explain how the contraction property can still be shown as $\\gamma_c \\to 1$?\n\nIn practice, this does indeed introduce some instability at values of $\\gamma$ very close to 1, as small inaccuracies due to approximating the safety value function can quickly propagate and worsen the quality of the rest of the value function. Fortunately, this can be resolved by capping the $\\gamma_c$ value at a maximum value of $0.99$. Because $\\gamma_c$ only approaches and never equals or exceeds 1, the contraction property shown in Theorem 1 of [16] holds throughout the execution of our algorithm. On the other timescales, the learning rates for $Q^c$ and $Q^r$ did not have to be tuned at all for our algorithm to succeed in practice.\n\n> Further, did you have to tune the rate at which $\\gamma_c$ approaches 1, or did a simple schedule (e.g., linear annealing) work out-of-the-box?\n\nVery minor tuning was initially required so that $\\gamma_c$ increased slowly enough so that an initial safety value function could be quickly learned, but after this a straightforward schedule based on exponential decay worked out-of-the-box. \n\n> Does the training process itself ever cause safety violations in the environment? If the agent takes an unsafe action, is the episode terminated or is it allowed to continue with a cost? In real-robot experiments, how were safety violations handled to protect the hardware?\n\nOur algorithm does require experiencing transitions that violate safety requirements in order to learn the safety value function, and so we do not terminate episodes upon safety violations. We note that a buffer can be instated for the safety requirements so that safety violations do not immediately result in harm to the robot.\n\nFor our real-robot experiments, training was exclusively performed in simulation to the point that safety constraints were not encountered during deployment of the policy.\n\n> How can ACQL be adapted to partially observable settings?\n\nWe wish to clarify that a partially observable setting in this context refers to a domain where the agent can only receive partial observations (e.g. images) or imperfect information of the underlying system state, but the task specification is still defined in terms of this underlying state.\n\nIn order to extend ACQL to this setting, we envision first augmenting the network so that throughout execution the history of observations is processed to obtain a latent representation of the underlying state, with which a Markovian policy should be well-defined.  Second, because atomic propositions relevant to the task specification can not be directly measured but instead must be deduced from the history of observations, our extended method should assume access to or learn a probabilistic function, similar to the one used in [4], for evaluating propositions. \n\nSubsequently, our method could maintain a probability distribution over automaton states to represent the agent’s belief about its current progress and update this distribution based on the incoming observations. Periodically sampling from this distribution would then yield a concrete subgoal list, which will be relabelled based on the final achieved subgoals. We believe this to be a very interesting and challenging direction for future developments of our work and the field of policy learning methods using temporal logic.\n\n[1] Jackermeier, Mathias, and Alessandro Abate. \"Deepltl: Learning to efficiently satisfy complex ltl specifications for multi-task rl.\" The Thirteenth International Conference on Learning Representations. 2025.\n\n[2] Hahn, Ernst Moritz, et al. \"Good-for-MDPs automata for probabilistic analysis and reinforcement learning.\" International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Cham: Springer International Publishing, 2020.\n\n[3] Hahn, Ernst Moritz, et al. \"Omega-regular objectives in model-free reinforcement learning.\" International conference on tools and algorithms for the construction and analysis of systems. Cham: Springer International Publishing, 2019.\n\n[4] Hasanbeig, Mohammadhosein, et al. \"Reinforcement learning for temporal logic control synthesis with probabilistic satisfaction guarantees.\" 2019 IEEE 58th conference on decision and control (CDC). IEEE, 2019."}, {"review_id": "42Z4qUpsvF", "reviewer": "Reviewer_v818", "summary": "The paper introduces Automaton Constrained Q-Learning, an algorithm for learning Reinforcement Learning (RL) policies for objectives given as Linear Temporal Logic (LTL) formulas. The method combines the use of LTL objectives in RL and safe RL techniques by rewarding based on the acceptance of the induced automaton of the given LTL formula and enforcing inferred safety constraints during training. Specifically, for the given LTL task, its safety and liveness components are extracted and used as reward and cost, respectively, in a product CMDP formulation while applying constraints based on the minimum over all future values of the cost, instead of a sum-based formulation. Then, separate Q-functions are learned simultaneously for reward and cost. Optimal actions are chosen w.r.t. the reward Q-values among the safe actions given by thresholding the cost Q-values. The authors present a proof of convergence for their algorithm as well as experiment results both in simulation and real-world settings.", "questions": "1. What is the main reason behind the sim2real success? Is it thanks to the proposed approach? Or was it an engineering effort? Have you tried any of the baselines in this setting? If so, what was their success rate?\n2. How do you pass the subgoal lists to the networks? Is it possible to use LTL formula embeddings [5] or automata embeddings [6, 7] instead of subgoal lists? If so, what is the advantage of using subgoal lists over such embeddings?\n3. Not algorithmically, but in terms of what is achieved, what are the differences between DeepLTL [1] and the proposed approach? Does the proposed approach provide anything that DeepLTL doesn't?", "limitations": "yes", "rating": 4, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 2, "clarity": 3, "significance": 2, "originality": 2, "strengths_and_weaknesses": "Strengths:\n- The paper presents a novel algorithm combining LTL objectives in RL and safe RL techniques in a non-trivial way. Developing learning algorithms tailored for the use of formal specifications in RL is a relevant contribution.\n- The proof of convergence for the algorithm seems sound, but I went through the proof only once so definitely it needs to be checked again in more detail. That being said, from the theoretical formulation of the method, the convergence result is intuitive and as expected. I even wonder if there could be a shorter and easier-to-read proof for the same result.\n- The real-world experiment performed on a 6-DOF robotic arm is one of the most interesting aspects of the paper, especially given that the training was done in a simulation environment and that the physical robot had a 100% success rate in real-world tests. I wonder if this sim2real success was an engineering effort or something enabled by the choice of minimum safety constraint or any other design choice made by the authors.\n\n\nWeaknesses:\n- In my opinion, the main weakness of the paper is that the time for this paper might have already passed. Specifically, there have been significant efforts and successes in the literature for using LTL objectives in RL over the last decade, some of which are cited in the paper as well. So, even though the proposed algorithm is a novel contribution to the best of my knowledge, its impact is debatable. Moreover, I think with a little bit more effort, the approach can be extended to multi-task settings, i.e., the same policy performing a large class of LTL tasks, or even, probably with more effort, to multi-agent ones.\n- Some important related work is missing [1, 2, 3, 4, 5, 6, 7]. DeepLTL [1] is a relevant baseline, and the authors should definitely consider comparing against this work both in simulation and real-world settings. A discussion of the difference between the proposed approach and [2, 3] is needed. Using HER in a multi-task RL context was proposed in [4]. Also, I am curious if LTL formula embeddings [5] and automata embeddings [6, 7] can be used here instead of the subgoal lists in the product CMDP definition, as these embeddings can be a compact way to substitute the same information (and probably even more) provided by subgoal lists. Overall, it is hard to properly position the paper in the literature without these discussions and a comparison with DeepLTL.\n- There are some issues with the formalism. In line 133, it is said that the alphabet of the automaton is the MDP states, which is fine in discrete state spaces, but if the state space is continuous, then the alphabet is uncountably infinite. So, I would recommend explicitly defining a labeling function as is usually done in the literature. In line 137, it is said that there are propositional formulas on the transitions that hold for all symbols in the alphabet, then does that mean any symbol would trigger any transition on the automaton? It is unclear what is meant here. Also, such a formulation, i.e., using propositional formulas on transitions, is almost describing a symbolic automaton rather than a Büchi automaton. In line 164, to define G^+, G^i is used but it is not clear what G^i is. It is later informally clarified in the paper but that initial part is confusing. In line 196, it is said that subgoal lists facilitate the use of HER, it is not clear why this is the case. HER can be easily applied in a standard product MDP definition (without subgoal lists) as well. Also, including Algorithm 1 (or a shorter version of it) in the main body of the paper might be helpful to the reader.\n\n[1] Jackermeier, Mathias, and Alessandro Abate. \"Deepltl: Learning to efficiently satisfy complex ltl specifications for multi-task rl.\" The Thirteenth International Conference on Learning Representations. 2025.\n\n[2] Shah, Ameesh, et al. \"LTL-Constrained Policy Optimization with Cycle Experience Replay.\" arXiv preprint arXiv:2404.11578 (2024).\n\n[3] Xu, Duo, and Faramarz Fekri. \"Generalization of temporal logic tasks via future dependent options.\" Machine Learning 113.10 (2024): 7509-7540.\n\n[4] Yalcinkaya, Beyazit, et al. \"Automata conditioned reinforcement learning with experience replay.\" NeurIPS 2023 Workshop on Goal-Conditioned Reinforcement Learning. 2023.\n\n[5] Vaezipoor, Pashootan, et al. \"Ltl2action: Generalizing ltl instructions for multi-task rl.\" International Conference on Machine Learning. PMLR, 2021.\n\n[6] Yalcinkaya, Beyazit, et al. \"Provably Correct Automata Embeddings for Optimal Automata-Conditioned Reinforcement Learning.\" arXiv preprint arXiv:2503.05042 (2025).\n\n[7] Yalcinkaya, Beyazit, et al. \"Compositional automata embeddings for goal-conditioned reinforcement learning.\" Advances in Neural Information Processing Systems 37 (2024): 72933-72963.", "was_revised": true, "final_justification": "The authors have adequately addressed my concerns in their rebuttal; therefore, I am increasing my rating by one point (3 --> 4), assuming the final version of the paper incorporates the clarifications provided in the rebuttal and the discussion of the highlighted related work.", "rebuttal": "Thank you for your insightful review and for taking the time to engage critically with our work. \n\nWe have addressed each of your points in the responses below. If our clarifications resolve your concerns, we would be grateful if you would consider raising your score. Thanks again for your feedback, which has helped improve our work.\n\n## Weaknesses\n\n> Even though the proposed algorithm is a novel contribution to the best of my knowledge, its impact is debatable. \n\n> The approach can be extended to multi-task or multi-agent settings.\n\n\nWe want to emphasize that the contributions of our work lie not only in the technical components of the algorithm itself, such as the integration of HER with a goal-providing product MDP and Temporal Logic-derived minimum-safety constraints, but also in the accompanying theoretical analysis and empirical performance..\n\nWhile the use of temporal logic in RL has seen progress over the past decade, we believe that key challenges still remain, particularly when scaling to continuous, sparse-reward, and safety-critical environments. Our method directly targets this space and advances the state of the art in integrating temporal logic with Deep RL.\n\nWe agree that extending this approach to multi-task and multi-agent settings would be a valuable next step. These directions pose non-trivial challenges and, in our view, our work provides a strong foundation upon which such work can be built. \n\n> Some important related work is missing [1, 2, 3, 4, 5, 6, 7]. \n\nThank you for bringing these works to our attention. We agree that they are highly relevant and we will include them in the final version of the paper. \n\n> DeepLTL [1] is a relevant baseline, and the authors should definitely consider comparing against this work.\n\n> In terms of what is achieved, what are the differences between DeepLTL [1] and the proposed approach?\n\n\nDeepLTL focuses on a different setting. It is designed for the multi-task paradigm, where the objective is to generalize across a distribution of LTL specifications using learned task embeddings. In contrast, our method targets single-task learning in high-dimensional continuous environments, with an explicit focus on safety.\n\nBecause of this difference, applying DeepLTL in our setting would require disabling several of its core mechanisms, such as multi-task generalization and curriculum-based training. For this reason, we believe a direct comparison would not be meaningful. \n\nAdditionally, DeepLTL places less emphasis on the RL backbone and on safety. It uses standard PPO within classical MDPs, whereas we adopt a CMDP formulation consistent with the safe RL literature, and introduce a product-CMDP construction along with a theoretical analysis. \n\nFrom examining the experimental domains featured in both works, we believe a key distinction is our method’s ability to learn effective policies in environments with complex robot dynamics and explicit safety requirements. In particular, our use of minimum-safety constraints instead of rollout termination results in greater robustness and safety guarantees.\n\nWe view these two approaches as complementary. DeepLTL advances generalization across tasks, while our method focuses on safely and effectively satisfying a single temporal logic specification in complex continuous domains. Exploring how to combine the strengths of both approaches is a promising direction for future research.\n\n> A discussion of the difference between the proposed approach and [2, 3] is needed. Using HER in a multi-task RL context was proposed in [4].\n\nThank you for pointing this out. We will include these references and discuss them in the Related Work section of the final version of the paper.\n\nSpecifically, the work in [2] is also orthogonal to our work and provides a technique for providing additional rewards based on the agent’s partial completion of accepting cycles in the task automaton. \n\nThe work in [3] is also a multi-task RL approach that, similar to the LOF [8], trains an option for several goals and also conditions each option on a representation of the possible sequence of subsequent goals. [4] also is an interesting approach that uses HER directly with goals based on embeddings of task automata, which we believe is distinct from our method’s use of HER for densifying rewards in a single-task setting. \n\n> LTL formula embeddings [5] and automata embeddings [6, 7] can be used here instead of the subgoal lists in the product CMDP definition\n\n> What is the advantage of using subgoal lists over formula embeddings [5] or automata embeddings [6, 7]?\n\n\nThank you for this question. We agree that using LTL formula embeddings or automata embeddings is an exciting direction, particularly in the context of multi-task learning.\n\nIn the single-task setting, we find it more effective to rely on explicit subgoal lists. Compressing an entire temporal logic objective into a single embedding introduces a layer of abstraction that may obscure the precise semantics of the task, making learning harder and less interpretable. In contrast, subgoal lists offer a direct representation of the automaton's state and progression, which provides clear task guidance at each step.\n\nUnderstanding how to combine the interpretability and task specificity of subgoal-based representations with the scalability and generalization potential of embedding-based approaches is an exciting direction for future work.\n\n> In line 133, it is said that the alphabet of the automaton is the MDP states. if the state space is continuous, then the alphabet is uncountably infinite.\n\nWe agree that defining a labeling function $L : \\mathcal{S} \\to 2^{AP}$ and the automaton in terms of the alphabet $\\Sigma = 2^{AP}$, as opposed to directly defining the automaton transition function as $\\delta: Q \\times \\Sigma \\to Q$ with $\\Sigma = \\mathcal{S}$, will improve clarity and our consistency with the literature. We are considering accordingly modifying our definitions in the final version of the paper.\n\n> In line 137, It is unclear what is meant by propositional formulas on the transitions that hold for all symbols in the alphabet.\n\nWe introduce this definition of transition predicates, inspired by the terminology on page 3 of [9], to more easily discuss the implications of the automaton transition function $\\delta$. These predicates still only are true for a subset of symbols, so it is not the case that any symbol can trigger any transition, and we believe this terminology is still compatible with Büchi automata.\n\n> In line 164, it is not clear what G^i is.\n\nThe $\\mathcal{G}^i$ refers to the i-fold cartesian product of $\\mathcal{G}$ with itself, and we agree this should be made more clear. We intend to resolve this in the final version for the paper.\n\n> It is not clear why subgoal lists facilitate the use of HER. Also, including Algorithm 1 in the main body of the paper might be helpful to the reader.\n\nAn obstacle to applying HER to a standard product MDP is that the standard product MDP defines no notion of goal that is compatible with the temporal logic task. HER would require such a goal in order to perform relabeling for the episode, but adding goal-conditioning while still supporting the task specified by the reward machine is not trivial. Other methods require introducing another representation of goals in order to enable goal-conditioning, such as the reach-avoid sequences in DeepLTL or automata embeddings in [4]. Our work instead introduces the subgoal lists to enable goal conditioning and HER for introducing additional rewards. Without this augmentation, HER cannot be easily applied in a standard product MDP.\n\nWe will do our best to include Algorithm 1 in the final version of the paper.\n\n[8] Araki, Brandon, et al. \"The logical options framework.\" International Conference on Machine Learning. PMLR, 2021.\n\n[9] Alpern, Bowen, and Fred B. Schneider. \"Recognizing safety and liveness.\" Distributed computing 2.3 (1987): 117-126.\n\n## Questions\n\n> What is the main reason behind the sim2real success?\n\nThe sim-to-real success can be attributed primarily to the close alignment between the simulation and the real-world environment. The simulated setup used a state space and action space that were not highly affected by sensor noise, matched the real robot’s dynamics, and accurately modeled physical constraints such as the shelf. Training and evaluation were carried out entirely in this simulator.\n\nThis type of sim-to-real transfer is common in policy learning when the simulation is carefully constructed to reflect the real-world system.\n\n> Have you tried any of the baselines in this setting? If so, what was their success rate?\n\nBased on initial evaluation in the simulator, we were able to determine if trained policies were safe to deploy or not. The baselines did not perform well in the simulated environment, and therefore we did not believe it was appropriate to deploy them in the real world. \n\n> How do you pass the subgoal lists to the networks?\n\nThe subgoal list is processed by the networks according to how they appear in the boolean propositional statement $O(q)$ (defined in line 162) where $q$ is the agent’s current automaton state. Each goal is passed to a single-goal-conditioned value function module, and the output values for each goal are then combined according to min and max operations based on the “and” and “or” operators in $O(q)$ until a final value is obtained for the goal list. For more details, refer to the Appendix C Paragraph 1."}]

Author rebuttal:

Meta-review: The paper proposes Automaton-Constrained Q-Learning (ACQL), a reinforcement learning algorithm designed to satisfy Linear Temporal Logic (LTL) objectives in continuous domains. The key idea is to translate an LTL formula into a deterministic Büchi automaton (DBA) and then construct an augmented product constrained MDP (CMDP), in which the environment state is combined with the automaton state and automaton-derived subgoals. To address reward sparsity, ACQL employs goal-conditioned RL with Hindsight Experience Replay (HER), treating automaton subgoals as intermediate targets that densify learning signals. To address safety, the authors introduce a minimum-safety constraint over trajectories, rather than a discounted cumulative cost, which biases the learning toward avoiding unsafe actions in a more principled way. The paper provides a convergence proof, empirical validation on continuous-control domains, ablations, and a real-world robotic manipulation experiment where a 6-DOF robotic arm successfully executes LTL-specified tasks.

**Strengths**
ACQL makes a well-motivated and technically sound contribution by combining LTL-to-automaton translation, CMDP formalization, HER-based goal conditioning, and a trajectory-level safety constraint. This is a non-trivial synthesis of ideas from multiple areas. The use of HER with automaton-derived subgoals is a compelling way to mitigate reward sparsity, while the minimum-safety constraint is a conceptually strong alternative to standard cumulative costs. The theoretical contribution is also meaningful: the construction of the product CMDP and the convergence proof for the two-timescale Q-learning scheme are carefully developed. The experimental evaluation is convincing, with ablations clarifying the role of HER and safety constraints, and with validation extending beyond simulation benchmarks to a real robotic arm, which strengthens the practical relevance of the work.

**Weaknesses**
The paper's choice of baselines is a point of concern. It does not compare against several relevant LTL-based RL approaches—such as automata embeddings, experience replay method via counterfactual reasoning, and cycle experience replay—which are necessary for stronger positioning within the literature. The paper also lacks an analysis of how automaton complexity affects sample efficiency, a crucial factor for scaling to more complex specifications. Clarity can be improved in several places. First, the definition of subgoal lists is ambiguous, and the construction algorithm in the appendix appears somewhat ad hoc. It is not clear why the design is formalized as a list, especially since the representation passed to the neural network effectively encodes goals as Boolean combinations of subgoals via fuzzy logic. Second, the experiment does not clarify whether the approach naturally supports more general goal structures, such as conjunctions/disjunctions of goals or overlapping subgoals, which raises questions about extensibility. Lastly, the paper makes implicit assumptions about the goal space that are not formally stated. In particular, it assumes all propositions in $\text{AP}_\text{goals}$ are defined over the same set of state dimensions for goal-conditioned learning, which prevents handling cases where e.g. some propositions depend on positions while others depend on velocities.

During the rebuttal, the authors added a comparison with reward machines. However, this alone is insufficient; a broader set of relevant LTL-based RL baselines should be included for a fair and convincing evaluation. Overall, the paper presents a technically sound and well-motivated contribution at the intersection of LTL-based RL and safe RL, combining HER-based goal densification with a minimum-safety constraint in a product CMDP formulation. The meta-reviewer encourages the authors to improve the paper’s positioning within the literature and expand baseline coverage; in addition, the scalability and expressiveness limitations require clearer discussion. Addressing these points would significantly strengthen the work.
Decision: Accept (poster)