LTL-Constrained Policy Optimization with Cycle Experience Replay
Authors: Ameesh Shah
Cameron Voloshin
Chenxi Yang
Abhinav Verma
Swarat Chaudhuri
Sanjit A. Seshia
Venue: Accepted by TMLR ()

Abstract: Linear Temporal Logic (LTL) offers a precise means for constraining the behavior of reinforcement learning agents. However, in many settings where both satisfaction and optimality conditions are present, LTL is insufficient to capture both. Instead, LTL-constrained policy optimization, where the goal is to optimize a scalar reward under LTL constraints, is needed. This constrained optimization problem proves difficult in deep Reinforcement Learning (DRL) settings, where learned policies often ignore the LTL constraint due to the sparse nature of LTL satisfaction. To alleviate the sparsity issue, we introduce Cycle Experience Replay (CyclER), a novel reward shaping technique that exploits the underlying structure of the LTL constraint to guide a policy towards satisfaction by encouraging partial behaviors compliant with the constraint. We provide a theoretical guarantee that optimizing CyclER will achieve policies that satisfy the LTL constraint with near-optimal probability. We evaluate CyclER in three continuous control domains. Our experimental results show that optimizing CyclER in tandem with the existing scalar reward outperforms existing reward-shaping methods at finding performant LTL-satisfying policies.

Published in Transactions on Machine Learning Research (03/2025)
LTL-Constrained Policy Optimization with Cycle Experience Replay
Ameesh Shah" UC Berkeley
ameesh@berkeley.co edu
Cameron Voloshin"
cavolostinn@la..oo
Latitude AI
Chenxi Yang
cayyong 19 W0ttettas....... edu
UT Austin
Abhinav Verma Penn State University
vermo.@psu.cm edu
Swarat Chaudhuri
swarat@css www.wat.ecsommm edu
UT Austin
Sanjit A. Seshia UC Berkeley
sseshia@eecs sechhia@eecs.berkeeey. edu
Reviewed on OpenReview: https: //
// openreview. net/ forum? poUp2d4JTuu
Abstract
Linear Temporal Logic (LTL) offers precise means for constraining the behavior of rein- forcement learning agents. However, in many settings where both satisfaction and optimality conditions are present, LTL is insulficient to capture both. Instead, LTT-constrained policy optimization, where the goal is to optimize scalar reward under LTT, constraints, is needed. This constrained optimization problem proves difficult in deep Reinforcement Learning (DRL) settings, where learned policies often ignore the LTL constraint due to the sparse nature of LTL satisfaction. alleviate the sparsity issue, we introduce Cycle Experience Replay (CyclER), novel reward shaping technique that exploits the underlying structure of the LTL constraint to guide policy towards satisfaction by encouraging partial behaviors compliant with the constraint. We provide theoretical guarantee that optimizing CyclER will achieve policies that satisfy the LTL constraint with near-optimal probability. We evaluate CyclER in three continuous control domains. Our experimental results show that optimizing CyclER in tandem with the existing scalar reward outperforms existing reward-shaping methods at finding performant LTL-satisfying policies.
1 Introduction
Significant research effort has explored Linear Temporal Logic (LTL) alternative to Markovian reward
functions for specifying objectives for reinforcement learning (RL) agents Sadigh et al. 2014 Hasanboig
et al. 2018 Camacho el al. 2019 Wang et al., 2020 Vaezipoor el al. 2021 Alur el al. 2022 De Giacomo
et al. that are often not reducible scalar Markovian rewards (Abel al. 2021 Unlike typical reward functions,
2020 Voloshin et al. 2023). LTL provides a flexible language for defining objectives, or specifications,
objectives defined in LTL are composable, easily transferred across environments, and offer precise notion of satisfaction.

---

Published in Transactions on Machine Learning Research (03/2025)
LTL specifications and Markovian reward functions have been used separately in variety of RL settings, but few works consider both rewards and specifications in the same setting (Voloshin et al. 2022 The combination of the two is important: an LTL specification can define the meaning of achieving a task, and a reward function can be optimized to find the best way of achieving that task. For example, in robot motion planning, an LTL, specification can describe the waypoints a robot should reach and obstacles it should avoid, and a reward function can optimize for factors like energy consumption, stability of motion, and so forth.
This work considers the problem setting of RL-based reward optimization under an LTL constraint. This constrained learning problem be naturally formulated in an unconstrained form through a Lagrange-style relaxation (Le et al. 2019; Achiam et al. 2017) where the LTL constraint is represented by prozy reward function. Some versions of this proxy have been introduced in prior literature (Hasanbeig et al., 2020 Voloshin et al. 2023 Camacho et al. 2019). However, these proxy rewards are sparse and difficult to optimize. As a result, learned policies practice often end up ignoring the LTL constraint entirely and focus only on optimizing the reward function. A few existing works attempt circumvent this sparsity issue by considoring alternative temporal logics that provide denser reward signal (Krasowski al. 2023 Lavaei et al. 2020 2021) by limiting their approach to discrete state spaces that can be solved exactly (Voloshin et al. )022).
Gundana & Kress- Gazit
In this paper, we introducing a novel reward-shaping proxy for LTL called Cycle Experience Reploy (CyclER) that alleviates the reward-sparsity issue of previous LTL proxy rewards, allowing us to scale to continuous state and action spaces with an objective readily optimizable by deep RL (DRL) approaches. We briefly summarize the CyclER approach as follows. Given the (known) automaton structure representing an LTL objective, CyclER computes all possible infinite paths, or cycles, through the automaton that define accepting behaviors for our task. Then, when an agent collects finite episode of experience in the world, CyclER counterfactually reasons over that experience by considering how much progress it made through each cycle. The cycle that the agent progressed through the furthest is then used to shape LTL reward. We provide a visualization of this approach in Figure I
Under certain assumptions, CyclER maintains theoretical guarantees on LTL optimality that are competitive with state-of-the-art LTL proxy rewards (Voloshin et al. 2023). key advantage of CyclER is how it readily incorporates quantitative semantics (QS), popular technique for reward design in temporal logic that has yet to be extended to infinite-horizon LTL tasks. Our empirical results demonstrate CyclER's 's effectiveness during policy learning.
In summary, this paper makes the following contributions. We present a problem formulation for LTL- coistrained policy optimization in the presence of continuous spaces and function approximators for use deep RI.
We propose technique for this problem setting. CyclER, that alleviates the proxy reward sparsity issue and provides guarantees that ensure approximate optimality of LTL satisfaction.
Third, we introduce a new way to leverage quantitative semantics in LTL reward shaping. Lastly, we present promising experimental results using CyclER in I.TL-constrained optimization settings, outperforming existing approaches.
2
Problem Setting
2.1 Preliminaries
An atomic proposition is variable that takes on a Boolean truth value. We define an alphabet Σ as all possible combinations over a finite set of atomic propositions (AP); that is, Σ = 2AP For example, if AP = {a, b), then Y = (fa 6),((); (b), 0}. We will refer to individual combinations of atomic propositions, or prodicates, in Σ v.
Labeled MDPs We formulate our environment as a labelled Markov Decision Process M A. TM, do.7, y. r, LM), containing a state space S, an action space A, an unknown transition function, T S A > A(S), initial state distribution dg E ASS), a discount factor 0 < 7 < 1, reward function
2

---

Published in Transactions on Machine Learning Research (03/2025)
2
ry YB
4
CyclER
R
ryg
reward
reward %
Figure 1: Left: The Flald MDP and an example trajectory. Right: An LDBA for the LTL formula
& = ((FF()))(())&FF(( (G)))) (some edges omitted for readability); the accepting state coded in green. The CyclER method considers all accepting paths within an LDBA and selects the most reward-ful path for the trajectory shape LTL reward. Unlike previous approaches (Camacho al., 2019 Voloshin et al.
2023 CyclER offers dense reward, even without visiting the accepting state.
r: S A [Rmin Rmax]; and labelling function T.M SS + E. The labelling function returns which atomic propositions in our set AP are true for given MDP state.
As running example, consider the "FlatWorld" MDP in Figure the green dot) can move around the environment and visit different colored regions of interest. The agent is given a reward
| (left), where an agent (represented by
every time it visits one of the small purple regions. Our alphabet in Flat World is defined as AP (r: g, y), corresponding to whether the agent is the red, green, blue, or yellow region any point time.
Linear Temporal Logic (LTL) Linear Temporal Logic (Puulli 1977 is specification language that composes atomic propositions with logical and temporal operators to precisely define tasks. We use the symbol y to refer to an LTL task specification, also called an LTL formula.
In LTL, specifications are constructed using both logical connectives: not (-), and (&), and implics (+); and temporal operators: next (X), repeatedly/ahee always globally (G), eventually (F), and until (U). For more /llaa//loobbllllyyyyyyoooaooaaya
detail the exact semantics of LTL operators, see Baier & Katoen (2008).
As an example, let us demonstrate task specifications in the "Flat World" environment from Figure 1 (left). LTL can easily define some simple objectives, such as safety G(-b) (avoid the blue region), reachability F(g) (reach the green region), or progress (FF)) (reach the yellow, then the red region). We can also combine operators to bring together these objectives into more complex specifications, such as which instructs an agent oscillate amongst the red, yellow, and green regions
indefinitely while avoiding the blue region.
In order to determine the logical satisfaction of an LTL specification, we transform it into specialized automaton called Limil Delerminisläc Büchi Aulomalon (LDBA). See Sickert el al. (2016); Hahn el al. (2013): Kietínský et al. (0188) for details on how LTL specifications can be transformed into semantically equivalent LDBA.
E, More precisely, a (de-generalized) LDBA a tuple = (B, alphabet Σ of predicates that defines deterministic transitions in the automaton, a transition function 2 B (2 U)) > B, set of accepting states B*, and initial state b-1- An LDBA has separate deterministic and nondeterministe components B = BDUBN such that 8 C Bp, and for be Bp, x E Σ then 8 (b.x) C Bp. & is a set of "jump" actions, also known as epsilon-transitions. for b E Bx that transitions to BD without evaluating any atomic propositions. A path & = (bo, b1,...) is sequence of states in B reached through successive transitions under T not including the initial state b_1, as the labeling function L-M transitions the state of B by to be consistent with the initial state of the MDP.
with a set of states B, the
Definition 2.1 (Acceptance of E). We accept a path & (bo. b.....) if an accepting state of the Bücchi automaton is visited infinitely often by e.
3

---

Published in Transactions on Machine Learning Research (03/2025)
2.2 Problem Statement
We would like to learn a policy that produces satisfactory (accepting) trajectories with respect to given LTL formula while maximizing r, the reward function from the MDP, Before we define our formal problem statement, we introduce more notation:
Definition 2.2 (Product MDP). A product MDP synchronizes the MDP with an LDBA. Specifically, let M be an MDP with state space S S B. Policies over our product MDP space can be defined S + (AA), where our new set of actions combine (f((s, 6]) A(s) US, to include the jump transitions in B possible actions. We define the space of all possible policies as 11. The new probabilistic transition relation of our product MDP is defined as:
T TM (s,as, a b
T(s,b,,,
a a ( otherwise
(1)
A policy generates trajectorics r = ((su, by ao), (s1, b,, a1)....) in the product MDP. Define R(T) = Ei= 7'r(s;,a) as the total reward along a trajectory т.
Definition 2.3 (Trajectory acceptance). A trajectory is said to be accepting with respect to y (T |= 9, or " accepts r") if there exists some b 1 that is visited infinitely often.
II satisfies & with some probability P F pp] B. [-] Here, is an indicator variable that checks whether or not a trajectory T is accepted by 49 and MM is the distribution of trajectories induced by policy π in a product MDP M
Definition 2.4 (Policy satisfaction). A policy
Definition 2.5 (Probability-optimall policies). We will denote II the of policies that maximize the probability of satisfaction with respect to şo; that is, the policies that have the highest probability of producing accepted trajectory: II (x HP[p + o) max IP[m' }= +]}.
Our aim is to find a policy in the probability-optime set II that collects the largest expected cumulative discounted reward. We state this constrained objective formally as follows:
argmax By [R(T)]
(2)
For notational convenience, we will refer to the MDP value function as R2 = E, [((T)].
In certain cases, the probability-opting set of policies II" may be empty; consequently, solution to 2 may not exist. In section 3] introduce proxy objective with similar potential of non-existence and discuss how our ultimate optimization objective behaves in this setting.
To align with our intended applications towards deep RL, we consider stochastic, memoryless policies over the product MDP. Such policies are capable of capturing probabiity-optimall policies for a given LTL specification if an optimal policy exists (Bozkurt et al. 2020: Voloshin et al. 2022
3 LTL-Constrained Policy Optimization
Finding policy within II is, in general, not tractable: an LTL constraint yp is defined over infinite-length trajectories but policy rollouts in practice produce only finite-lentth trajectories (Yang et. al. 2022). We adopt eventual discounting (Voloshin et al. 2023), common approach in the existing literature which aims to optimiza a proxy value function that approximatos the satisfaction of y. Eventual discounting is defined as:
I = 1 (b. = {:
if (he E B²)
V=
E T~Me
Σ Cor
3
otherwise
where jr Ei (LTL(bb) counts how many times the set B has been visited (up to and including the current. timestep). Notably, eventual discounting does not discount based on the amount. of time between
4

---

Published in Transactions on Machine Learning Research (03/2025)
visits to accepting state. A policy that maximizes this eventual discounting reward is approximately probability-optimal with respect to yp when Tp: the discounting factor associated with yp, is selected properly (see Theorem 4.2 in Voloshin et al. (0033) for an exact bound).
As a result of eventual discounting, we can replace II" in objective 2 V. Let Vmax maXzen V be the maximal value.
with the set of policies that maximize
argmax " V =
[R
(4)
We now form the Lagrangian dual of objective 4
*² miny argmaxzen R2 +(V -Vaxx]] In theorem 3.2 we show that because only care about constraint- maximizing policies, there exists X E IR such that solving the inner maxinization of the Lagrangian dual must be constraint optimal for any fixed À > X*. Intuitively, the higher X is, the more our learned policy will account for Vz during optimization until the constraint must be satisfied. At that point, because wo are already achieving the maximum possible V,, any additional lift will only come from maximizing over the MDP value R, even we continue increase A. With this observation, we can form an unconstrained objective function from objective 4 to be the following:
π arg max R + AV TEll
where have dropped the dependence Viuxx since it is constant and fixed >> X*. We show that under certain assumptions, an exact value for X can be found to ensure that policy that maximizes eq. 5 will certainly maximize V
Assumption 3.1. There ezists positive nonzero gap > 0 between the value V₂ of policies in E II* and the vague policies that are not; that is, Vmax max
Theorem 3.2. Under Assumplion 3. for any choice of X > Buns - Bunin the solution to objective must be solution to objective See Appendir Section for the proof.
c(l->)
We note that Assumption 3.1 can be found in previous literature VVoloshin et al. 2023 and serves sufficient but not necessary condition for our results. We provide further analysis for the existence of Assumption 3.1 in Appendix Section
B.1
As brielly mentioned in Section 2 the probability-optimall set of policies with respect to may be emply. The same is true for our updated definition II* that contain policies that achieve Vmax- In the case of this non-existence, Assumption 3.1 does not hold, and policy that optimizes 3 the potential expense of R,, We provide an extended discussion of this consequence in Section B.2
will prioritize improving V,
Empirical Considerations. Since the conditions for Assumption 3.1 often unknown, there may not be verifiable way to know that that our learned policy is maximizing V Because of this, we will treat À as a tunable hyperparameter that allows a user to trade off the relative importance of empirically satisfying the LTL constraint. There are a number of strategies one can use to find an appropriate X: for example, one can iteratively increase À until a desired LTL reward is achieved. In our experiments, we show an example of this trade off, and notice that the trade off lessens in severity once exceeds a value that enables learning LTI-satisfying policies (table 2
4 Cycle Experience Replay (CyclER)
To distinguish between the MDP's s reward function and the exentusl-disccuuting proxy reward in 3 we write the MDP reward function r(x,a) a) as (MDP(s, a). In Deep RI. settings, we maximize objective using the reward function ( by, ar) = 7'TMDP(5t 0z) + Lbdrrir(bb...
However, optimizing objective 5 is challenging due to the sparsity of TLTL- FLTL is nonzero only when an accepting state in B is visited, which may require long, precise sequence of actions.
5

---

Published in Transactions on Machine Learning Research (03/2025)
Consider the FlatWorld MDP and LDBA in Figure [ The MDP's reward function incentivizes visiting the small purple regions in the world. Under TITI, a policy will receive no reward until it completes the entire task of avoiding blue and visiting the red, yellow, and green regions through random exploration. If TMDP is dense, a policy may fall into an unsatisfactory 'local optimum' by optimizing for TMDP it reccives carly during learning, and ignore VLTl entirely. In Figure 2 we see that a policy trained on "DUAl makes such an error.
We seek to address this shortcoming by automatically shaping FLTL so that a more dense reward for yp is available during training. Below, present our approach, which exploits the known structure of the LDBA IB and cycles within IB that visit accepting states.
4.1 Rewarding Accepting Cycles in I
By definition of LTL satisfaction (def. 2.3), trajectory must repeatedly visit an accepting state b' in an LDBA. In the context of the automaton itself, that means that an accepting trajectory will traverse an accepting path from the initial state to an accepting state, and then repeatedly traverse accepting cycles within B that contimually visit accepting states, Definition 4.1 (Accepting Initial Path (AIP)). An accepting initial path in B is set of valid transitions (b;; b,bb) (i.c., the predicate that transitions b; to b,) in B that starts at the initial state b-1 and ends at an accepting state b% E B"
Figure 2: Trajectories from un- shaped rDUAL (left) and CyclER rDUAL (right) for the formula G(F())&F(() & G(-b).
Definition 4.2 (Accepting Cycle (AC)). An accepting cycle in is a set of valid transitions (b,, v, by) in B that start and end at accepting states 0g bj E B
Our key insight is that we can use accepting paths and cycles in B to shape FLTL- Instead of only providing reward when an accepting state in B is visited (as per previous approaches e.g. VVooshhn et al. (2023)). )) we reward progress within an accepting path or cycle. In our example from fig [ if we reward each transition in the initial path (1, 2, 0} and the cycle with the same states, the agent would receive rewards for visiting the red region, then yellow, then green, then for returning to rod, and so on.
Multiple accepting paths and cycles may exist in B. The path and cycle that is used shape FL.TI cannot be picked arbitrarily, since they may be infeasible under the dynamics of the MDP. For example, the cycle {1,2, 0} in Figure ! cannot effectively shape FLTL because it is impossible to be both in the yellow and green regions at the same time.
4.2 Reward Shaping with CyclER
CyclER is a reward function that automatically selects paths and cycles to shape FLTI based on collected experience.
Definition 4.3 (Minimal AIP (MAIP).. A minimal accepting initial path for accepting state bg is an AIP that does not contain a subeycle for any node b, in the path where b, # bt- Definition 4.4 (Minimal AC (MAC)). A minimal accepting cycle e for accepting states bg and bj is AC that does not contain a subeycle for any node b, in the cycle where b, & (bt, b7].
We provide CyclER with all MAIPss and MACs in an LDBA using Depth-First Search with backtracking (see Appendix Algs. and Let P and C be the set of MAIPs and MACs, respectively.
We also maintain a frontier e of visited transitions B at each timestep a trajectory that ensures reward will only be given once per transition until an accepting state is visited. In particular, we set el(b,, v, 6;)] when a transition (bi, v, by) is taken and reset all when by B*. Policies that use CyclER observe 8, b, and e as their current state.
Now we describe the CyclER reward computation. We first collect a full trajectory 7 induced by My for a given policy π. Then, at each timestep 1 from 0 to |T| - 1, we compute re for every path in P if we have not
1 'Qur usage of the word "cycle" is a cycle in the traditional sense of graph search, but instead refers to paths that connect. two accepting states in B (allowing for "cyclical" acceptance).
6

---

Published in Transactions on Machine Learning Research (03/2025)
yet visited accepting state, or every eycle in C if we have. We will abuse notation slightly and use to refer to elements in either P or C:
di [el
if (b. Es) and e/b, L (M),), = =0
re(s, (ls,b,8,,B.c.
otherwise
This function rewards every transition taken in given c. In other words, when an agent "gets closer" to an accepting state by progressing along path or cycle, we reward that progress. Importantly, we do not reward transitions taken in given more than once per visit to accepting state. In other words, a trajectory that repeatedly takes transitions in but never reaches an accepting state b* will only receive reward for the first instance of each transition taken in c. To account for e of varying length, rewards are normalized by the length |c]-
If we visit an accepting state b* or reach the end of trajectory, we retroactively assign rewards to the timesteps that preceded this point, up to the most recent accepting state visit (if one exists). Assigned rewards correspond to the cycle with the highest total reward for that partial trajectory. Put simply, CyclER picks the 'best' cycle for a partial trajectory and uses to shape reward. Even if a trajectory does not manage to visit an accepting state, CyclER will still provide reward if it was able to take any transition along any MAIP. The CyclER algorithm is formally outlined in Algorithm
Algorithm 1: Cycle Experience Replay (CyclER)
Input: Trajectory 7, B",, cycles C, paths P, Labelling function L.M
Initialize matrix Re size max([C), (PI) ([F) - 1): Initialize TCydER to an array of size (TT 1);
Initialize j=
foreach t= ==,....,77! do
if j then
foreach Path p: P do Rcli, re St b441, pt)
else
foreach Cycle cs E do
Let us walk through an example of using CyelER to shape reward by referring to the specification ip and trajectory in the Flat MDP from Figure I Here, the agent produces a trajectory of length 4, indicated by the end of each line segment, starting from its initial state. The corresponding LDBA path for this trajectory & is (1, 3). Under the unshaped (non-CyelER) proxy reward defined in 3 no reward would be gained from this trajectory, as the accepting state of the LDBA is not visited. Instead, let us consider how CyclER shapes the reward for each transition in this trajectory. There are three MAIPs in this LDBA: {(1,ryg, 0)}, ((1, (2, yg, 0)}, and [(1,r, (2, 3), (3, y, 0)}. For each of these MAIPs, CyclER will retroactively assign rewards to each transition within the trajectory. Under the MAIP {(1, 0)}. no transitions will receive reward, as the predicate ryg is not achieved. For {(1,r, 2), (2, yg. 0)}, the transition to the second timestep of the trajectory will receive a reward of for visiting the red region. Lastly, for the MAIP {(1,r, 2), (2. g. 3), (3, y, 0)}, both the transitions to the second and fourth limesteps will receive a reward of 3. for visiting the red and green regions, respectively. Therefore, CyclER will choose to shape the trajectory's 's rewards using the MAIP {(1,r, 2). (2. g, 3), (3, y, 0)), as it results in the highest cumulative reward assigned to the entire trajectory.
I Reli,,]= (br, 81-1, be11, cr, ci) Set e(be, (s(+1), bet1] 1;
if b E B² or ++++=1110 |r| then
Select i argmax Ex Re(i.
foreach from j to t +++1 do
TCy]ER|("] Reli, [']
1=++1;
Set all e
return ToydRRi
We denote the rewards returned from Algorithm| 1 as TCydER FCyelER can be used in place of the unshaped TLTL in function 3 to provide more dense reward for r.
Theorem 4.1 (Informal). By replacing TLTL with TCyelER in 3 the solution to problem remains (approzi- mately) probability optimal in satisfying the LTL formula 4p See Appendir Lemma C. for the proof.
4.3 CyclER with Quantitative Semantics
A number of recent works have explored the usage of Quantitative Semantics (QS) to help shape rewards for
temporal logic tasks (Li al. 2017: Balakrishnan & Deshmukh 2019 Jothimurugan et al. 2021 Kalagarla
et al. 2021 Ikemoto& & Ushio 2022) QS defines set of rules for temporal logic which extend Boolean logic to
7

---

Published in Transactions on Machine Learning Research (03/2025)
operations over real values. Using QS, we can take real-valued signals from our atomic propositions z E AP, and compose them with the QS version of our logical connectives (&, and -) and temporal operators ((X), (G), (F), and (U)) to compute a real-valued signal for how close a trajectory comes to satisfying a specification. We will refer to this computation as the guantitative evaluation of a trajectory with respect to an LTL lask. The exact quantitative semantics of the alorementioned LTL operations are provided in Figure D of the Appendix.
Unfortunately, there are several shortcomings of "off-tho-shelf" usage of QS as reward function. Quantitative evaluation produces single value for entire trajectory, which makes credit assignment for individual transitions difficult. More pressingly, quantitative evaluation of a finite trace frequently produces values that do not correlate with visits to accepting states in IB, especially for LTL formulae with indefinite horizons or arbitrarily ordered sub-goals. Existing approaches have circumvented these issues by using QS for explicitly time-bounded temporal logics with simple tasks (Kalagarla et al. 2021 Balakrishnan & Deshmukh| 2019). or by considering fragments of LTL that can be reasoned about as finite sequences of ordered sub-tasks (Jothimurugan el. al., (021)) In what follows, we show that CyclER easily incorporates QS for more effective LTL reward shaping by considering each transition in B as independently evaluable sub-task.
We first define some notation. In order to use QS, we assign robastness measures (real-valued signals) fa la:& S + R to each atomic proposition I E AP, where æ is true when fa(s) 2 C2 (a constant threshold). We will follow standard practice and notate the quantitative evaluation of an LTL formula yp over a trajectory T as (T),), where vp is true when PT( > O. We also define a maximum and minimum for p as Pmax and Pmint respectively.
Now we explain how to incorporate QS into CyclER. At given state b in B, we can think of our sub-task as taking the next transition in the accepting path or cycle currently under consideration by CyclER. We need to only consider one transition at a time because CyclER reasons about each accepting path and cycle independently. Our approach to incorporating QS builds on this idea by rewarding quantitative progress towards taking the next. transition in path or cycle. Importantly, each transition v in BB associated with an atomic predicate, which can be quantitatively evaluated at individual states rather than entire trajectories (i.c., (s) S + R). If we move from state to s' in M, can evaluate how much closer are to satisfying the predicate of our next transition by laking the difference in quantitative evaluation between successive states: Ps(s') (s). This measure of progress is used to shape reward.
Specifically, our approach to incorporating QS uses the following reward function for a given cycle or initial path c. We use e(b to refer to the transition predicate in e with parent node b:
Papals'> Pap (s) if (b, (s'),, E e and elb. (M'))) 0]= = (emax Pmin
Fap Te L, 8. e), =
(7)
otherwise
We use Pmax and Puni to normalize the quantitative progress made towards taking a transition Reward function 7 acts direct substitute to function 0 in Alg. 1 to compute TCydER- Unlike function 6 function 7
allows for nonzero rewards to be given more than once per transition in an LDBA, allowing for dense reward even in LDBAs with few transitions.
In our experiments (section 5). we show that incorporating quantitative semantics into CyclER for shaping FLIl leads to improvement in empirical performance when compared to existing methods of using QS. We provide the full QS for LTL, along with additional explanation and examples for CyclER=QS in Appendix
5 Experiments
We demonstrate experimental results in several domains with continuous state and action spaces on LTT tasks of varying complexity. We seek to answer the following questions: (1) Does CyclER learn satisfactory policies
We note that the reward in fn. 7 most well-shaped when the robustness measures for all E AP are of similar scale, but make such assumptions for the sake of generality.
8

---

Published in Transactions on Machine Learning Research (03/2025)
and avoid ignoring FLTL in favor of "MDP? (2) Does policy that optimizes the dual reward formulation in "dUAl gain higher TMDP than a policy that only seeks to satisfy the LTL constraint? (3) How does the value of À in rDUAL affect the performance of the learned policy?
5.1 Experimental Domains and Tasks
In our experiments, we evaluate the efficacy of CyclER indefinite-horizon (w-regular) tasks expressible by LTL. We use environments where TMDP does not explicitly correlate with FLTI in order to effectively distinguish between policies that learn to only optimize TMDP and policies that learn to satisfy the LTL specification.
Flat World The World domain [1] is a two dimensional world with continuous state and action spaces. The agent's state, denoted by x, is updated by an action
The agent (denoted by green dot) starts via x' = x + a/10 where E R and E [0, 1]2. There exists a set of randomly generated purple 'bonus regions', which offer small reward when visited. We use the specification from Figure 1 as our LTT. task.
Env We use the Zones environment from the MuJoCo-based Safety-Gymnasiun suite of environ- ments (Ji et al. 2023). In this domain, a robot must navigate the environment, which includes four differently colored goal regions and 'hazard' areas that offer small negative reward. The robot receives an observation of lidar data that detects the presence of nearby objects at each timestep. The LTL task description instructs the agent oscillate amongst. visiting the four colored regions.
This domain is more challenging version of the Zones environment, where an agent must press a number of small buttons in larger space while avoiding cube-shaped 'gremlins' that move in a fixed circular path. The LTL task description instructs the agent to press two specific buttons infinitely often, while avoiding making contact with gremlins. Unlike the ZonesEnv, 'bonus' regions are scattered around the environment, offering a small reward if visited.
ButtonsEnv We use the Buttons environment, also from
5.2 Implementation Details and Baselines
We use entropy-regularized PPO (Schulman et al. 2017 with a Gaussian policy over the action space as our
policy class.
Although we are not aware of an existing approach that considers reward optimization under general LTL constraints for deep RL, we compare against number of existing reward methods for temporal logic-guided RL TLTL in our 7DUAL formulation. We use baseline policy trained using the LCER method (Voloshin et al, 2023), a state-of-the-art approach to RL for general LTL. that uses an unshaped reward with counterfactua experience replay to improve the sample efficiency of learning. Additionally, we compare against the LCER baseline, but trained only on the unshaped LTL reward function TLTL: in order to observe the performance of a policy that does not get 'distracted' during training by TMDP-
In the Zon and ButtonsEnv domains, where the dynamics are more complex, we define simple robustness measures for each atomic proposition and use the QS version of CyclER defined in section 4.3 Tn these enviromments, we compare against two additional baselines that also use QS for reward shaping and are computable for afinite-horizon LTL tasks: a ILTL-based reward (Li et al. 2017 and BHNR (Balakrishnan & Deshmukh 2019).
For each baseline, was chosen to be that which led to best performance (on unshaped FLTL, using TMDP as tie-breaker) from a hyperparameter sweep. The robustness measures used in these domains along with all hyperparameters used during training are available in Appendix G
5.3 Results
(1) Does CyclER learn satisfying policies and prevent ignoring FLTL? Yes our results demonstrate that CyclER achieves significant improvement in performance in satisfying the LTL task when compared to our baseline methods. In Figure we plot the learning curves for both the unshaped FITI. and (MDP- We
9

---

Published in Transactions on Machine Learning Research (03/2025)
World
ZonesEnv
ButtonsEnv
8" visits
TMDP
8 visits
TMDP
B" visits
TMDP
CyclER
2.0 0.5
45.3
1.8
-27.8 4.55
2.6
0.3
3..4
LCER
0.0 0.0
76.6
0.0 0.0
13.
0.0
188.:143.2
LCER, no TMDP
0.8 0.4
0.0
-.9
0.4
13.2 8.53
TLTL
0.0
2.2
0.0
9.6 6.7
BHNR
0.0 0.0
-0.8 - 0.6
0.0 1 0.0
35.8 + 7.9
Table 1: Reward average and standard deviation achieved on each domain with extended horizon. 5 visits identifies the average number of visits to accepting state in B achieved for trajectory from n, and TMDP refers to the average MDP reward collected during a trajectory.
Flat World
ZonesEna
ButtonsEnv
CyclER
2.0
CyclER
24
CyclER
LCER
LCER
LCER
MDP)
LCER MDP)
LCER MDP)
Unvhhppd Rewand
TLTL
TLTL
BHNR
BHNR
0.4
2.4
0.2
0.3
0/2
CyclER
2
175
CyclER
LCER
LCER
150
LCER
LCER (no MDP)
LCER (no MDP)
LCER (no MDP)
-17
NDP nonurd
BHNR
BHNR
-20
-35
Timastap (xleb)
Timestace (xled]
Figure 3: Training curves showing unshaped FLTL (top) and TMDP (bottom) performance averaged over 5 random seeds. Each point the mean of 10 stochastic policy rollouts.
record the (stochastic) performance of the best policies found during training on an extended horizon to enable repeated visits to the accepting state, and present the results (averaged over 50 rollouts) in Table 1
We find that unshaped rewards (LCER) quickly ignore FLTT in most trials. From Table 1 we see that the LCER baseline even without TMDP was not able to accomplish the LTL task as consistently as CyclER, even when successful in visiting accepting state. This implics that reward shaping is critical for LTL- guided RL even in settings where FMDP is present. In ZonesEnv and ButtonsEnv, the TLTL and BHNR baselines, which are not suited to infinite-horizon tasks with multiple unordered subgoals, learned behavior that optimized their respective QS-shaped LTL rewards but did not correlate with task satisfaction (zero FLIl achieved in Figure 3). CyclER with QS, on the other hand, quickly learned to achieve the tasks in these two domains. Most meaningfully, CyclER able to repeatedly visit the accepting state all domains (as evidenced by Table D. demonstrating that our technique enables consistent-behavinng policies that can indefinitely traverse accepting cycles. We additionally provide qualitative analysis of learned behavior in the Flat World domain in Appendix D
(2) Does optimizing /DUAL improve TMDP? To evaluate this question, we conducted an ablation study where we trained a CyclER-based policy in the Flat World domain, making it completely unaware of rMDP, and then evaluated its performance to observe if the rDUAL formulation led to a nontrivial difference in behavior between policies. We found that the opptiiiig CyclER policy visited B* an average of 2.0 times (std. dev. 0.3) and achieved an MDP reward of 45.3 (std. dev. 8.5), and the FLTL-only policy visited B an average of of 2.2 times (std. dev. 0.4) and achieved MDP reward of 27.4 (std. dev. 0.7). Optimizing
10

---

Published in Transactions on Machine Learning Research (03/2025)
'DUAL does lead to improvement in PMDP; albeit at the potential cost of LTL satisfaction. We provide qualitative comparison of the two learned policies in Appendix D
(3) How does varying À affect the resulting policy? In Table 2 we
report results from a study where we vary the value of in rDUAL for the
Flat World
Forld domain experiment. We observe, as expected, a tradeoff the performance of LTL satisfaction and TMDP as À increases. However, we
B* visits
PMDP
A 100
0.0 + 0.0
62.7 4.36
notice that the tradcoff diminishes once a value for À is reached that enables
A 200
0.0 2.0
69.6 4.1
LTL-satisfying behavior. This supports our intuition that À can effectively be used as a hyperparameter to trade off the empirical performance of
300
2.0
37.2 = 9.0
A 400
2.1 34.3 - 7.3
LTL satisfaction and the MDP reward achieved by a policy.
Table 2: Performance results for
CyclER with differing A.
6 Related Work
Our work falls under the broad umbrella of specification-guided approaches to gerrect-by-constuuttiin machine learning (Seshia et al., 2022). with a. particular focus on RL.
Temporal Logic-Constraine Policy Optimization. Previous work has explored cost-optimal control under linear temporal logic constraints with known dynamics (Ding et al., 2014 Cai et al. 2021 More
recently, interest has emerged in RL-based approaches to logic-constrained policy optimization. Voloshin et al. (202) provides an exact solution method for policy optimization under general LTL constraints in discrete settings where the dynamics are unknown by assuming a lower bound on transition probabilities in M. Other works focus on Signal Temporal Logic (STL. and are either designed for discrete spaces (Kalagaria ct al.) 2021) or lack guarantees (Ikemoto & Ushio 2022). Our CyclER- QS method can be viewed as an approach designed for subset of STL,, with improved performance by our leveraging of the LDBA during policy learning.
RL with Temporal Logic Objectives. In contrast to settings with both temporal logic constraints and reward functions, a significant amount of work has been devoted to developing RL approaches with temporal logic specification(s) as the lone objective. Early efforts focused primarily on using Q-learning-styr methods
over angmentations of M (Sadigh et al.]
[0144 Aksaray et al.] 2016 Venkataraman et al.) 2020 Cai et al.,
2021). Subsequent works (Hasanbeig al.
2020 Toro Icarte et al. 2022 Camacho et al.) 2019 Jothimurugan
ct al. 2019) extend temporal logic-guided RL to deep RL settings In developing the thcoretical limitations of temporal-logic guided RL, (Yang et al.
2022 Alur et al. 2022) show that guarantees on RL for LTL
cannot in general be made. To obtain (approximate) guarantees on learning, existing works have made
assumptions on the environment dynamics (Fu & Topcu 2014 Voloshin et al.
2022
Wolff et al. 2012) or
finitized the policy's 's horizon through discounting or recurrence time (Alur et al.]
2023
Perez ct al. 2023). In
continuous spaces, prior works provide guarantees that the optimal policy under a proxy objective will salisfy
the original logical specification of interest (Voloshin et al.] 20233] Hasanbeig et al.
2020
Jothimurugan et al.
2021 Camacho et al.) 2019), similar to the guarantees made in our work.
To handle longer-horizon specifications, previous endeavors proposed compositional RL approaches that leverage the DAG-like structure for finitary fragments of temporal logic (Jothimurugan et al. 2021 Bonassi
et al. 2023). Other works take multi-task RL approach that learns subtasks, which allows for the completion
of cortenned-horiizon tasks and unseen tasks over the same AP set (Vaezipoor et al. 2021 Qiu et al. 2023
León et al. 2022 Liu et al. 2022). ) An extensive body of work uses quantitative signals to provide denser
feedback for temporal logic objectives that aids policy learning in longer-horizon task settings Li et al. 2017
Balakrishnan & Deshmukh 2009 Ikemoto & Ushio 2022); Krasowski et al. (0233 These quantative signals.
which are often captured in Signal Temporal Logic, are also used by our QS approach introduced in section However, the usage of these quantitative signals leads to a number of pitfalls in deep RL that CyclER is able
to avoid, as discussed in section 4.3 and Appendix D More recent. work considers problem settings where there is uncertainty in an agent's 's knowledge of atomic propositions and proposes a belief based approach to policy learning in this sotting (Li et al., 2024). Our approach able handle indefinite-horizon specifications for single tasks and we see the integration of our reward shaping into both multi-task frameworks and noisy environments as exciting directions for future work.
11

---

Published in Transactions on Machine Learning Research (03/2025)
Constrained Policy Optimization. The broader constrained policy optimization works mostly relate to the constrained Markov Decision Process (CMDP) framework (Te et. al.) 2019 Achiam et al. 2017 A Altman 2021), which enforce penalties over expected constraint violations rather than absolute constraint violations. In contrast, our work aims to satisfy absolute constraints in the form of LTL.
7 Conclusion
This paper proposes a novel approach to finding policies that are both reward-maximal and probability-optimal with respect to an I.T,, constraint. Specifically, we introduce CyclER, an experience replay technique that automatically shapes the LTL proxy reward based on cycles within Büchi automaton, alleviating sparsity issue that often plagues LTL-driven RL approaches. CyclER enables LTL-constrained policy optimization in cont cont inuous spaces using function approximators. We extend CyclER to effectively use quantitative semantics for full LTL and demonstrate its success empirically.
There are numerous directions for future work. For example, the reward shaping idea behind CyclER can be extended to other classes of logical specifications, such as Reward Machines (Toro Icarte et al. 2022 We are also interested in applying CyclER, accolcrate learning in multi-task LTL scttings, such as (Vezzppor et al. 2021 Qiu et al. 2023).
Acknowledgments
The authors would like to thank Adwait Godbole, Federico Mora and Niklas Lauffer for their helpful foedback. This work was supported in part by NDSEG Fellowship (for Shah), ONR Award No. N00014-20-1-210 DARPA contract FA8750-233 -3----00--- C-0080 (ANSR), C3DTI, Toyota and Nissan under the iCyPhy center, and by NSF grant 1545126 (VeHICaL).
References
David Abel, Will Dabney, Anna Harutyunyan, Mark K Ho, Michael Littman, Doina Precup, and Satinder Singh. On the expressivity of markov reward. In Advances in Newral In- formation Processing Systems, 2021. URL httpss//pproceeeinggs itwpeeedddnnnnnnnnnieeeeeee https/ccpaapp/////111000 40910115440110444999/7/111422222 P.f
Joshua Achiam, David Held, Aviv Tamar, and Pieter Abbeel. Constrained policy optimization. In International conference on machine learning, pp. 22-31. PMLR, 2017.
Derya Aksaray, Austin Jones, Zhaodan Kong, Mac Schwager, and Calin Belta. Q-learning for robust satisfaction of signal temporal logic specifications. In 55th IEEE Conference on Decision and Control, CDC 2016, Las Vegas, NV. USA, December 12-14, 2016, pp. 1565-65700 IEEE, 2016. doi: 10.1109/CDDC22016.77990 URL https:://oi. org/ 10. 1109/CDC..CC. 2 7799279
Fitan Altman. Construined Markoe decision processes. Routledge, 2021.
Rajeev Alur, Suguman Bansal, Osbert Bastani, and Kishor Jothimurugan. A framework for transforming spec- ifications in reinforcement learning. In Hean-Françoii Raskin, Krishnendu Chatterjee, Laurent Doyen, and Rupak Majumdar (eds.), Principles of Systems Design Essays Dedicated to Thomas A. Henzinger on the Occasion of His 60th Birthday, volume 13660 of Lecture Notes in Computer Science, pp. 604 624. Springer, 2022. doi: 10.1007 (00007997---0000 02-003311223--20 29. URL https:://oi..oo org/10 1111111110077778111 -31--33112222222222
Rajeev Alur, Osbert Bastani, Kishor Jothimurugan, Mateo Perez, Fabio Somenzi, and Ashutosh Trivedi. Policy synthesis and reinforcement learning for discounted LTT. In Constantin Enea and Akash Tal (eds.), Computer Aided Verification 35th International Conference, CAV 2023, París, France, July 17-22, 2023, Proceedings, Part I, volume 13964 of Lecture Noles in Computer Science, pp. 415 435. Springer, 2023. doi: 10.1007 9711999778---11-7776------- 21. URL
Christel Baier and Paestr Katoen. Principles of model checking. The MIT Press, Cambridge, Mass, 2008. ISBN 022449-..
12

---

Published in Transactions on Machine Learning Research (03/2025)
Anand Balakrishnan and Jyotirmoy V. Deshmukh. Structured reward shaping using signal temporal logic specifications. In 2019 IEEE/RO /RSJ International Conference on Intelligent. Robols and Systems, IROS 2019, Macau, SAR, China, November 3-8, 2019, pp. 3481 3486. LEEE, 2019. doi: 10.109/IR0044099.2001 8968254. URL htttps://di..og: 10. 100111109RRRR IROS40897
Luigi Bonassi, Giuseppe De Giacomo, Marco Favorito, Francesco Fuggitti, Alfonso Emilio Gerevini, and Enrico Scala. Planning for temporally extended goals pure-past linear temporal logic. In Sven Koenig, Roni Stern, and Mauro Vallati (eds.), Proceedings of the Thirty Third International Conference on Automated Planning and Scheduling, July 8-13, 2023, Prague, Czech Republic, pp. 61-69. AAAI Press, 2023. doi: 10. 10.1609/TCAPS. V33I 27179. URL
27179
Alper Kamil Bozkurt, Yu Wang, Michael M Zavlanos, and Miroslav Pajic. Control synthesis from linear temporal logic specifications using model-free reinforcement learning. In 2020 IEEE International Conference on Robotics and Automation (ICRA), pp. 11845-10355. IEEE, 2020.
Mingyu Cai, Shaoping Xiao, Zhijun Li, and Zhen Kan. Optimal probabilistic motion planning with potential infeasible LTL constraints. IEEE Transactions on Automatic Control, 68(1):301 316, 2021.
Alberto Camacho, Rodrigo Toro Icarte, Toryn Q Klassen, Richard Valenzano, and Sheila A. McIlraith. LTL and beyond: Formal languages for reward function specification in reinforcement learning. In Proceedings of the Stuenly-Eighll International Joinl Conference Artificial Intelligence, IJCAT-19, pp. 6065 6073. International Joint Conferences on Artificial Intelligence Organization, 7 2019. doi: 10.24963 10.24963/jjcai 201.aa.00099/8000 URL https://doi.org: org/ 10. 24963/1jcas 2019/840
Giuseppe De Giacomo, Marco Favorito, Luca Iocchi, Fabio Patrizi, and Alessandro Ronca. Temporal Logic Monitoring Rewards via Transducers. In Proceedings of the 17th International Conference on Principles
of Knowledge Representation and Reasoning, pp. 860 870, 9 2020. doi: 10.24963/kr. 20200//8... URL https://doi..rr:: 10. 1rg.o//93/r//0.. 2020/89
Xuchu Ding, Stephen L. Smith, Calin Belta, and Daniela Rus. Optimal control of markov decision processes with linear temporal logic constraints. IEEE Transactions on Automatic Control, 59(5):1224412)) May 2014. ISSN 0018-9286, 1558-2523.
doi: N0.1109/TAC.2014.22 22981433..
Alexandre Luret-Lutz, Etienne Renault, Maximilien Colange, Florian Renkin, Alexandre Gbaguidi Aisse, Philipp Schlehuber-Caissin 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 Proceedings of the 34th International Conference on Computer Aided Verification (CAV'22), volume 13372 of Lecture Notes in Computer Science, 9.
pp. 174 187. Springer, August 2022. doi: 1110007977---031-11
Georgios E. Fainckos and George J. Pappas. Robustness of temporal logic specifications for continuous- -4911, 2009, doi:
time signals. Theor. Comput. Set., 021 https://doi... orl. orgg//..111//............
URL
Jie Fu and Ufuk Topcu. Probably approximately correct MDP learning and control with temporal logic constraints. In Dieter Fox, Lydia E. Kavraki, and Hanna Kurniawati (eds.). Robotícs: Science and Systems X, University of California, Berkeley, USA, July 12-16, 2014, 2014. doi: 10.15607/RSS.2211..2 wrggrrss0/p3333 html
URL
David Gundana and Hadas Kress-Gazit Event-based signal temporal logic synthesis for single and multi- robot tasks. IEEE Robotics Autom. Lett., 6(2):3687-3694, 2021. doi: 200.0//LRA.22213062222222 URL 3064220
https: wttp//0..1199/111
Ernst Moritz Hahn, Guangyuan Li, Sven Schewe, Andrea Turrini, and Lijun Zhang. Lazy probabilistic model checking without determinisation. arXiv preprint 1rXiv:1311.2922 2013.
Mohammadhosein Hasanbeig, Alessandro Abate, and Daniel Kroening. Logically reinforcement learning, 2018. URL htt.:ttss////r...oo///bbba/ 08099
13

---

Published in Transactions on Machine Learning Research (03/2025)
Mohammadhosein Hasanbeig, Daniel Kroening, and Alessandro Abate. Deep reinforcement learning with temporal logics. In International Conference on Formal Modeling and Analysis of Timed Systems, pp- 1-22. Springer, 2020.
Junya Ikemoto and Toshimitsu Ushio Deep reinforcement learning under signal temporal logic constraints using lagrangian relaxation. JEEE Access, 10:114814-11488 2022. doi: 10.1109/ (0.1109/ACCESS, ACCESSS.022.32118/ URL https://doi. owg/10....... 1.1109//ACEESS 2022. 32182266
Jiaming Ji, Borong Zhang, Jiayi Zhou, Xuchai Pan, Weidong Huang, Ruiyang Sun, Yiran Geng, Yifan Zhong, Juntao Dai, and Yaodong Yang. Safely-gymnasium: unified safe reinforcement learning benchmark. arXiv preprint arXiv:2810.1220 2023.
Kishor Jothimurugan, Rajeev Alur, and Osbert Bastani. A composable specification language for reinforeement learning lasks. Advances in Newral Information Processing Systems, 32, 2019.
Kishor Jothimurugan, Suguman Bansal, Osbert Bastani, and Rajeev Alur. Compositional reinforcement learning from logical specifications. In Marc' Aurelio Ranzato, Alina Beygelzimer, Yann N. Dauphin, Percy Liang, and Jennifer Wortman Vaughan (eds.), Advances in Neural Information Processing Systems 34: Annual Conference on Neural Information Processing Systems 2021, NewrIPS 2021, December 6- 14, 2021, virtual, pp. 10026 10039, 2021. URL https://proceedings htw.:pooocediiggg...rrpppsp nwwripe..p.... wwtppcpr/e/////////// 2atrr//22//aaaaaae /hash/ html
Krishna C. Kalagarla, Rahul Jain, and Pierluigi Nuzzo. Cost-optimal control of markov decision processes under signal temporal logic constraints. In 2021 Seventh Indian Control Conference (ICC), pp. 317 312-322, 2021. doi: 0000//CCC54144.221.999990
Hanna Krasowski, Prithvi Akella, Aaron D. Ames, and Matthias Althoff. Safe reinforcement learning with probabilistic guarantees satisfying temporal logic specifications in contimuous action spaces. In 62nd IEEE Conference Decision and Control, CDC 2023, Singapore, December 13-15, 2023, pp. 4372 4378. IEEE, 2023. doi: B0.1009/CDC49953.2222 2TE0499753.2222133833330 URL http::ttttti.orrreeeeet 10383601
2023
Jan Křetínský, Tobias Meggendorfer, and Salomon Sickert. Owl: library for w-words, automata, and LTL. In International Symposium on Automated Technology for Verification and Analysis, pp. 543-550. Springer, 2018.
Abolfazl Lavaci, Fabio Somenzi, Sadegh Soudjani, Ashutosh Trivedi, and Majid Zamani. Formal controller synthesis for continuous-space mdps via model-free reinforcement learning. In 11th ACM/IEEE International Conference on Physical Systems, ICCPS 2020, Sydney, Australia, April 21-25, 2020, pp. 98 107. IEEE, 2020. doi:
202.08804..20000000.... URL httL:httss///ee //op::://doi..o 1ttp://.......01...1111///////// 10w.11109/ICCPSS4BE 2020 00017
Hoang Le, Cameron Voloshin, and Yisong Yue. Batch policy learning under constraints. In International Conference on Machine Learning, pp. 3703-3712 PMLR, 2019.
Borja G. León, Murray Shanahan, and Francesco Belardinelli. In a mutshell, the human asked for this: Latent goals for following temporal specifications. In The Tenth International Conference on Learning Represenlations, ICLR 2022, Virtual Event, April 25-29, 2022. OpenReview.ned 2022. URL https: //openreview //openrerieew.et//foorrr http://oruundddrUUUmSSCCCCCCC
Andrew C. Li, Zizhao Chen, Toryn Q. Klassen, Pashootan Vaezipoor, Rodrigo Toro Icarte, and Sheila A. McIlraith. Reward machines for deep RL in noisy and uncertain enviromments. CoRR, abs abs/2400 221220006210 2024. doi: 10.48550/ARB, ARXIV 2406.00120. URL https:://oi. wtt.://////.....//////.//../
Xiao Li, Cristian-Toan Vasile, and Calin Belta. Reinforcement learning with temporal logic rewards. In 2017 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), pp. 3834-3839. IEEE, 2017.
14

---

Published in Transactions on Machine Learning Research (03/2025)
Jason Xinyu Liu, Ankit Shah, Eric Rosen, George Konidaris, and Stefanie Tellex. Skill transfer for temporally- extended task specifications. CoRR, hass/2206.5500 2022. doi:
URL
https://doi.org// http///...rr///...////////////// (18550/arXiv.200 2206. 2000000066666662
Oded Maler and Dejan Nickovic. Monitoring temporal properties of continuous signals. In Yassine Lakhnech and Sergio Yovine (eds.), Formal Techniques, Modelling and Analysis of Timed and Fault- Tolerant Systems, Joint International Conferences on Formal Modelling and Analysis of Timed Systems, FORMATS 2004 and Formal Techniques in Real- Time and Fault-Tolerant Tolerant Systems, FTRTFT 2004, Grenoble, France, September 22-24, 2004, Proceedings, volume 3253 of Lecture Notes in Computer Science, pp. 162-166. Springer, 2004. doi: 10. 00007/978-3-285 540-30400---000 12. 12. URL https://doi..... www.o....oo////. 111////001000777----500000000000
Mateo Perez, Fabio Somenzi, and Ashutosh Trivedi. A PAC learning algorithm for LTL and omega- regular objectives in mdps. CoRR, abs/2330.12228, 2023. doi: 10.48550/ARXII 231.ARXXXI1221112266 2310.12248. URL
https://doi.org: http:///0...ogg/000.6.66///2/221 2310. 12248
Amir Pnueli. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science (sfes 1977), pp. 46-57. ieee, 1977.
Wenjie Qiu, Wensen Mao, and He Zhu. Instructing goal-conditioned reinforcement learning agents with temporal logic objectives. In Alice Oh, Tristan Naumann, Amir Globerson, Kate Saenko, Moritz Hardt, and Sergey Levine (eds.), Advances in Neural Information Processing Systems 36: An- wual Conference on Newral Information Processing Systems 2023, NeurIPS 2023, New Orleans, LA, USA, December 10 16, 2023, 2023. URL http::/papers. nips wwtppcppppatiiieeeee www.fffleeppppeeee paape//023//aas// 7b3546994444bebb7edd1beeee 16ace5cc Abstract- htmll
Dorsa Sadigh, Eric S Kim, Samuel Coogan, S Shankar Sastry, and Sanjit A Seshia. A learning based approach to control synthesis of markov decision processes for linear temporal logic specifications. In 53rd IEEE Conference on Decision and Control, pp. 1091-1096. IEEE, 2014.
John Schulman, Filip Wolski, Prafulla Dhariwal, Alee Radford, and Oleg Klimov. Proximal policy optimization algorithms. CoRR, ftss/177..0631,, 2017. URL http://arxiv wwwg wwtp//os//////////// attaaab///0100000 063447
Sanjit A. Seshia, Dorsa Sadigh, and S. Shankar Sastry. Toward verified artificial intelligence. Communications of the ACM, 65(7):46-55, 2022.
Salomon Sickert, Javier Esparza, Stefan Jaax, and Jan Křetínský. Limit-deterministic büchi automata for linear temporal logic. In Swarat Chaudhuri and Azadeh Farzan (eds.), Compuler Aided Verification, pp. 312 332, Cham, 2016. Springer International Publishing. ISBN
Rodrigo Toro Icarte, Toryn Q. Klassen, Richard Valenzano, and Sheila A. Mcllraith. Reward machines: Exploiting reward function structure in reinforcement learning. J. Artif. Int. Res., 73, may 2022. TSSN 1076-9757. doi: 10. 1...1////.....1///////.
URL
1.
Pashootan Vaezipoor, Andrew C. Li, Rodrigo Toro Tearte, and Sheila A. Mellraith. I.TL2Actio:: Generalizing LTL instructions for multi-task RL. In Proceedings of the 38th International Conference on Machine Learning, JCML, volume 139 of Proceedings of Machine Learning Research, pp. 10497- 10508, 2021. URL http://proceedings. mmr.iinnnmm.......mmmmmm..m.mm.. pttes///33//vacccprra.... html
Harish K. Venkataraman, Derya Aksaray, and Peter Seiler. Tractable reinforeement learning of signal temporal logic objectives. In Alexandre M. Bayen, Ali Jadbabaie, George J. Pappas, Pablo A. Parrilo, Benjamin Recht, Claire J. Tomlin, and Melanie N. Zeilinger (eds.), Proceedings of the 2nd Annual Conference on Learning for Dynamics and Control, L4DC 2020, Online Event, Berkeley, CA, USA, 11-12 June 2020, volume 120 of Proceedings of Machine Learning Research, pp. 308 337. PMLR, 2020. URL hhtml
http://proceedingg .mw.ingg.........m.............. mlr.
Cameron Voloshin, Hoang Minh Le, Swarat Chaudhuri, and Yisong Yue. Policy optimization with linear temporal logic constraints. In Alice H. Oh, Alckh Agarwal, Danielle Belgrave, and Kyunghyun Cho (eds.), Advances in Neural Information Processing Systems, 2022. URL https://openreviie http://ppaarvvvooo.oee//rrrrrcc yZcPRIZEWDG
wwt:ffrummidd
15

---

Published in Transactions on Machine Learning Research (03/2025)
Cameron Voloshin, Abhinav Verma, and Yisong Yue. Eventual discounting temporal logic counterfactual experience replay. Tn Andreas Krause, Emma Brunskill, Kyunghyun Cho, Barbara Engelhardt, Sivan Sabato, and Jonathan Scarlett (eds.), International Conference on Machine Learning, 1CML 2023, 23-29 July 2023, Honolulu, Hawaii, USA, volume 202 Proceedings of Machine Learning Research, pp. 35137-35150. PMLR, 2023. URL htttps://proceeding wem.mmlr..ess.e wttpprree//2222/oooooo222222 .tml
Chuanzheng Wang, Yinan Li, Stephen L Smith, and Jun Liu. Continuous motion planning with temporal logic specifications using deep neural networks. arXiv preprint arXiv:2004.02610, 2020.
Eric M. Wolff, Ufuk Topeu, and Richard M. Murray. Robust control of uncertain markov decision processes with temporal logic specifications. In 2012 TEEE 51st IEEE Conference Decision and Control (CDC), рp. 3372 3379, 2012. doi: Ww.1109/CDC.202...00
Cambridge Yang, Michael L. Littman, and Michael Carbin. On the (in)tractability of reinforcement learning for LTL objectives. In Lud De Raedt (ed.), Proceedings of the Thirly-Firss International Joinl Conference Artificial Intelligence, IJCAI-22, pp. 3650 3658. International Joint Conferences Artificial Intelligence Organization, 7 2022. doi: 10.24963 1//66//jje /ijeai. 2022/0022222 /07.. URL http://///b...oog00022/99///////
2022/507
Main Track.
16

---

Published in Transactions on Machine Learning Research (03/2025)
Contents
Introduction
1
2
Problem Setting
2
Preliminaries
2
2.2
Problem Statement
4
UTL-Constrained Policy Optimization
4
Cycle Experience Replay (CyclER)
5
Rewarding Accepting Cycles
4.2
Reward Shaping with CyclER
6
4.3
CyclER with Quantitative Semantics
7
Experiments
8
5.1
Experimental Domains and Tasks
9
5.2
Implementation Delails and Baselines
9
Results
Related Work
11
Conclusion
12
Limitations
18
B Proof for Theorem 3.2
B.1 On the existence of Assumption 3.1
18
B.2 On the existence of solution to 4
19
C Proof for Thcorem 4.1
19
D Additional Experimental Results
21
E Quantitative Semantics for LTL
23
F Additional Algorithmic Details
25
F. 1 Finding Minimal Accepting Cycles and Accepting Initial Pat
25
G Additional Experimental Details
25
17

---

Published in Transactions on Machine Learning Research (03/2025)
A Limitations
The success of CyclER is ultimately limited to the quality and achievability of the atomic propositional variables in a given environment. If robustness measures are not available and a task specification has relatively few variables that are difficult to satisfy, CyclER will not provide significant improvement over existing unshaped LTL reward proxies. For example, the specification F(G(=)) with no robustness measure for will offer the same reward under CyclER and existing methods. When robustness measures are available, it is important that measures for each variable in the set AP are of similar scale, so that the QS-shaped rewards do not vary highly across different transitions in B. The issue of needing similar scale for robustness measures is well-known in the temporal logic literature and is an open direction for future work Balakrishnan Li et al. (2017).
& Deshmukh 2019
Although we show that the performance of policy learning is somewhat robust to À in our formulation of rDUAL, we do not have a systematic way of finding an appropriate value for À beyond traditional hyperparameter search methods. We see an interesting opportunity for future work to intelligently search for À based on the desired FLTL and FMDP of user.
The CyclER approach incurs computational overhead by (1) computing all possible cycles prior to policy learning and (2) keeping track of all potential reward values for each cycle for each trajectory stored in an agent's replay buffer. We did not observe a significant slowdown or memory increase in our experiments as a result of this overhead. We ackuowledge that in complex specifications with a large number of cycles this overhead may become meaningful.
B Proof for Theorem 3.2
Proof. Consider two policies: (1) π E II \ II",, which does not achieve Viaax (2) II", achieving Vmax- Let Rmax and Rmin be upper and lower bounds the maximum and minimum achievable single-step reward in M, respectively. Evaluating objective 5 for both of these policies satisfies the following series of inequalities:
(o) Rmin + A(V +C)
-
(b) Rmax XV
(e) 2 Rr + AV
R₂ + AV
where (a) follows from assumption 3.1 and bounding the worst-case MDP value, (b) follows from selecting
À >> Rmax Ramm <(I-)) (= X*), (c) follows since the highest MDP value achievable by must be upper bounded by
the best-case MDP value.
As a consequence of (a (a-c) c)
that policies achieving Vmax are preferred by objective 5 Consider n' E II", the solution to objective 5 Thus, since n² E II,, then x¹ must also achieve V.- V Vmax. Therefore, in comparing objective 5 for both n² and # it follows immediately that Rx- 2 R2 since π" is optimal for
objective 5 Since the choice of is arbitrary, we have shown that nt is also a solution to objective
B.1 On the existence of Assumption 3.1
If we are restricted to stationary policies and the space of policies 11 is finite, then assumption 3.1 will always hold. A finite space of policies can be enumerated over, and we can take the difference between the optimal and next-best policies to find e. As an example, consider a toy MDP with a continuous, 1-dimensional state space [0, 1] and continuous, 1-dimensional action space [0, 1], where the transition function determines the next state as the agent's action, i.e. T'M(s (s,a, s') = a. Suppose we are given a task specification G(F(1)). Under this specification, the agent will receive reward of 1 every time it outputs 1, and 0 otherwise.
Consider a finite-sized policy class II of just two deterministic policies: To that only outputs 0, and m that only outputs 1. Here, assumption 3. holds even in this continuous space.
However, assumption 3.1 is not limited to just finite-sized policy classes. Consider an infinite-sized II, where one policy in II, called n²" always outputs 1, and all other policies are Gaussian policies with = 0.0001 and μ uniformly sampled from the interval [o, 0.0001]. Here, even when II infinite and contains stochastic policies in continuous space, assumption B.1 holds.
18

---

Published in Transactions on Machine Learning Research (03/2025)
Although the aforementioned examples toyish, they demonstrate that although assumption 3.1 is always true when II is finite, this is not the only case. Further characterization for when the assumption holds is left. for future work.
B.2 On the existence of solution to
In our definition of II in 2.5 and the formulation of our objective in 2 it is possible that no solution to exists in settings where IT" empty. This non-existence issue reoccurs objective ! where possible that no policies exist that achieve Vmax- In all of these cases, non-existence is a result of an infinite-sized II where sequence of policies exists in II that come increasingly arbitrarily close achieving Viaax (or, in the case of 2 to achieving the optimal probability of satisfying (p), without ever reaching the maximum value.
In these cases, we clarify what a policy that optimizes our true objective 5 is actually achieving. Recall that we ultimately aim to optimize a proxy objective of Rr + AV=, under a sufficiently large A. If the set II* is empty, then by definition, there does not exist a "gap" between policies II" and policies outside of it. other words, the value of is 0, and Assumption 3.1 does not hold. As a result, as À tends to infinity, the sequence of policies that increasingly optimal with respect to Rx + AV, will always prioritize increasing V over Rx- In other words, if assumption 3.1 does not hold, optimizing 5 will continually try to improve the proxy reward for LTL satisfaction and will ignore resulting changes to the MDP reward R..
It is theoretically possible that subsequent policies along the aforementioned sequence have arbitrarily different R7, which is undesirable. However, in practice, this does not tend to be the case, and policies that learn to optimize objective 5 exhibit behavior that is apparently both LTL-satisfying and performant in MDP reward, as evidenced by our experiments in Section 5 Generally, values for R2 are not highly unstable along the sequence of policies that are increasingly optimal with respect Vx,, and allowing to serve as a hyperparameter effectively enables tradcoff to value R₂ against V, (sce Scction 5
C Proof for Theorem 4.
We start with some notation. Let reyelEn represent the reward function for trajectory 7 that are returned by the execution of Alg, Let T(7) be the set of timesteps when an accepting state in B is visited for a trajectory. We write the value function for CyclER, letting Ie be the same function as defined in function
Assumption C.1. Suppose Trax max Er-My [(T) ( - Φ < M, there is a uniform bound on the
last time a bad (non-accepting) trajectory visits an accepting state across all bad trajectories induced by any policy.
Lemma C.2. Under Assumption C.1 for any π E II and > 0 we have
V2- [T + pl s
when 7 2 (1 (1- is chosen appropriately.
Proof. We follow the proof style of Lemma 4.1 from Voloshin el al. 2023
Let IP|T }= yp] = p be the probability
that n satisfies the LTL specification sp. Recall the value function
0
Peyc
E MM
Σ
TrrCYEERR!
Let ((T) be the (random) i-th visit to an accepting state in B. Let T(T) T(r)( refer to the first and last visit, respectively.
Because E
[t] = 1 only when a transition in a cycle is taken (and only once per that transition) and the
To
distance between successive visits to accepting state is le] then most 2d reward is accumulated between
19

---

Published in Transactions on Machine Learning Research (03/2025)
Rean Ei Tigtt Per PerCyaEal1) and therefore
successive visits to an accepting state. In other words Mr-
Ve S T-
Further, every trajectory т is decomposable into (1) the partial trajectory up to the first visit (ie. at time (()), the partial trajectory between the first and last visit (ie. between time (()) and (()) and (3)
the remainder of the trajectory. For trajectories that satisfy the LTL specification, (()) = oo, otherwise (-) S M, finite and bounded (by Assumption C.1 For ease notation, we omil. the dependence of on (i.e. we write (() T())). By linearity of expectation, we can rewrite our previous equation as:
Tio
T
Veyc
E TNME
Σ 1=0
r re CydlERR +
Σ +1
r T TyelER
E Trc
Σ
TMM
L=
11
When a path is accepting, by definition, Br-ME initial path will achieve a reward 1.
Eieo L Eyd r
1 because every accepting
By considering accepting trajectories of LTL formula ip, then ((-1) = 00:
Ter E } bo] PPTT T 0l p 1-7
Veye
1+
E T-MM
Σ +1
where the incquality follows from having dropped any value from non-satisfying trajectories. On the other hand, by the law of total expectation, for lower bound we have:
Veye P
T T Ter 7 +(1 +(1-p) p)
Σ r r BreYCIER
11/= k /
M
1 N41
S P 1- + (1 p)
-
where the first term comes from the upper bound on Vaye S 1 and the second term comes from bounding Tio with uniform upper bound M by Assumption C.1
Combining the upper and lower bound together and subtracting off p from both sides, have
0 < (1 - (1->)\eve S M+1
Select 7 2 (1 e) e)xTI which implics that
((1 (1-7)) VV-ye - pl S
Lemma C.3. Let max P|T t v/. Under Assumption C.1 then any policy optimizing Veye (te. achieving max] } maintains Veae p"1 S
Proof. This follows by an identical argument as in Theorem 4.2 Voloshin et al. 2023). by using Lemma peye prot-optimiiing policy wyye must satisfy [11 7) Veye
p=1 < < <when 7 is selected as Lemma C.2
20

---

Published in Transactions on Machine Learning Research (03/2025)
Flat World
ZonesEnv
ButtonsEnv
432
1290
1790
1300
1200
1000
Stapped tn.
205
Figure 4: Training curves showing the shaped FLTL achieved by CyclER-learned policies, averaged over 5 random seeds. Each point the mean of 10 stochastic policy rollouts.
CyclER
LCER
LCER (no 7MDP)
Figure 5: Sample trajectories from each baseline method in the Forld domain (each row is different sood). CyclER is able to consistently learn behavior that repeatedly visits and accepting state. The LCER baseline cannot achieve this long horizon task and instead optimizes for TMDP. The LCER (no PMDP) baseline, even when successful visiting the accepting state (bottom right), does qualitatively learn satisfying behavior despite visiting the accepting state.
Additional Experimental Results
Shaped Reward Training Curves In Figure 4 provide training curves for CyclER's performance the shaped LTT. proxy reward (i.e., CyclER-hhaped reward) in each of our experimental domains. These curves allow us to compare the difference in performance between unshaped and shaped LTL reward and provide insight into a potential correlation between the two. We notice that in all baselines, CyclER-learned policies are able to achieve nonzero shaped reward early training. Our learned policies achieve nonzero unshaped reward (recall the curves in Figure 3 slightly after significant returns shaped reward are achieved, which supports our hypothesis that CyclER-shaped reward will successfully 'guide' policy towards visiting the LDBA accepting state. We note that the scales of the CyclER-shaped LTL rewards visualized in Figure | vary significantly; the exact numerical values are dependent on specific environments and do not hold any exact meaning with respect to the unshaped LTL reward.
Qualitative Analysis To provide more insight into how CyclER learns to repeatedly visit the accepting state, we visualize sample trajectorics from policies learned by each of our basclines the Flat World domain, and present these samples in Figure 5 Recall that in this domain, our LTL specification instructs an agent to traverse the red, yellow, and green regions indefinitely, while avoiding the blue region. Tt. is obvious that.
21

---

Published in Transactions on Machine Learning Research (03/2025)
2.0
CyclER
LCER (no MDP)
Unshaped LT Reward
1.0
0.5
2
3
5
Timesteps (x1e5)
Figure 7: Training curve comparing unshaped LTL reward achieved by CyclER and LCER in the Flat domain with = (()) Performance is averaged over 5 random seeds. Each point is the mean of 10 stochastic policy rollouts.
the most efficient path to achieve this behavior is to navigate around the blue region and visit each colored region along a circular path.
On the left hand column of Figure 5 we see that policies learned using CyclER are able to perform this behavior, only slightly diverting from the circular path to visit purple regions and collect reward from TMDP. In the middle column, we visualize trajectories from policies learned where LCER used as FLTL- Due to the sparsity of this reward function, the policy quickly finds areas in the MDP where purple regions are clustered together, and repeatedly visits those areas (in the top middle, it traverses to a corner where the entropy of the policy will affect its position the least.) On the right hand column, we show trajectories from LCER trained without TMDP in its reward formulation. On the top right, we see that the baseline fails to achieve the task at all. More interestingly, however, on the bottom right, we find that the baseline does indeed achieve the task (i.e., visits the accepting state once), but does not exhibit behavior that qualitatively satisfies our task specification. After completing the task once, the agent turns back in the opposite direction and does not make obvious progress back towards either the red yellow regions, suggesting that this bascline has not learned to repeatedly satisfy the task.
We also provide sample trajectories from the two policies learned in the experiment addressing question 2 in section 5. The trajectorics, visualized in Figure G. show the difference in behavior wet the two successful policies when one is aware of TMDP during training and when one is not, The MDP reward-aware policy acts notably different, altering its trajectory to reach purple bonus areas (even those that are somewhat far away from the colored regions of interest), while the MDP reward-unawan policy makes no such adjustments and optimizes for completing the LTL task as often as possible.
Figure 6: Trajectories from CyclER-trained policy on rdual (left) and a CyclER-trained pol- icy on just the shaped rI.II (right) in the Forld domain.
Direct comparison in LTL-only setting To more directly eval- uate CyclER's efficacy in alleviating the reward sparsity problem, recreate the FlatWorld experiment from (Voloshin et al.) 2023 with the LTL specification G(F(red)&:X (F (Fyellow) )&G(bel This domain does not have additional MDP reward to be op- timized. As such, the LCER bascline is able to consistently accomplish this objective. This allows us to observe whether CyclER-based reward shaping provides improvements in LTL-guided policy learning even in the absence of an MDP reward. We visualize the training curves in Figure 7 We can see that CyclER not only converges a satisfying policy more quickly, but consistently achieves a higher reward when compared the LCER baseline. This confirms our hypothesis that reward shaping is valuable even in settings where the LTT. specification serves the lone objective.
22

---

Published in Transactions on Machine Learning Research (03/2025)
P(stttk: T) = Pinax;
b, < (x) = cz - (o(()))
P(s1Atte: [p) = -p(sLctkiip)
p(SEetki4 = ) max( -pppppp((ttt (), p( v))
P x&() min(p(@r:444: (
( p1(6) max p(
P(stetk, G(p))
min (p(se: (p(s):ttk:))
P(Stackk F(z))
max (p(Se:e4211)) ME(r,t+))
P( X(p)) (p)
p( (pU+)) = max (min( v) min (((spa)))))) rE(((t)))
Figure 9: Quantitative Semantics for LTL.
E
Quantitative Semantics for LTL
Practitioners have defined Quantilative Semanlics (QS) for number of lemporal logics in order to quantify the measure of satisfaction for given specification. These semantics, originally developed to monitor how continuous-valut sensor data (Maler & Nickovic 2004). have since been used in reinforcement learning to learn policies that satisfy formulae in a variety of specification languages, including Signal Temporal Logic (STL.) (Li et al. 2017 Balakrishnan & Deshmukh 2019). However, existing methods of QS for reward shaping fail to effectively extend to indefinite-horizon LTL tasks. what follows, we will introduce QS for LTL, discuss why naively using QS as reward is ill-fitted to deep RL for LTL, and introduce our own approach, extending the CyclER reward shaping method to effectively incorporate QS.
close hybrid control systems are to violating properties reliant
To use QS, we associate each atomic predicate E AP with robusiness measwre fa S + R that quantifies how close æ is to being satisfied at state s. x evaluates to truc at a given state iff f (s) 2 Cr, where ea is a constant threshold. We can compose variables AP with the logical and temporal operators of LTL by introducing QS for each operator, which follows the standard semantics defined for languages like TLTL {Li et al.) (017)) and STL (Maler & Nickovic 2004 Fainckos & Pappas 2009) and is provided in figure 9 An LTL formula &p is true il the itative evaluation of P& > 0 and false herwise We also define
(0.5, 1)
(1. 0)
a maximum and minimum achievable value for in a given MDP as Punx and Pmin; respectively.
(-1,
(0.5.-1)
To better understand quantitative evaluation for given LTL formula, consider a trajectory (which we will denote as {) from the Flatworld MDP, shown in figure g and the formula PPay F(r)&G((-e))
Figure 8: A toy trajectory in the Flatworld MDP.
We can define robustness measures for our atomic propositional variables fs(s) distance(s, Zcenter) < Tradius, requiring that the agent be within a region for its variable to evaluate to true.
Let's quantitatively evaluate Ptay on the trajectory ç. For the expression F(r), we find the maximum quantitative evaluation for the variable r in our trajectory. Since our trajectory visits the red region at point (0.5, -1), the evaluation for r at that point is some positive value c, > 0, so the expression F(r) will evaluate true. For the expression G(-b), we negate the quantitative evaluation and find the minimum value for the negated evaluation of b. At the point (1, 0), the agent closest to the blue region, but since it does not enter
23

---

Published in Transactions on Machine Learning Research (03/2025)
it, the minimum value is some positive value c6 > 0. The quantitative evaluation for Ptoy on & is therefore positive value min(c,,(t, so Ptay evaluates to true for &.
Suppose we were to naively use the quantitative evaluation of a given LTL specification "off-the-shelf" as a reward function for an RL agent. Since the quantitative evaluation of a trajectory at any given point in time requires evaluating the future states of the trajectory, we can only assign a reward for entire trajectories. For the toy specification considered in our example, the reward would be the smaller of (1) the maximum distance the agent reaches from the blue region and (2) the minimum distance the agent reaches from the red region during the trajectory. Although this seems reasonable evaluation of an LTL formula becomes increasingly more obscure as the specification increases in complexity. For example, for the specification defined in Figure [ which instructs the agent to indefinitely oscillate amongst the red, green and yellow regions while avoiding blue, & would have a lower quantitative evaluation than a trajectory that does not visít. any of the three regions but just barely enters the blue region, even though the latter violates the specification without making any qualitative progress. Moroover, there would be no meaningful difference in quantitative evaluation between & and a trajectory that visits red, green and yellow while avoiding blue, or between trajectory that completes the task twice, thrice, and on.
reward for example, the quantitative
The quantitative evaluation of a trajectory as a reward signal for LTL fails because there are no well-defined terminal conditions for evaluating a finite trace under an infinite-horizon specification (e.g., +o from Figure D. which means that value produced is often useless when used as a reward signal. This is made worse due to the fact that quantitative evaluation of an LTL formula assigns a single value for an entire trajectory, making credit assignment difficult. We propose an alternative reward that avoids these issues, extending the CyclER approach to handle quantitative semantics by rewarding "progress" made by traversing individual transitions in IB.
The high-level intuition for our method is as follows: recall that for a given trajectory, CyclER computes hypothetical rewards for each cycle in B, where reward is given if the next transition is taken within that cycle during the trajectory. Our key insight is that we can straightforwardly extend this paradigm to use QS by instead rewarding quantitative progress made towards taking the next transition within an individual cycle. Each transition in IB corresponds to a non-temporal predicate of atomic propositions. Crucially, we can quantitatively evaluate these prodicates on individual states, rather than trajectories. When agent moves to new state in M, we can quantify how close the agent is to satislying the transition predicate (and therefore taking the transition in the cycle), and compare it to how close the agent was to satisfying the transition predicate in the previous state. If there is a positive difference between these two values, we reward that progress made towards satisfying the transition predicate.
We present our reward function in function 7 in the main text. In the context of Alg. I the reward function defined in / will replace re. Intuitively, we can interpret the reward function defined in 7 as identical to rc, but rewarding quantitative progress towards taking transition in cycle rather than only offering reward once that transition is taken We normalize progress using Pmax and Pmin to ensure that the scale of rewards from function 7 remain consistent.
Let us once again return to the example trajectory in Figure g with the LTL specification and LDBA from Figure D as our objective, and consider the cycle {1, 2, 3, 0). We begin in state 1 of IB, where the transition we aim to take has the corresponding predicate r. When we transition from (-1, -1) to (0.5, -1), we satisfy r, and receive positive reward from CyclER because we are closer to than we were in the previous state. We are now in state 2 of B and seek to take the transition with predicate g. For the transition from (0.5, -1) to (1, 0), we reccive positive reward for getting closer to 9, and for the transition from (1, 0) to (0.5, 1) we receive positive reward for successfully moving closer to g. Note that each transition of our trajectory & qualitatively makes progress towards visiting the accepting state of B, and this is reflected in the positive rewards assigned by Tgs.
In environments where the individual variables in AP are difficult to satisfy, the usage of QS can offer more dense reward that still leverages the full expressivity of L.L. In our experiments, we show that using the QS version of CyclER strongly outperforms existing approaches of using QS in learning to satisfy andefinteehorizonn LTL specifications (Li et al.) 2017 Balakrishnan & Deshmukh, 2019) and enables the learning of LTI-coopliant policies in complex environments.
24

---

Published in Transactions on Machine Learning Research (03/2025)
Algorithm 2: Find Minimal Accepting Initial Paths and Cycles (FindMAITSAAnIMICAS
Imput: LDBA B, accepting states set B Initialize C to an empty set;
Initialize P to an empty set:
DFS(b-1, (, P);
foreach accepting state 6" E B" do
Initialize visited
empty set;
Initialize C. to emply set; DFS(b",, O, C);
Add C to C; return C, P
Algorithm 3: DFS (Helper for Alg. 2
Input: Starting node b, Path set S
Add node 6 to visited;
foreach Outgoing transition (b, v, b) from do
if D' E B" then Add the transition (b, b,)') to
Add p to S;
else
if 6' & visited then
Add the transition v, b') to p: DFS(b 5); Remove node b from visited;
F Additional Algorithmic Details
Motivation of visiting frontier. To motivate the importance of maintaining the visited frontier e introduced in section 4.2 we show via example that the existence of non-accepting cycles in may allow for trajectories that infinitely take transitions in a MAC or MAIP without ever visiting an accepting state.
0
g
Consider the accepting cycle (3, 1, in the partial automaton in Figure 10 Although this cycle is a MAC, there does exist separate cycle starting and ending at state 1 (L.e. the cycle (1, ()-) If we give reward every time a transition in the cycle (3,1,2) 1, is taken, a policy may be able to collect infinite reward without ever visiting an would infinitely
2
r
b
accepting state. For example, in Figure 10 a path 21,2,0,1,,,0 take transitions in a MAC, and therefore collect infinite reward without ever visiting the accepting state Our visited frontier will ensure that rewards will only be given once per transition until an accepting state is visited.
3
Figure 10: A partial
Büchi automaton that necessitates visited frontier.
F.1 Finding Minimal Accepting Cycles and Accepting Initial Paths
In algorithms 2 and we include the psuedocode for finding minimal accepting initial paths and minimal accepting cycles in a given B, which constitute the sets P and C respectively for usage in algorithm
G Additional Experimental Details
For each random seed of training, the locations of the following objects were randomized and fixed: in ForlW, the location of the bomus areas, ZonesEnv, the locations of all colored regions and hazard regions, and in ButtonsFnv, the locations of the buttons, bonus areas, and
Environments and Tasks.
25

---

Published in Transactions on Machine Learning Research (03/2025)
Environment
LTL
Flat WarlWorldd
((F(gee)) (FPyllll (or G (bbneeeeFluuppeeeee[dddod... (green)) G(F
ZonesEnv
ButtonsEav
Table 3: Specification for each domain.
gremlins. In ZonesEnv and ButtonsEnv, 2-dimensional action space E [-1,
the Point robot from Ji el. al. 2023 agent, which has
The observation space and environment used in our EnnesEnv are the the default spaces provided the Zones Level 1 environment in Ji et al. (023). with the following changes: there are additional lidar observations for each the four colored zones, and we place four static collidable walls as boundaries to enclose the agent's 's environments at the border of where objects can be randomly placed. The observation space and environment. used in our ButtonsEnv experiments are the default spaces provided the Button Level 1 environment in Ji et al. 2023 with two gremlins and eight bonus regions.
In Zon and ButtonsEuv, we define simple robustness measure for each alomic propositional variable in the environments (the red, yellow, green, and purple regions in ZonesEnv, and buttons 1 through 4 and gremlin for ButtonsEnv). The robustness measure for a general variable x at a given state s defined as follows:
fa(s) distance(s, 5
For example, if an agent was distance of 2 units away from the red region in ZZoeeEnvv, the robustness measure of the variable "red" at that state would evaluate to -2. For ButtonsEav, where the gremlin variable refers to multiple moving objects, the robustness measure corresponds to the minimum distance from the agent to any gremlin. We set Paax = in our environments and Pmin to be the negative largest distance achievable each environment.
Our LTL task specifications are defined in Table g We use the Spot tool Duret-Lutz et al. 2022 to convert our specifications into corresponding LDBAs We report the number of states, transitions, and MACs in each LDBA used in our experiments in Table
Training details. For experiments, results are averaged over five random seeds. We provide hyper- parameter choices for PPO for each experiment in
Figure 11: Example visualizations of the ZonesEnv (left) and ButtonsEny (right) environments.
Table 6 and choices for À in Table 4 In Table G batch size refers to the number of trajectories. In our PPO implementation, we use a 3-layer, 64-hidden unit network as the actor using ReLU activations, and a 3-layer, 64-hidden unit network architecture with tanh activations between layers and no final activation function for the critic. The actor outputs the mean of Gaussian, the variance for which learned by 3-layer, 64-hidden unit network that shares the first 2 layers with the actor policy itself. All experiments were done equipped with NVIDIA RTX A4500 GPU. We use the Adam optimizer in all experiments.
Intel Core i9 processor with 10 cores
In Figure 3 reward was computed by evaluating the policy every ten trajectories in the case of Flat World, and every 25 trajectories for ZonesEnv and ButtonsEnv. The FITL and TMDP values shown are from averaging performance over ten rollouts for each data point with a smoothing window of size
For the BHNR baseline, we use partial signal window size of 60 for FlrlWorld, 700 for ZonesEnv, and 750 for ButtonsFav, treating this value as hyperparameter and performing sweep to select the window size.
26

---

Published in Transactions on Machine Learning Research (03/2025)
Environment CyclER
LCER
TLTL
BHNR
Flat 400
1000
ZnnesEnv 200
1000
10
ButtonsEnv
100
1000
10
Table 4: Values for used by baselines for each domain.
Environment
States
Edges
MACs
Flat World
18
14
ZonesEuv
35
44
ButtonsEnv
9
Table 5: Details for the LDBAs used each experimental domain.
Our TLTL baseline trained by assigning the TLTL value a trajectory as the reward the end of the trajectory, and using the discounted reward-to-go for each prior timestep as the reward signal. For TLTT. and BHNR baselines, evaluation of the formula the reward, where the resulting rewards were mostly negalive due to how we defined our robustness measures for each variable. To evaluate if the sign and magnitude of the reward caused difficulty during learning, we normalized the quantitative evaluation done in TLTL and BHNR using Puin and Pmax: so that the reward value would be between and 1. We found that this adjustment did not have a significant impact on either baseline's ability to learn FLTL, but it did allow for easier optimization ion of TMDP; therefore, we report the results from the normalized evaluation in our experiments.
tried computing FLTL in two ways: first, tried using the original quantitative
Environment
Critic LR
Actor LR
Update freq.
7
Batch size
[r] (training)
World
0.001
0.0003
1
0.98
128
120
ZonesEuv
0.0125
0.0025
0.3
3
0.99
128
700
ButtonsEnv
0.001
0.0003
0.2
3
0.99
128
750
Table 6: Hyperparameters used during training for each domain.
27


Reviews:
[{"review_id": "StkAMjxnd7", "reviewer": "Reviewer_tqsv", "summary": "", "questions": "", "limitations": "", "rating": null, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "# Strengths\nWhilst this problem seems to have been studied in only one prior paper [Voloshin et al. 2022], it is natural and relevant.\nThe approach to reward shaping is innovative, reasonably intuitive and shows promise in the experiments, which are presented in good detail.\n\n# Weaknesses\nThere is a significant lack of clarity in Sec. 4. There is a lot of semi-formal prose and it feels like a lot of clarifications have been moved to the appendix in such a way that just reading the main text is insufficient for grasping the ideas.\n\nI think the paper might have benefitted from focussing on the simpler problem of RL where the single objective is to maximise LTL objectives. The constrained setting mostly adds orthogonal challenges (although reward sparsity becomes an even bigger problem). That way, the presentation could be improved and space is created to explain the main ideas CyclER with QS in sufficient detail in the main body.\n\nThe environments seem pretty simple and similar. There is no empirical comparison to other works for the RL + LTL special case apart from Voloshin et al. 2023.\n\n# Questions\n- What is the intuition why re-distribution of rewards in CyclER help? I guess it depends on how advantage is estimated in PPO? Is bootstrapping used?\n- It is not clear how CyclER with QS can provide a dense reward signal. E.g. consider a reachability task which requires lots of transitions in the MDP but only self-loops in the initial state of the LDBA are taken. Then it seems to me that your method only provides small rewards twice: the first time the loop is taken and when the accepting state is reached. On the other hand, a large number of transitions in the MDP, which make slow but steady progress, remain unrewarded. Am I missing something?\n- Are there theoretical guarantees for CyclER with quantitive semantics?", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "Yes", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "paper_topic_and_main_contributions": "", "excitement": null, "reproducibility": null, "ethical_concerns": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "summary_of_contributions": "The paper investigates a constrained RL problem, where the objective is to find a policy maximising a cost objective amongst the policies satisfying a high-level logical specification provided in linear temporal logic (LTL) with maximal probability. \nIt is shown that the constrained problem can be transformed to an unconstrained one via a Lagrange multiplier and eventual discounting provided certain hyperparameters are chosen sufficiently high.\nThereafter, a denser reward signal for LTL satisfaction is provided, which acknowledges partial progress to accepting states and re-distributes the reward at accepting states.\nLeveraging quantitative semantics, a refined reward signal is presented, which is denser for LDBAs with few transitions.\nFinally, the benefits are demonstrated empirically.", "claims_and_evidence_yn": "Yes", "claims_explanation": "", "audience_yn": "Yes", "audience_explanation": "", "requested_changes": "It is very important to improve the presentation of Sec. 4. In particular, I would appreciate a full worked example for CyclER and a better explanation of Fig 1 (the label is misleading: there is no actual formal MDP and the part on the very right isn’t really explained).\nIt would be helpful to have the experiments available online to independently verify them.\n\nMinor points:\n- p. 3 \"An LDBA _may_ have separate\": by _definition_ an LDBA always has those separate components\n- p.3 \"not including the initial state $b_{-1}$\": why is $b_{-1}$ not included?\n- p.4 make it clear in notation that $j$ depends on $t$, e.g. use $j_t$\n- Theorem 3.2: consistently use roman font for $R_{max/min}$\n- Def. 4.1: check $b_0$ vs. $b_{-1}$\n- p. 6 what is meant by “complete trajactory”\n- Eq. 6: subscript $b_t$ missing on RHS\n- P.6 “once per visit to accepting state”: Obscures that reward is also provided at non-accepting states\n- Theorem 4.1: Formally state Theorem 4.1 in appendix and clarify relation to Lemma C.3\n- Algorithm 1: It would aid understanding to reset e explicitly\n- Eq. 7: check index $b_{t+1}$\n- P. 9 “visits value” not defined\n\n- p. 17: definition of $T^M(s,a,s')$ isn't given\n- p. 17: last paragraph is unclear\n- p. 18: Can you give a counter-example for the emptyness of $\\Pi^*$? Can this be fixed by compact action spaces?\n- App. B.2 middle pargraph: What does it mean for $\\lambda$ to be \"sufficiently large\"? Doesn't it need to be infinite in that case\n- p. 22 last line typo in coordinate", "broader_impact_concerns": "N/A", "additional_comments": "", "extra_scores": {}, "extra_text": {}}, {"review_id": "OjrLWv4116", "reviewer": "Reviewer_srmk", "summary": "", "questions": "", "limitations": "", "rating": null, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "# Strengths\n\n* The paper is generally well written and polished.\n* The method and contributions are well motivated, and fills in a gap in the RL+LTL literature in providing a method that (1) is based on deep RL (allowing continuous MDPs), (2) combines both RL and LTL objectives. \n* The main contribution, the reward shaping method itself, CyclER, is quite intuitive, and seems to produce much smoother rewards than prior work (notably LCER).\n\n# Weaknesses\n\nI think the main weakness is in the experimental evaluation. The authors show 3 MDPs where CyclER effectively optimizes $r_{LTL}$, while the baselines essentially fail (e.g., even LCER with the LTL reward only, though it has non-zero performance). This essentially shows, by an existential argument, that there are situations where \"CyclER works\", whereas prior work doesn't. I generally believed this when reading the paper, since the method seems sensible to me. Thus, it would have been more informative to understand where the boundary lies, or how far can CyclER go. Given that LTL has an inherent sparseness/long-horizon challenge to it, it would have been very helpful to get a sense of how sparse can the LTL reward be such that CyclER can still satisfy it within a reasonable computational budget, and where that breakdown point is compared to LCER or other baselines.", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "Yes", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "paper_topic_and_main_contributions": "", "excitement": null, "reproducibility": null, "ethical_concerns": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "summary_of_contributions": "This paper introduces CyclER, a method for Deep Reinforcement Learning with continuous state and action spaces under general Linear Temporal Logic constraints. The key idea is to post-hoc reward-shape past trajectories in the MDP (thus, Experience Replay) using a metric of partial progress towards either a first accepting state in the Büchi automaton corresponding to the LTL objective, or a cycle since the last state, with higher rewards given to shortest paths / cycles, and only once per transition. The authors then optimize for a Lagrangian objective that combines the MDP's reward and the LTL objective, and propose a method to incorporate Quantitative Semantics into CyclER. In experiments in 3 environments, CyclER finds policies that effectively satisfy the LTL constraint, while still seeking the MDP's rewards.", "claims_and_evidence_yn": "Yes", "claims_explanation": "", "audience_yn": "Yes", "audience_explanation": "", "requested_changes": "(Not critical, but I think would significantly strengthen the experimental argument): Compare to LCER in environments where LCER was initially successful on, to isolate just the influence of reward shaping in satisfying LTL. It should suffice to just run on the 2 variations of FlatWorld (no MDP rewards) that LCER used. This would be a cleaner comparison to justify that the reward shaping alone is helpful, even in the absense of the MDP rewards.", "broader_impact_concerns": "N/A", "additional_comments": "", "extra_scores": {}, "extra_text": {}}, {"review_id": "ttc129MalF", "reviewer": "Reviewer_AdC7", "summary": "", "questions": "", "limitations": "", "rating": null, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "Strengths:\n- Innovative idea for the problem that LTL rewards are usually sparse and might not include all objectives that should be considered\n- Solid evaluation with different ablations on three environments.\n\nWeaknesses:\n- The proposed concept is not clearly presented in the Abstract and Introduction\n- The contributions are formulated too vaguely throughout the text and have to be more concise", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "Yes", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "paper_topic_and_main_contributions": "", "excitement": null, "reproducibility": null, "ethical_concerns": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "summary_of_contributions": "The paper proposes a new reward-shaping approach for model-free RL with LTL task specification. Specifically, the authors propose a reward function with an LTL and an MDP component. The LTL component is usually a sparse reward for visiting accepting states. This paper proposes a reshaping approach to make the LTL reward more dense. The authors evaluate their approach and existing baselines on multiple benchmarks and observe that their approach performs better with respect to the LTL objective than approaches with sparse rewards.\n\nThe clarity of the paper varies between sections as well as the writing quality.", "claims_and_evidence_yn": "Yes", "claims_explanation": "", "audience_yn": "Yes", "audience_explanation": "", "requested_changes": "- The abstract needs improvement. The problem addressed and contributions are not clear enough, and the language can be improved.\n- The introduction is not well written and rather confusing: \n   * the work is not well motivated by the first paragraph, \n   * the second paragraph requires references\n   * in the third paragraph it is unclear what RL-based reward optimization means and it is not clear what the novelty of the proposed approach is\n    *  (+) the last sentence in the third paragraph is too strong or too vague: there is work that uses temporal logic (TL) for constraining and deep RL for performance objectives [1], there is work that uses TL for deep RL where the specification describes [2-4]\n   * it seems that there are three \"in this paper paragraphs\" - please restructure to one concise paragraph \n   * for the fourth paragraph the fit into the overall story of the introduction seems off\n- Fig. 1 requires references after \"unlike other approaches\"\n- The contributions are not concise enough. This work is not the first on deep RL and TL (this statement is repeated multiple times - please revise everywhere), see previous comment marked with (+)\n- Can you discuss the scalability of your reward shaping with an increasing number of states? \n- If transitions are scarce, then the reshaped reward in Eq 6 or 7 is still very sparse. Can you add to your experiments how many transitions are in the automata? And can you discuss this issue?\n- The first two paragraphs in Sec. 4.3. distract from the proposed work. In my opinion, they are either preliminaries or related work.\n- The experiments are solid, yet they are not described and discussed well enough:\n  * it would be good to report the shaped rewards for the first set of experiments. Right now it is not clear how much information gain is accomplished with the new reward\n  * it would be good to introduce a notation that clarifies when the quantitative $r_{LTL}$ reward is used and when the transition-based shaped reward.\n  * The question (2) is not well demonstrated and discussed. If you do not want to make a table for the results, then rather state relative metrics between ablations. Also, what do you observe qualitatively?\n  * the usage of $r_{LTL}$ for unshaped and shaped reward is confusing\n- Fig 3: It is unclear what the x-label \"trajectories\" means and for how many training steps the approaches are trained with PPO. \n- Table 1: I think $r_{LTL}$ is confusing since this is the unshaped reward. Reporting satisfaction cycles or similar would be much better.\n- The literature review in the appendix sometimes repeats the exact same sentences and it is unclear what the criteria are for the literature presented in the main text and the literature in the appendix. I would suggest having a concise but full literature review in the main text.\n\nMinor:\n- The notation on page 3 for $b_0$ seems inconsistent. Or what is $b_{-}$?\n- In Sec. 4 your proposed approach becomes clear. Yet, it would be better if you could achieve this in the introduction already.\n- I believe the \"column\" formatting of Alg. 1 and Tab. 2 is not aligned with style requirements. I think these should be adapted to single-column format. Additionally, the tables could be made more visually appealing.\n- Can you relate/discuss your work with respect to safe RL (e.g., [5-8]) where safety (in your case the task specification) and performance objectives (in your case the MDP reward) are also often incorporated differently?  \n\nReferences:\n\n[1] Safe Reinforcement Learning with Probabilistic Guarantees Satisfying Temporal Logic Specifications in Continuous Action Spaces. Hanna Krasowski, Prithvi Akella, Aaron D. Ames, and Matthias Althoff. In Proc. of the IEEE Conference on Decision and Control (CDC), 2023 \n\n[2] A. Lavaei, F. Somenzi, S. Soudjani, A. Trivedi and M. Zamani, \"Formal controller synthesis for continuous-space MDPs via model-free reinforcement learning\", Proc. of the ACMIIEEE International Conference on Cyber-Physical Systems, pp. 98-107, 2020.\n\n[3] D. Gundana and H. Kress-Gazit, \"Event-based signal temporal logic synthesis for single and multi-robot tasks\", IEEE Robotics and Automation Letters, vol. 6, no. 2, pp. 3687-3694, 2021.\n\n[4] M. Cai, M. Hasanbeig, S. Xiao, A. Abate and Z. Kan, \"Modular deep reinforcement learning for continuous motion planning with temporal logic\", IEEE Robotics and Automation Letters, vol. 6, no. 4, pp. 7973-7980, 2021.\n\n[5] Hanna Krasowski, Jakob Thumm, Marlon Müller, Lukas Schäfer, Xiao Wang, and Matthias Althoff, Provably Safe Reinforcement Learning: Conceptual Analysis, Survey, and Benchmarking, Transactions on Machine Learning Research, 2023 \n\n[6]  Mohammed Alshiekh, Roderick Bloem, Rüdiger Ehlers, Bettina Könighofer, Scott Niekum, and Ufuk Topcu.\nSafe reinforcement learning via shielding. In Proc. of the AAAI Conf. on Artificial Intelligence (AAAI),\npp. 2669–2678, 2018.\n\n[7] Xiao Li, Zachary Serlin, Guang Yang, and Calin Belta. A formal methods approach to interpretable reinforcement learning for robotic planning. Science Robotics, 4(37), 2019a\n\n[8] Bettina Könighofer, Florian Lorber, Nils Jansen, and Roderick Bloem. Shield synthesis for reinforcement\nlearning. In Leveraging Applications of Formal Methods, Verification and Validation: Verification Princi-\nples, pp. 290–306, 2020.", "broader_impact_concerns": "N/A", "additional_comments": "", "extra_scores": {}, "extra_text": {}}]

Author rebuttal:

Meta-review: The reviewers initially pointed out several issues of clarity. However, by engaging in a continuing discussion with the reviewers and updating the manuscript accordingly, the authors have significantly improved the clarity of the work. They have also conducted additional experiments to better support their claims. At this point, I consider the paper ready for publication.
Decision: Accept (poster)