Accelerated Learning with Linear Temporal Logic using Differentiable Simulation
Authors: Alper Kamil Bozkurt
Calin Belta
Ming Lin
Venue: ICLR 2026 Poster (2026)
Keywords: reinforcement learning
temporal logic
differentiable simulation
Primary area: reinforcement learning
TL;DR: We address challenges of scalable learning with correct objectives, using LTL as the formal specification language and differentiable simulation to accelerate learning.

Abstract: Ensuring that reinforcement learning (RL) controllers satisfy safety and reliability constraints in real-world settings remains challenging: state-avoidance and constrained Markov decision processes often fail to capture trajectory-level requirements or induce overly conservative behavior. Formal specification languages such as linear temporal logic (LTL) offer correct-by-construction objectives, yet their rewards are typically sparse, and heuristic shaping can undermine correctness. We introduce, to our knowledge, the first end-to-end framework that integrates LTL with differentiable simulators, enabling efficient gradient-based learning directly from formal specifications. Our method relaxes discrete automaton transitions via soft labeling of states, yielding differentiable rewards and state representations that mitigate the sparsity issue intrinsic to LTL while preserving objective soundness. We provide theoretical guarantees connecting Büchi acceptance to both discrete and differentiable LTL returns and derive a tunable bound on their discrepancy in deterministic and stochastic settings. Empirically, across complex, nonlinear, contact-rich continuous-control tasks, our approach substantially accelerates training and achieves up to twice the returns of discrete baselines. We further demonstrate compatibility with reward machines, thereby covering co-safe LTL and LTLf without modification. By rendering automaton-based rewards differentiable, our work bridges formal methods and deep RL, enabling safe, specification-driven learning in continuous domains.

Published as a conference paper at ICLR 2026
ACCELERATED LEARNING WITH LINEAR TEMPORAL LOGIC USING DIFFERENTIABLE SIMULATION
Alper Kamil Bozkurt"
Calin Belta & Ming C. Lin
Electrical & Computer Engineering Virginia Commonwealth University Richmond, VA, USA bozkurta@vcu. edu
Department of Computer Science University of Maryland College Park, MD, USA
{calin, 1 1in] 3 @und. edu
ABSTRACT
Ensuring that reinforcement learning (RL) controllers satisfy safety and reliability constraints in real-world settings remains challenging: state-avoidance and con- strained Markov decision processes often fail capture trajectory-Ieve require- ments or induce overly conservative behavior. Formal specification languages such as linear temporal logic (LTL) offer sorrect-y--constructii their rewards are typically sparse, and heuristic shaping can undermine correct- ness. We introduce, to our knowledge, the first end-to-end framework that inte- grates LTL with differentiable simulators, enabling efficient gradient-based Iearn- ing directly from formal specifications. Our method relaxes discrete automaton transitions via soft labeling of states, yielding differentiable rewards and state representations that mitigate the sparsity issue intrinsic to LTL while preserving objective soundness. We provide theoretical guarantees connecting Büchi accep- tance to both discrete and differentiable LTL returns and derive a tunable bound on their discrepancy deterministic and stochastic settings. Empirically, across complex, nonlinear, contact-rich continuous-contro tasks, our approach substan- tially accelerates training and achieves up twice the returns of discrete base- lines. We further demonstrate compatibility with reward machines, thereby cov- ering co-safe LTL. and LTL, without modification. By rendering automaton- based rewards differentiable, our work bridges formal methods and deep RL, enabling safe, specification-driven learning in continuous domains.
objectives, yet
INTRODUCTION
The growing demand for artificial intelligence (AI) systems operate in wide range of envi- ronments underscores the need for systems that can learn through interaction with their environ- ments, without relying on human intervention. Reinforcement learning (RL) has emerged as powerful tool for training controllers to perform effectively in uncertain settings with intricate, nigh-dimensional, and nonlinear dynamics. Despite the promising results in controlled environ- ments, deploying learned controllers in real-world systems where malfunctioning can be costly or hazardous-require not only high performance but also strict compliance with formally specified safety and reliability requirements. Therefore, ensuring that learned controllers meet these criti- cal specifications essential to fully realize the potential of AI systems real-world applications. Safety in learning is often modeled with constrained Markov decision processes (MDPs) (e.g. Ding et al. (2021)), where the accumulated cost must be within a budget. However, additive cost functions may not reflect real- world safety, as assigning meaningful costs to harms is challenging. Alterna- tive approaches define safety by avoiding unsafe states or actions (e.g. QQi et al. (202I)). which is simpler than designing cost functions. However, this may result in overly conservative policies and could not capture complex trajectory-level requirements.
Recently, researchers have explored specifying RL objectives using formal languages, which ex- plicitly and unambiguously express trajectory-based task requirements, including safety and live- ness properties. Among these, linear temporal logic (LTL) has gained particular popularity (e.g. Hahn et al. (2019); Bozkurt et al. (2020b); Icarte et al. (002)); Hasanbeig et al. (2023)) due to the automaton based memory it offers, which ensures history- indeeendeneee and makes it especially
"wor done while at University of Maryland, College Park cqual supervising

---

Published as a conference paper at ICLR 2026
suitable for long-horizon tasks, unlike other languages such as signal temporal logic (STL). Speci- fying desired properties in LTL inherently prevents mismatches between the intended behavior and the behavior learned through reward maximization- -ne of the most well-known safety challenges in AT (Amodei et al. 2016). Although these methods are proven to define the correct RI, objec- tives, the sparse logical rewards make learning extremely difficult, as obtaining nonzero reward often requires significant exploration. Denser LTL-based rewards provided through heuristics might accelerate learning (Kantaros] (022); however, if not carefully designed, they can compromise the correctness of the objective and misguide exploration depending on the environment, ultimately re- ducing learning efficiency. In this work, we address the challenge of scalable learning with correct objectives for temporally extended tasks. We adopt LTL as the specification language, leveraging the intuitive high-level language and the automaton- based memory provides. Unlike prior methods, our approach hurnesses gradients from disferentiable simulators to facilitate esficient learning di- rectly from LTL specifications, while preserving the correctness of the objectives. Our contributions can be summarized as follows:
We propose, to the best of our knowledge, the first approach that accelerates learning from LTI. specifications using differentiable simulators. Our approach effectively mitigates the inherent is- sue of the sparse rewards without sacrificing the expressiveness and correctness that LTL provides. We introduce soft labeling techniques for continuous environments that yield probabilistic s- actions and transitions in the automata derived from LTL, which ensures the differentiability of rewards and states with respect to actions. We establish formal guarantees connecting automata acceptance conditions with our differentiable framework, yielding a tunable bound on the discrep- ancy between discrete and differentiable LTL rewards, including in stochastic settings.
We demonstrate that our method accelerates learning, achieving up to twice the returns of base- lines across diverse experiments in complex, nonlinear, contact-rich settings where standard ap- proaches struggle to learn without handcrafted reward shaping. We further evaluate on reward machines, showing that our differentiable approach generalizes across formal method frameworks.
2 RELATED WORK
Safe RL. One common perspective in Safe RL defines safety as the guarantee on the cumulative costs over time within a specified safety budget, which is often modeled using constrained MDPs and has been widely studied (Gareıa & Fernández, 2013 Chow al. 2018 Stooke al.) 2020 Ding et al. (021). relying on additive cost functions and budgets, which may not adequately capture safety in many scenarios. In practice, it is often difficult to assign unambiguous scalar costs reflecting trade-offs between different harmful situations (Skalse et al. 2022). Other approaches define safety in terms of avoiding unsafe states and focus on preventing or modifying unsafe actions via shielding or barrier functions (Berkenkamp et al. [2117] Cheng et al. [219 Qin et al. [021: Zhan et al. 2024), requiring only the identification of unsafe states and actions, which is often casier than designing cost functions (Wang al.. 2023); however, they lead to overly conservative control policies Yuu jet al. 2022). Moreover, the requirements are often placed over trajectories, which could be more complex than simply avoiding certain states (Hsu et al. 2021). Our approach avoids these issues by employing LTL as the specification language to obtain conrect-by-construction RL objectives.
RL with Temporal Logics. There has been increasing interest in using formal specification lan- guages to encode task objectives that are vajectory-dependees particularly those involving safety requirements. LTL has emerged as a widely adopted formalism due to its expressiveness and well- defined semantics over infinite traces. Initial attempts to combine LTL with RL relied model- based approaches (Fu & Topcu 2014a Wen & Topcu 2021), which reduce specification satisfaction into a reachability problem that can be solved by RL, by exploiting the MDP transition structure to construct a product MDP with automata derived from LTL. However, the unavailability of accurate transition models limits their applicability, especially in deep RL contexts. Thus, model-free RL methods for LTL emerged, notably reward machines (RMs) (Toro Icarte et al. 2018 g Icarte et al.) 2018 Camacho et al.) (2019] Icarte et af., (022) for co-safe LTL. and LTT,, fragments, which directly generate rewards based on the acceptance states of the derived automata without explicit knowledge of transition dynamics. The introduction of LDBAs for MDP model checking (Hahn et al.. 2015), facilitated structured reward design with their simpler acceptance conditions for general LTL formu-
las (Hahn et al.) 2019 Bozkurt et al., (2020b). This line of work inspired numerous extensions and
applications across broader domains VVlooshi al. 2022 2023 Le et al. 2024 Perez et al.) 2024
Yalcinkaya et al. 2024; Jackermeier & Abate| (025). 3... Researchers have also explored continuous-
time logics such as STL,, whose robustness scores be used as rewards (Aksaray et al. 2016).
2

---

Published as a conference paper at ICLR 2026
However, these scores typically depend on historical information, violating the Markov assumption and thereby restricting their use in Long-horizon stochastic, or value-based RL settings. For detailed explanations and comparisons, see Appx. A
RL with Differentiable Simulators. Differentiable simulators enable gradient- based policy opti- mization in RL by computing gradients of states and rewards with respect actions, using analytic
methods (Carpentier & Mansard, 2018 Geilinger et al.,
2020
Qiao et al., 2021 Xu et al. [021]
Werling et al. 2 or nuto-differnntiation (Heiden et al.,
2021 Freeman et al. 2021), While Back-
propagation Through Time (BPTT) is commonly used (Zamora et al. 202 Du et al. 2021 Huang
ct al. 2021 Hu et al. 2020; Liang et al., 2019; Hu et al. 2019). it suffers from vanishing or explod-
ing gradients for long horizons as it ignores the Markov property of states (Metz et al. 2021). To
address this, several differentiable RL algorithms have been proposed (Parmas et al. 2011]] Suh et a
2022]. Short Horizon Actor-Critic (SHAC) (Xu al.) 2022) divides long trajectories into shorter segments where BPTT is tractable and bootstraps the remaining trajectory using the value function. Adaptive Horizon Actor-Critic (AHAC) (Georgiev et al.] 2024) extends SHAC by dynamically ad- justing the segment lengths based on contact information from the simulator. Gradient-Informe PPO (Son et al. (023) integrates gradient information the RL framework in an adaptive manner. Our approach builds a differentiable, Markovian transition function for LTL-derived automata, mak- ing it compatible with all differentiable RL methods. Unlike prior STL-based efforts (Leung et al.] 2023 Meng & Fan 2023), which rely mon-Markovian rewards and BPTT, our method supports efficient long-horizon learning with full differentiabilityy
3 PRELIMINARIES AND PROBLEM FORMULATION
MDPs. We formalize the interaction between controllers with the environments MDPs.
Definition 1. A (differentiable) MDP is a tuple M = (S, A, fo) such that S a set of continuous states; A is set of continuous actions; f f:Sx A + S is a differentiable transition function; po is an initial state distribution where Po(s) denotes the probability density for the state s.
For instance, for a given robotic task, the state space is the positions x and velocities x of relevant objects, body parts, and joints. The action space A may consist of torques applied to the joints. The transition function f captures the underlying system dynamics and outputs the next state via computing the accelerations ž by solving Mi J'F(x, x) + C(x, x) + T(x, &, a), for a given state = (x, x) E S and action a E A. Here, M is mass matrix; and F. C, and T are, respectively, force, Coriolis, and torque functions that can be approximated using differentiable physics simulators.
RL Objective. In RL, a policy A is evaluated based on the expected cumulative reward, i.c. return, associated with the paths d==$y$1... ... (sequence of visited states) generated by the Markov chain (MC) M, induced by the policy л. We write o [t], or [:f). a[t:] for st, the prefix sy... and the suffix S,5t+1 1 ... For given reward function R discount factor (E, (E, 1) and a horizon H, the return of a path a from time IEN, is defined as G (a)= >H 7" R((r::)) For simplicity, we denote the infinite-horizon return starting from t=0 as G (o) and further drop the sub- script to write G(a):= lim (o). We note that for Markovian reward functions (R:S+R), memoryless policies (T:S++A) suffice. However, the tasks cies. To address this, we reduce the problem of obtaining a finite finite-memory policy to that of learning memoryless policy by augmenting the state space S with memory states, detailed in Sec. The discount factor reduces the value of future rewards to prioritize immediate ones: a reward re- ceived after i steps contributes 7² R(a (f]) to the return. The objective in RI., specifically in policy gradient, is to learn optimal policy parameters 0* =argmaxx.. where =(0)=EE Mr, [G In
consider require finite-memory poli-
differentiable MDPs, RL can leverage first-order gradients v!"l è =0)= [o) where 8GH BG 01 aG aG at Oo. Dos+1 Us.' Dda Des41 da, via BPTT (see also Appx. B C
Labels. We define the set of atomic propositions (APs), denoted by A, as properties of interest that place bounds on functions of the state space. Formally, each AP takes the form a:= (=>=)>>)>''"" where g: S + R is assumed to be differentiable function mapping a given state to a signal. For example, the function (( x)) = x² - x? can be used to define an AP that specifies that the velocity of the i-th component must be below an upper bound x The labeling function I. S - 24 returns the set of APS that hold true for given state. Specifically, an AP a == "g(s) > 0' is included in the
label set L(s) of state s - i.e.. s is labeled by a if and only if (iff) g(s) O. We also write, with a slight abuse of notation, L(a) == (or())) ... to denote the trace (sequences of labels) of path a. Finally, we write M M-MM, L) to denote a labeled MDP.
3

---

Published as a conference paper at ICLR 2026
LTL. LTL provides a high-level formal language for specifying the desired temporal behaviors. Alongside the standard operators in propositional logic negation (-) and conjunction (A) - LTL offers two temporal operators, namely next (O) and until (U). The formal syntax of LTL is defined by the following grammar (Baier & Katoen, 2008::
== true a - 91 A P2 Oip pp Uy2, a E A. The semantics of LTL. formulas are defined over paths. Specifically, path o either satisfies sp, denoted by a + p, or not (a ffr s). The satisfaction relation is defined recursively as (0] (i.e., a immediately holds); if y = - and 1/= q p 41 A 62 and (ar } (21) A (a F 92); if = Φi U2p and there exists t 2 0 such that ft:] F 42 and for all 0 S i < t, ofi F fi. The remaining Boolean and temporal operators can be derived via the standard equivalences such as eventually (Op= == true U (P) and always (0yp == -(0-)))
follows: a = ip if p = and
LDBAs. If a path satisfies a given LTL formula o can be checked by building an LDBA, denoted by Ag that is suitable for quantitative model-checking of MDPs (Sickert et al. 2016). An LDBA is a tuple AQ=(Q. qu: Σ, B) where Q a finite set of states; quEQ is the initial state; Σ=24 is the set labels; 6 Q (XU(E)) + 2 is a transition function triggered by labels; B S Q the accepting states. An LDBA Ag accepts a path a (i.e., =)), iff its trace l((r) induces an LDBA execution visiting some of the accepting states infinitely often, known as the Büchi condition (see Appx. D))
LTL Learning Problem. Our objective is to learn control policies that ensure given path speci- fications are satisfied by given labeled MDP. In stochastic environments, this objective translates to maximizing the probability of satisfying those specifications. We consider specifications given as formulas since L.T. provides a high-level formalism well-suited for expressing safety and other temporal constraints in robotic systems-and, importantly, finite-memory policies suffice to satisfy LTL specifications (Chatterjee & Henzinger 2012). We now formalize the problem as follows:
Problem 1. Given a labeled MDP M and a fTL.ull yp, find an optimal finite memiryy policy Thp that maximizes the probability of satisfying sp, i.e., T.p == argmax Pr Prowad {o a + v): where
II is the set of policies and is a path drawn from the Markov chain (MC) M3 induced by
4 ACCELERATED LEARNING FROM LTL USING DIFFERENTIABLE REWARDS
In this section, we present our approach for efficiently learning optimal policies that satisfy given LTL specifications by leveraging differentiable simulators. We first define product MDPs and dis- cuss their conventional use in generating discrete LTL--bsed rewards for RL. We then introduce our method for deriving differentiable rewards using soft labeling, enabling madient-bbsed optimization while preserving the logical structure of the specifications. We lastly establish a theorem yielding a tunable bound on the discrepancy between discrete and differentiable LTL rewards.
Product MDPs. A product MDP is constructed by augmenting the states and actions of the orig- inal MDP with indicator vectors representing the LDBA states. The state augmentations serve as memory modes necessary for tracking temporal progress, while the action augmentations, referred to as e-actions, capture the nondeterministic s-moves of the LDBA, The transition function of the product MDP reflects a synchronous execution of the LDBA and the MDP; i.e., upon taking an action, the MDP moves new state according to its transition probabilities, and the LDBA transi- tions by consuming the label of the current MDP state.
Definition 2. A product MDP is a tuple M=(S, A, f. Po. B), composed of a labeled MDP M MS= A, J, po, A, L) and an LDBBA (Q= (0 qo, B) derived from an LTL. formula yp such that S Sx Q is the set of product states and A=Ax Q the set of product actions where Q= 1](Q1 is the space set for the one-hot indicator vectors of automaton states; f:Sx defined as
T.SxA-3 A-A is the transition function
(" qu)) L E 5(g's)))
ae $ 5(g',E)
((ss.'") (a, ()
(1)
(88.9%))
for given s, s'S'ES, a. A and the indicator vectors qa, qe e q, q' 9 &Q respectively, where s'==f(s, a) and d'g I(s)): Po is the initial product state distribution where pā ((s, (4));=
B-l(s, 98) qEB) the set of accepting product states. product MDP said to accept product path iff a satisfies the Bücci condition, denoted as o DOB, which is to visit some states in B infinitely often.
By definition, any product path accepted by the product MDP corresponds to a path in the original MDP that satisfies the acceptance condition of the LDBA. Consequently, the satisfaction of the LTL specification y is reduced to ensuring acceptance in the product MDP. This reduces Problem T to maximizing the probability of reaching accepting states infinitely often in the product MDP:
4

---

Published as a conference paper at ICLR 2026
Lemma 1 (from Theorem 3 in (Sickert et al. 2016 A memoryless product policy T' that max- imizes the probability of satisfying the Buchi condition in a product MDP M constructed from a given labeled MDP M and the LDBA A, derived from a given LTL specification yp, induces policy T with a finite-mmmory captured by AG maximizing the satisfaction bncieetiiooroobbbie probability of ip in M+.
Discrete LTL Rewards. The idea to derive LTL rewards from the acceptance condition of the product MDP to train control policies via RL approaches. Specifically, we consider the approach proposed in (Bozkurt et al.) 2024) that uses carefully crafted rewards and state deteedee discount- ing based on the Büchi condition such that an optimal policy maximizing the expected return is also an objective policy n maximizing the satisfaction probabilities as defined in Lemma T which can be formalized as below:
Theorem 1. For a given product MDP M, the expected return for a policy a approaches the probubility of satisfying the Büchi acceptance condition as the discount factor " goes to I; i.e. lim,-1- Eg B, = Pra-M (a = =)B); if the return G(o) is defined as follows:
t-1
[1- 3 SEB
{8 SEB
G(o):= Σ (o) II [[o]), R(s)=
r(s):
(2)
0
sBB
(7 SBB
where IT 3 is a function of satisfying lim 1 = 0, R:SH |0, 1) and r 1::++00.1
state-dependent reward and the discount functions respectively.
The proof can be found in (Bozkurt et al. 2024). The idea is to encourage the agent to repeatedly visit an accepting state many times as possible by assigning larger reward to the accepting states. Further, the rewards are discounted with a larger factor in non-accepting states to reflect that the number of visitations non-accepting states by this approach, however, are very sparse; depending on the environment and the structure of the automaton, the agent might need to blindly explore a large portion of the state space before getting a nonzero reward, which constitutes the main hurdle in learning from LTL specifications.
important. The L.TL rewards provided
Differentiable LTL Rewards. We propose employing differentiable RL algorithms and simu- lators to mitigate the sparsity issue and accelerate learning. However, the standard LTL rewards described earlier are not only sparse but discrete, rendering them non-differentiable with respect to states and actions. This lack of differentiability primarily stems from two factors: the binary state-based reward function and discrete automaton transitions. To address this challenge, we troduce probabilistic "soft" labels. We start by defining the probability that given AP, denoted as a = "g()) > 0", belongs to the label L(s) of state 8. Formally:
1
Pr(a E I(s))= Pr(g(s) 0) = h(g(s)) 1 exp(-g(s))
Although we use the widely adopted sigmoid function here ! any differentiable cumulative distribu- tion function (CDF) h IK + [0, 1] could be applied. Building upon these probabilities, we define the probability associated with a label as follows:
(r(((s) = I) III Pr(a e L(s)) II [1- Pr(a e L(s))).
(4)
aEt
ag!
These probabilistic labels induce probabilistic automaton transitions, causing the controller to ob- serve automaton states probabilistically. Consequently, instead of modeling automaton states as deterministic indicator vectors in product MDPs, we represent them as probabilistic superpositions over all possible automaton states. By doing so, we design differentiable transitions and rewards within the product MDP. Let fr. S'xQ + Q denote the function that updates the automaton state probabilities based on the LDBA transitions triggered by probabilistic labels, and Iet q denote the vector where each element qg is the probability of being in automaton state q. then can define:
[I((s, q)) = =q' where L/
> (I) and Lgq. = (
(5)
IEL.,0
Intuitively, the probability of transitioning to a subsequent automaton state o' is computed by sum- ming probabilities across all current automaton states q and labels E T.q.q'' capable of leading to state q'. This computation can be efficiently done through differentiable matrix multiplication.
The remaining hurdle is the binary e-actions available to the controller, which trigger e-transitions in the LDBA. Similarly to the soft labels approach, E-actions can become differentiable by representing
For the correctness of I.TI,, Pr(g(s) > 0) must be exactly 0 or for values helow above certain thresh- olds, In practice, this is not an issue, overflow behavior of sigmoid ensures this condition is satisfied.
5

---

Published as a conference paper at ICLR 2026
0.4
Gradent
0.6
0.0
0.4
-0.2
0.2
0.0
-0.6
9 ogpark
Cmyrass
0.0
7.5 Deceleration rationaioo (msts")
2.5
5.0
10.0
0.0
7.5 Deceleration (m))e)
2.5
5,0
10.0
Satisfaction Probability
Return (Discrete
Return IDifferentiable
Figure I: LTL Returns and Derivatives. Left: The parking scenario where the car must brake to stop in the parking area without entering the grass field (4p)) Middle: L.TI. satisfaction probability and return estimates from discrete and differentiable LTL formulations as functions of deceleration. Right: LTL return gradients with respect deceleration and their standard deviation. The key challenge in learning from LTL arises from slightly-slope regions and sharp changes in the returns produced by discrete LTL rewards. Our differentiable LTL approach not only smooths these abrupt changes but also enables the use of low-variance first-order gradient estimates essential for effective learning in alihhty-sloper regions.
the probabilities of the e-transitions to be triggered. Let f& Q Q Q denote the function up- dating automaton state probabilities based on the e-action taken, and let q denote the vector whose elements indicate the probabilities of taking the E-actions leading to the corresponding automaton states, we then define:
fe q") = q' where df En Enn ( Qu:ci-aa ( (6)
qEQuo'
gEQq.e
Conceptually, the probability of transitioning automaton state of involves two scenarios: (the first summation in (6)) the probability of moving to q' via valid e-transitions, and (the second summation in (6)) the probability of remaining in q' after trying leave from q' via nonexistent e-transitions. These vector computations can be efficiently performed in differentiable manner. We can formulate the complete transition function f by composing fL. fe, and f as follows:
(7) This transition function first executes the E-actions, then performs the LDBA transitions triggered by state labels to update the automaton state probabilities, while applying the given action to update the MDP states. The function f fully differentiable with respect 8, q. a, and q.. We can now obtain reward Ri Q ~ (0. 1) and a discounting function D Q + (0. 1) that are also differentiable with respect to states and actions as follows:
f((s, q) (a, ) = (f(s, a), fr((s, fe fe ))))))
R((s, )) = (1 3) Σnn 4g D(g)
Σ 4g
+
Σ 4g
qEB
9EB
q&B
These differentiable reward and discounting functions allow us to obtain first-order gradient esti- mates (0) E,,,,, [V)G which are known to exhibit lower variance compared to zeroth-order estimates (Xu et al. 22022. Such first-order estimates can be effectively utilized by dif- ferentiable RI. algorithms to accelerate learning. In the following example, we illustrate employing these lower-variance gradient estimates is particularly crucial when learning from LTL rewards.
Parking Example. Consider parking scenario in which the vehicle starts with initial velocity of = 10 m/s. The controller applies the brakes with constant deceleration E [0 m/s² 10 m/s3] over the next 10 seconds, with the goal of bringing the car to rest inside the parking area. For safety, the vehicle must not enter the grass field before reaching the parking zone the right-hand side. We formalize these requirements in LTL as 9p- 0pprk A U-grass where the parking area and the grass field are defined as park (x> 10 m x< m) V (x>30 30 A x0 m) and grass == >020 m A xx m, respectively.
Fig. [ Iillstraate this task, including satisfaction probabilities. returns, and gradients with respect to decelcration. The satisfaction probability is for deceleration values between 2.5 m/s? and 5.0 m/s? and outside this range. The differentiable LTL returns closely match the discrete ones, except near the boundaries of the satisfaction region, where the differentiable version produces smoother tran- sitions. This smoothness is particularly evident in the gradient plots. Although differentiable LTL. rewards yield smoother return curves, learning remains challenging due the small gradient mag- nitudes across most of the parameter space except near the satisfaction boundaries. For instance, in the region between 0.0 m/s² and 2.5 m/s?, the returns increase with deceleration, but noisy gra- dient estimates still lead the learner away from the satisfaction region. Therefore, obtaining

---

Published as a conference paper at ICLR 2026
low-variance gradient estimates is especially beneficial when learning from LTL, where most of the landscape requires sharper gradients for effective optimization. See Appx. for comparison.
Discrete vs. Differentiable LTL Rewards. We now show that the maximum discrepancy between the discrete and differentiable values can be upper-bounded for a given tolerance parameter Ç and an activation function h in the theorem below. Since, by Theorem [ the discrete values converge the satisfaction probabilities, the bound is also valid in the limit for the actual satisfaction probabilities. Theorem 2. Let & be the tolerance on the signal bounds of atomic prepositions, and let be the probability associated with & (i.e., p = Pr(s 0) h(()) in d3y. Let Gdine and Gdiff de- note the returns obtained via discrete and differentiable rewards, respectively. Then the maximum discrepancy between them is upper bounded as:
Gliss (o) Griff (a)l
(
1+ (1-p)ia)
1+ (1-ble))
where B is the discount factor factor for accepting states, defined in (8). By linearity of expectation, this result immediately extends to the expected return (values) in stochastic environments; i.e,, the upper bound above holds for E [ddisss (o)) E (o)]l where expectations are over trajectories drawn under any given policy.
Proof. The maximum discrepancy between G and Gullft. occurs when all probabilistic transitions associated with soft labels yield positive differentiable rewards while their corresponding discrete rewards are zero (or vice versa). For given tolerance s, the probability of incorrectly evaluating all atomic propositions under soft labels is p == (1-p) where denotes the set of all atomic propositions defined in the LTL grammar. In this worst-case scenario, the differentiable return for trajectory a, where all such transitions lead to accepting states, is:
00
(o) S Σ p)
P
(- (1 p)B (1- + p3
1
1-8
1
1-8
P
(T-p)aT
Since ddise 0, this expression provides the upper bound on the maximum discrepancy.
EXPERIMENTS
In this section, through simulated experiments, we show learning from differentiable LTL rewards offered by our method is significantly faster than learning from discrete LTL rewards.
Implementation Details. We implemented our ap- proach in Python utilizing the PyTorch-based differen- tiable physics simulator dFlex introduced in Xu et al. (022). We used an NVIDIA GeForce RTX 2080 GPU, 4 Intel(R) Xeon(R) Gold 5218 CPU cores, and 32 gigabytes memory for each experiment. Specifi- cally, we generate the automaton description using Owl (Kretinsky et al. 2018) and parse it using Spot (Duret- Lutz al. 2016). We then construct reward and tran- sition tensors from the automata. We then compute the probabilities for each observation
Algorithm Differentiable RL with LTL
Require: MDP M. LTL formula y. Policy xo Derive LDBA Ag and APs from yp Derive f t and St, @ x from A,
while True
for i 1,,,.... do Initialize (0))~ (00 ~M) G+D for f 1,2, ..., 11 do
Get action (a. q²) ~ no (t11)) Exccute s-action
(..)))))
(q.9')
Exccute label transition q )
Exccute MDP
(())
(1)
explained in the previous section using a sequence of differentiable vector operations via PyTorch. Lastly, using the con- structed transition and reward tensors, we update the automaton states and provide rewards. The overall ap- proach is summarized in Algorithm[I]
Compute reward y 9i (t)
Update return GP G/2 + (g))
end for end for Calculate +0 ((0) 2 ΣN V.G(( Train my using 6 J(0) while
Baselines. We use two widely adopted and representative of-te--f-thee-rr (SOTA) model-free RL algorithms as our baseline non-dit non-differentiable RL methods (ØRLs): the on-policy Proximal Policy Optimization (PPO) (Schulman al. 2017) and the off-policy Soft Actor-Critic (SAC) (Haarnoja et al. 2018). For differentiable RL baselines (ØRLs), we employ SHAC and AHAC, which, to the best of our knowledge, represent the SOTA in this category. For each environment and baseline, we used the tuned hyperparameters from Georgiev et al. (2024).
Metric. We evaluate performance in terms of the collected LTL rewards averaged over 5 seeds since they can serve as proxies for satisfaction probabilities. We considered two criteria: (1) the maximum return achieved and (2) the speed of convergence. To maintain consistency, we used differentiable LTL rewards across all baselines as, for non-differentiable baselines, we observed no performance difference between the differentiable and discrete LTL rewards.
7

---

Published as a conference paper at ICLR 2026
Neturn (U Sat Prot ESt.
CartPole
Hopper
Choctah
Ant
2
20
60
Max
60
Max
Max 40
Max
Steps (M)
SHAC AHAC (9)
(ma)
(-a)
Comparison Across Environments: Differentiable vs. Discrete LTL Rewards. The wider plots show the learning curves of all baseline algorithms, while the narrower plots on the right display the maximum returns achieved after 100 M steps. All results are averaged over 5 random seeds, and the curves are smoothed using max and uniform filters for visual clarity. The reported returns, bounded between 0 and serve as proxies for the probability of satisfying the LTL specifications. In all the environments, algorithms utilizing differen- tiable LTL rewards (SHAC, AHAC) rapidly learn near-optimal policies, whereas those relying on discrete LTL rewards (PPO, SAC), display high variance, converge slowly, or are stuck with sub-optimal policies.
Figure 2:
CartPole. The CartPole environment consists of a cart that moves along a one-dimensional track, with pole hinged to its top that can be freely rotated by applying torque. The system yields a 5-dimensional observation space and a 1-dimensional action space. The control objective is to move the tip of the pole through sequence of target positions while maintaining the cart within desired region as much as possible and ensuring the velocity of the cart always remains within safe boundaries. We capture these requirements in LTL follows:
Peampole c'crrt serrttvx//or vx|
ccart x <20 A O O'Ipole.z-20
(pole 2-21/<A)
safety
repetition
reachability soquencing
Here, cart_x, cart-vx, and pole_z represent the cart position, the cart velocity, and the pole height respectively. This formula demonstrates how LTL can be leveraged to encode both complex safety constraints and performance objectives. We set Zu 10 m. 2/ 10 m/s as boundaries, 20 = -1 m, 21 = m as the target positions, and A 25 em as the allowable deviation.
Legged Robots. We consider three legged-robot environments: Hopper, Cheetah, and Ant. The Hopper environment features one-legged robot with components and 3 joints, resulting 10- dimensional state space and a 3-dimensional action space. The Cheetah environment consists of a two-legged robot with 8 components and 6 joints, yielding a 17-dimensional state space and 6-dimensional action space. The Ant environment includes a four-legged robot with 9 components and joints, producing 37-dimmesioo state space and 8-dimensional action space. In all three environments, the control task requires always keeping the torso/tip of the rohot above critical safety height, maintaining a certain distance between the torso/tip and the critical height as often as possible, and accelerating the robot forward, and then bringing the robot to full stop. We formalize this task in LTL as follows:
Plegeed O'torso 2>26 1l'torso 2>2i A O vx>'''1''orss vx<en).
(10)
safeey
repetition
renchaiiltty & sequencing
Here, torso and torso vx denote the height and horizontal velocity of the robots. This for-
mula captures several key aspects I.TI., including, safety, reachability, sequencing, and repetition. The values of zg and ž1 were chosen based on the torso height of each robot in their referential system. Specifically, we used 2g = -110 cm, 21 = --05 em for Hopper; 2g = -75 cm, 21 -70 for Cheetah; and 2g 0 cm, 21 = 5 em for Ant, where zo denotes the critical safety height and 21 represents a safe margin above it. We set 0 = 1 m/s, V1 = 3 m/s, and 01 = 1.5 m/s for Hopper, Cheetah, and Ant, respectively, reflecting movement speeds relatively challenging yet achievable for each the robots. For deceleration, we set Up = m/s for all the environments. An illustration of a policy learned from this specification for Cheetah is provided in Fig. in Appx. F
Results. Fig. presents our simulation results. Across all environments. ØRL algorithms that leverage our differentiable LTL rewards consistently outperform ØL algorithms terms of both maximum return achieved and learning speed from the LTL specifications.
CartPole. The safety specification induces automaton with three states, each having 64 transitions-but only one of these transitions yields a reward. This extreme sparsity, even in a low- dimensional state space, severely hinders the learning process for øRLs, shown in the leftmost plot of Fig. 2 contrast, ØRL algorithms leverage the gradients provided by differentiable rewards, en- abling them to efficiently learn policies that nearly satisfy the LTL specification. Specifically, ØRLs converge to optrnoptimal policies (Pr>0.8) within just 20 M steps, whereas ØRLs (SAC: all seeds; PPO: one seed) fail learn any policy that achieves meaningful reward, even after 100 M steps.
8

---

Published as a conference paper at ICLR 2026
Legged Robots. As we move to environments with higher- nigher-dimensional state spaces- 10, 17, and 37 dimensions for Hopper, Cheetah, and Ant, respectively even relatively simple LTL specifications pose a significant challenge for RLLs The automata derived from the LTL specifications in these environments consist of four states, each with 16 transitions, of which four transitions in the third state yield rewards. Reaching this state, however, requires extensive blind exploration of the state space, making it significantly harder for øRLs to learn optimal control policies. On the other hand, öRLs, guided by LTL reward gradients, quickly identify high-reward regions of the state space and learn effective policies.
evenn
For Hopper. aRLs converge to near-optimal policies (Pr>0.8) within 20 M steps. while PPO requires the full 100 M steps to converge, and one SAC seed gets trapped in a local optimum. For Cheetah, ØRLs attain optimal performance (Pr>0.9), whereas PPO converges to a suboptimal policy even after 100 M steps, and SAC consistently fails by getting stuck in poor local optima. For Ant, ORLs again learn near-optimal policies rapidly, while @RLs converge only to suboptimal policies.
rewards differen- tiable and can therefore be readily applied to frameworks such as RMs. We conducted analogous experiments in the Cheetah environment described in Icarte et al. (0022). Specifically, we used the same RMs from TASK 1 and TASK 2 and made them differentiable with method. We then trained policies using the SHAC algorithm. Table in Appx. G reports the returns obtained with the differentiable RMs alongside the best returns reported in Figure 10 of lcarte al. (2022). Our differentiable RM-based approach significantly outperforms all discrete RM baselines.
Generalization to Reward Machines. Our approach renders automaton-
Ablation Study. To isolate the impact of LTL. reward differentiability from inherent algorithm and environment properties, we conducted two ablation studies. First, trained SHAC and AHAC with discrete LTL rewards. The corresponding learning curves are shown in Fig. / in Appx. H We observe a substantial performance degradation across all environments: the performance of SHAC/AHAC with discrete LTL rewards is markedly lower than with differentiable ones, and is mostly lower than that of PPO and SAC. The performance drop is especially pronounced in the nigher-dimensional environments, Cheetah and Ant, where no reasonable policy is obtained. This suggests that the strong performance of ØRLs in Fig. i primarily due to our differentiable LTL rewards. Second, we trained each approach under simplified versions of the LTL formulas (21) in Appx. HD lacking the complexity that makes learning from LTL challenging. Each algorithm even- tually learns optimal policy (Pr > 0.9) for all environments (see Fig. 8 in Appx. (H.. These results support the conclusion that the lower performance of ØLLs in Fig. 2 arises primarily from their inability to handle complex LTL formulas as effectively ØRLs with our differentiable rewards, rather than from mavironment-ppeciff properties.
6 CONCLUSION
In this work, we tackle the challenge of scalable RL for temporally extended and formally speci- fied tasks. By adopting LTL as our specification framework, we ensure objective correctness and avoid the ceward-misspecfficationn issues common in conventional RL. To overcome the learning in- efficiencies caused by sparse logical rewards, we introduce a method that leverages differentiable simulators, enabling gradient-based learning directly from LTL objectives without compromising expressiveness or correctness. Our approach employs soft-labeling techniques that preserve differ- entiability through the transitions of automata derived from LTL formulas, yielding an end-to-end differentiable learning framework. Across simulated experiments, we show that our framework substantially accelerates learning compared to state-of-the-ar non-differentiable baselines, pointing toward more reliable and scalable deployment of autonomous systems in real-world environments. Our approach accelerates learning from LTL specifications by leveraging differentiable RL algo- rithms and gradients provided by differentiable simulators. Consequently, the overall performance of our method is inherently tied to the quality and efficiency of the underlying simulators and RL algorithms, and cannot be directly extended to discrete MDPs. A further consideration is that our method introduces an additional hyperparameter, the activation function used for probability esti- mation, which should be tuned for optimal performance. Another challenge lies in the formaliza- tion of LTL specifications: while LTL offers a more intuitive and structured way to specify tasks than manual reward engineering, it still requires familiarity with formal logic and sufficient domain knowledge to define meaningful bounds. An immediate direction for future work is to combine our approach with other techniques such as counterfactual experience replay and barrier nets. Another direction is to design LTL-specific differentiable RL methods that exploit the compositional struc- ture of the automata enable efficient exploration and transfer. See Appx. [oor further discussion.

---

Published as a conference paper at ICLR 2026
ETHICS STATEMENT
This work complies with the ICLR Code of Ethics. All experiments in this study were conducted exclusively in simulated environments; therefore, no human participants, sensitive data, or real- world deployments were involved, thereby eliminating ethical risks associated with those settings.
REPRODUCIBILITY STATEMENT
The source code needed to reproduce the results reported in this manuscript is included in the sup- plementary material, together with a README. md explaining the required steps. Upon acceptance, we will make the complete source code publicly available.
ACKNOWLEDGMENTS
This work is supported in part by NSF-EFRI #2422282, IARPA HAYSTAC, Brendan Iribe Endowed Professorship, Dr. Barry Mersky and Capital One E-Nnovte Endowed Professorships, University of Maryland Distinguished University Professorship, and ARL-UMD ArtIAMAS Cooperative Agree- ment. We sincerely thank all the reviewers for their detailed and constructive feedback.
REFERENCES
Derya Aksaray, Austin Jones, Zhaodan Kong, Mac Schwager, and Calin Belta. Q-learning for robust satisfaction of signal temporal logic specifications. 2016 IEEE 55th Conference on Decision and Control (CDC), pp. 6565-6570. IERE, 2016.
Dario Amodei, Chris Olah, Jacob Steinhardt, Paul Christiano, John Schulman, and Dan Mané. Con- crete problems in ai safety. arXiv preprint arXiv: 160.60666666 2016.
OpenAl: Marcin Andrychowicz, Bowen Baker, Maciek Chociej. Rafal Jozefowicz, Bob McGrew, Jakub Pachocki, Arthur Petron, Matthias Plappert, Glenn Powell, Alex Ray, al. Learning dexterous in- hand manipulation. The International Journal of Robotics Research, 39(1):3-20, 2020.
Szilárd Aradi. Survey of deep reinforcement learning for motion planning of autonomous vehicles. IEEE Transactions Intelligent Transportation Systems, 23(2):740-755 2022.
Kai Arulkumaran, Marc Peter Deisenroth, Miles Brundage, and Anil Anthony Bharath. Deep rein- forcement learning: A brief survey. IEEE Signal Processing Magazine, 34(6):26-38, 2017.
Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. MIT Press, Cambridge, MA, USA, 2008
Felix Berkenkamp, Matteo Turchetta, Angela P Schoellig, and Andreas Krause. Safe model-based reinforcement learning with stability guarantees. NIPS, 2017. doi: 10.48550/arxiv.177 110t 1705.0551..
Alper Kamil Bozkurt. Toward Assured Autonomy With Model-Free Reinforcement Learn- ing. PhD thesis. Duke University. 2024. URL https: www. http:://wwwwwwouuut.t.eot
com/
pesserttaiion--theessses http://ttwaaaaasueeeeeeeeeeeeeee wtt.eeeaaotooooootwii----ooooooo free/ wttpee//////111///eeee
Copyright Database copyright ProQuest I.CC; ProQuest does not claim copyright the individual underlying works; Last updated 2024-06-16.
Alper Kamil Bozkurt, Yu Wang, Michael M. Zavlanos, and Miroslav Pajic. Control synthesis from linear temporal logic specifications using model-free reinforcement learning. In Proceedings of the 35th International Conference on Robotics and Automation (ICRA), pp. 10349-10355, 2020a.
Alper Kamil Bozkurt, Yu Wang, Michael M. Zavlanos, and Miroslav Pajic. Control synthesis from linear temporal logic specifications using model-free reinforcement learning. In International Conference on Robotics and Automation (ICRA), pp. 10349-10355, 2020b.
Alper Kamil Bozkurt, Yu Wang, and Miroslav Pajic. Secure planning against stealthy attacks via model-free reinforcement learning. In International Conference on Robotics and Automation (ICRA), pp.
IEEE, 2021a.
10

---

Published as a conference paper at ICLR 2026
Alper Kamil Bozkurt, Yu Wang, Michael M. Zavlanos, and Miroslav Pajic. Model-free reinforce- ment learning for stochastic games with linear temporal logic objectives. In International Con- ference Robotics and Automation (ICRA), pp. 10649-10655, IEEE, 2021b.
Alper Kamil Bozkurt, Yu Wang, Michael M. Zavlanos, and Miroslav Pajic. Learning optimal con- trollers for temporal logic specifications in stochastic games. Transactions on Automatic Control (TAC), 2024.
Tomáš Brázdil, Krishnendu Chatterjee, Martin Chmelik, Vojtëch Forejt, Jan Kictinský, Marta Kwiatkowska, David Parker, and Mateusz Ujma. Verification of Markov decision processes using learning algorithms. In Proceedings of the 12th International Symposium on Automated Technol- ogy for Verification and Analysis, pp. 98 14, 2014.
Mingyu Cai, Mohammadhosein Hasanbeig, Shaoping Xiao, Alessandro Abate, and Zhen Kan. Mod- ular deep reinforcement learning for continuous motion planning with temporal logic. RA-L, (4):7973 -9800, 2021a. ISSN 2377-3766.
doi: 10.1 10.1109//r..0211110000
Mingyu Cai, Shaoping Xiao, Baoluo Li, Zhiliang Li, and Zhen Kan. Reinforcement learning based temporal logic control with maximum probabilistic satisfaction. ICRA, 00:806-811 2021b. doi: 10.1 (0.1009/cra44506.2000 2021 9511599988000002229999990000
Mingyu Cai, Erfan Aasi, Calin Belta, and Cristian-Ioun Vasile. Overcoming exploration: Deep re- inforcement learning for continuous control in cluttered environments from temporal logic speci- fications. RA-L., ((4):2158-2166) 2023a. ISSN 2377-3766. doi: 10.1 109//09..r... 2023.3246844.
Mingyu Cai, Shaoping Xiao, Junchao Li, and Zhen Kan. Safe reinforcement learning under temporal logic with reward design and quantum action selection. Scientific Reports, 13(1):1925, 2023b. doi: (0008//41598-022-25555555
Alberto Camacho, Rodrigo Toro Icarte, Toryn Q Klassen, Richard Anthony Valenzano, and Sheila A Mcllraith. Ltl and beyond: Formal languages for reward function specification in reinforcement learning. In IJCAI, volume 19, pp. 6065-6077 2019.
Justin Carpentier and Nicolas Mansard. Analytical derivatives of rigid body dynamics algorithms. RSS, 2018. doi: 10. 20.15567//ss.2118.vvvvoo
Krishnendu Chatterjee and Thomas A. Henzinger. A survey of stochastic w-regular games. Journal of Computer and System Sciences, 4832):394-413, 2012.
Yu Fan Chen, Michael Everett, Miao Liu, and Jonathan P How. Socially aware motion planning with deep reinforcement learning. In 2017 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), pp. 1343-1350. IEEE, 2017.
Richard Cheng, Gabor Orosz, Richard M. Murray, and Joel W. Burdick. End-to-end safe reinforce- ment learning through barrier functions for safety-critical continuous control tasks. AAAI, 2019.
Yinlam Chow, Ofir Nachum, Edgar Duenez-Guzman and Mohammad Ghavamzadeh. A Iyapunov- based approach to safe reinforcement learning. Advances in neural information processing sys- tems, 31, 2018.
Bohan Cui, Keyi Zhu, Shaoyuan Li, and Xiang Yin. Security reinforcement learning under linear temporal logie specifications. ICRA, 00:12367-123777 2023. doi: 10.1 10.1109/ir2448891.2222 10160753.
Jingjing Cui, Yuanwei Liu, and Arumugam Nallanathan. Multi-agent reinforcement learning- resource allocation for uav networks. IEEE Transactions on Wireless Communications, 19(2): 729-743, 2019.
Rongxin Cui, Chenguang Yang, Yang Li, and Sanjay Sharma. Adaptive neural network control of auvs with control input nonlinearities using reinforcement learning. IEEE Transactions on Systems, Man, and Cybernetics: Systems, 1009 2017.

---

Published as a conference paper at ICLR 2026
Dongsheng Ding, Xiaohan Wei, Zhuoran Yang, Zhaoran Wang, and Mihailo Jovanovic. Provably efficient safe exploration via primal-dual policy optimization. In International conference on artificial intelligence and statistics, pp. 3304-3312. PMLR, 2021.
Tao Du, Kui Wu, Pingchuan Ma, Sebastien Wah, Andrew Spielberg, Daniela Rus, and Wojeiech Matusik. DiffPD: Differentiable projective dynamics. TOG, 41(2)11-21, 2021. ISSN 0730-0301. doi: 00.11453349016.
Alexandre Duret-Lutz, Alexandre Lewkowicz, Amaury Fauchille, Thibaud Michaud, Etienne Re- nault, and Laurent Xu. Spot 2.0-a framework for Itl and-automata manipulation. In Proceed- ings of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA), pp. 122-129, 2016.
C. Daniel Freeman, Erik Frey, Anton Raichuk, Sertan Girgin, Igor Mordatch, and Olivier Bachem. Brax- differentiable physics engine for large scale rigid body simulation. NeurlPS, 2021.
Jie Fu and Ufuk Topeu. Probably approximately correct MDP learning and control with temporal logic constraints, 2014a. arXiv:1404.7073 [cs.SY].
Jie Fu and Ufuk Topcu. Probably approximately correct MDP learning and control with temporal logic constraints. In Robotics: Science and Systems Conference, 2014b.
Javier Garcia and Fernando Fernández. A comprehensive survey on safe reinforcement learning. Journal of Machine Learning Research, 16(1):1437-1480) 2015.
Moritz Geilinger, David Hahn, Jonas Zehnder, Moritz Bacher, Bernhard Thomaszewski, and Stelian Coros. ADD: Analytically differentiable dynamics for multi-body systems with frictional contact. TOG, 2020.
Ignat Georgiev, Krishnan Srinivasan, Jie Xu, Eric Heiden, and Animesh Garg. Adaptive horizon actor-critic for policy learning in contact-rich differentiable simulation. ICML, 2024. doi: 10. 48550/arxiv22055. 17784.
Ian Goodfellow, Yoshua Bengio, and Aaron Courville. Deep learning. MIT press. 2016.
Tuomas Haarnoja, Aurick Zhou, Kristian Hartikainen, George Tucker, Sehoon Ha, Jie Tan, Vikash Kumar, Henry Zhu, Abhishek Gupta, Pieter Abbeel, et al. Soft actor-critic algorithms and appli- 2018.
cations. arXiv preprint (rXXiv:8822.055
Ernst Moritz Hahn, Guangyuan Li, Sven Schewe, Andrea Turrini, and Lijun Zhang. Lazy probabilis- tic model checking without determinisation. In Proceedings of the 26th International Conference on Concurrency Theory (CONCUR), pp. 354, 2015.
Ernst Moritz Hahn, Matco Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, and Dominik Wojtczak. Omega-regular objectives in model-free reinforcement learning. In Proceedings of the 25th International Conference on Tools and Algorithmss for the Construction and Analysis of Systems (TACAS), pp. 395-412, 2019.
Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, and Dominik Wojtczak. Model-free reinforcement learning for stochastic parity games. In 31st International Conference on Concurrency Theory (CONCUR 2020). Schloss Dagstubl-Leibniz--eentu für Informatik, 2020.
Hosein Hasanbeig, Daniel Kroening, and Alessandro Abate. Certified reinforcement learning with logic guidance. Artificial Intelligence, 322: 103949, 2023. ISSN 0004-3702. doi: 10.10166/.artinn 2023.103949.
Mohanmadhosein Hasanbeig, Yiannis Kantaros, Alessandro Abate, Daniel Kroening, George J Pap- pas, and Insup Lec. Reinforcement learning for temporal logic control synthesis with probabilistic satisfaction guarantees, 2019. arXiv:1909
05304 190.05040 [cs.LO].
Eric Heiden, Miles Macklin, Yashraj Narang, Dieter Fox. Animesh Garg, and Fabio Ramos. DiSECt: A differentiable simulation engine for autonomous robotic cutting. RSS, 2021. doi: 10.15607/rss. 2021.xo0 2v11xxvii067..
12

---

Published as a conference paper at ICLR 2026
Kai-Chieh Hsu, Vicenç Rubies-Royo Claire Tomlin, and Jaime F Fisac. Safety and liveness guarantees through reach-avoid reinforcement learning. RSS, 2021.
Yuanming Hu, Jiancheng Liu, Andrew Spielberg, Joshua B. Tenenbaum, William T. Freeman, Jia- jun Wu, Daniela Rus, and Wojeiech Matusik. ChainQueen: A real-time differentiable physical simulator for soft robotics. ICRA, 00:6265-6271, 2019. doi: 10. 10.1109/icra.2111 20t...99999.89935
Yuanming Hu, Luke Anderson, Tzu-Mao Li, Qi Sun, Nathan Carr, Jonathan Ragan-Kelley, and Frédo Durand. DiffTaichi: Differentiable programming for physical simulation. ICLR, 2020. doi: 10048550amxx.11100009333
Zhiao Huang, Yuanming Hu, Tao Du, Siyuan Zhou, Hao Su, Joshua B Tenenbaum, and Chuang Gan. PlasticineLab: A soft-body manipulation benchmark with differentiable physics. ICLR, 2021. doi: 10448500amii.2100..3311..
Jemin Hwangbo, Joonho Lee, Alexey Dosovitskiy, Dario Bellicoso, Vassilios Tsounis, Vladlen Koltun, and Marco Hutter. Learning agile and dynamic motor skills for legged robots. Science Robotics, 4(26):caau5872, 2019.
Rodrigo Toro Icarte, Toryn Klassen, Richard Valenzano, and Sheila Mcllraith, Using reward ma- chines for high-level task specification and decomposition in reinforcement learning. In Interna- tional Conference on Machine Learning, pp. 2107-2116 PMLR, 2018
Rodrigo Toro Icarte, Toryn Q Klassen, Richard Valenzano, and Sheila A McIlraith. Reward ma- chines: Exploiting reward function structure in reinforcement learning. JAIR, 2022.
Mathias Jackermeier and Alessandro Abate. Deepltl: Learning to efficiently satisfy complex Itl specifications for multi-task rl. In International Conference on Learning Representations, 2025.
Yiannis Kantaros. Accelerated reinforcement learning for temporal logic control objectives. IROS, 00:5077-5082, 2022. doi: 10. 00.11099roo47761222222..999
Ravi Kiran, Ibrahim Sobh, Victor Talpaert, Patrick Mannion, Ahmad A Sallab, Senthil Yoga- mani, and Patrick Pérez. Deep reinforcement learning for autonomous driving: A survey. IEEE Transactions on Intelligent Transportation Systems, 2396):490--4926, 2021.
Jens Kober, J Andrew Bagnell, and Jan Peters. Reinforcement learning in robotics: A survey, The International Journal of Robotics Research, 32(11):228--1244 2013.
Jan Kretínský, Tobias Meggendorfer, and Salomon Sickert. Owl: A library for w-words, automata, and LTL. In Proceedings of the 16th International Symposium on Automated Technology for Verification and Analysis (ATVA), volume 11138 LNCS, pp. 543-550, 2018.
Xuan- Bach Le, Dominik Wagner, Leon Witzman, Alexander Rabinovich, and Luke Ong. Reinforce- ment learning with LTL and $) omegaS-regulan objectives via optimality-peesevving translation to average rewards. NeurIPS, 2024. doi: (0.48550/arxix.2410.222
Yann LeCun, Yoshua Bengio, and Geoffrey Hinton. Deep learning. nature, 521(7553):4664444 2015.
Joonho Lee, Jemin Hwangbo, Lorenz Wellhausen, Vladlen Koltun, and Marco Hutter. Learning quadrupedal locomotion over challenging terrain. Science robotics, 5(47)eeabc5986, 2020.
Karen Leung, Nikos Aréchiga, and Marco Pavone. Backpropagation through signal tempo- ral logic specifications: Infusing logical structure into gradient-based methods. The Interna- tional Journal of Robotics Research, 42(6))356-370, 2023. ISSN 0278-3649. doi: 10.1177/
02783649221082115.
Sergey Levine, Chelsea Finn, Trevor Darrell, and Pieter Abbeel. End-to-end training of deep visuo- motor policies. The Journal of Machine Learning Research, 17(1):1334-137) 2016.
Xiao Li, Cristian- 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.
13

---

Published as a conference paper at ICLR 2026
Xiao Li, Zachary Serlin, Guang Yang, and Calin Belta. A formal methods approach to inter- pretable reinforcement learning for robotic planning. Science Robotics, 4(37), 2019. doi: 10.1 10.1116/scirroootess..o htwp:/rrrooreeee..66....... aay6276.
Junbang Liang, Ming C. Lin, and Vladlen Koltun. Differentiable cloth simulation for inverse prob- lems. NeurlPS, pp. 1-22, 2019, ISSN 0066-5452. doi:
Chi Harold Liu, Zheyu Chen, Jian Tang, Jie Xu, and Chengzhe Piao. Energy-efficies uav control for effective and fair communication coverage: A deep reinforcement learning approach. IEEE Journal on Selected Areas in Communications, 36(9):2059-2770, 2018.
Huimin Lu, Yujie Li, Shenglin Mu, Dong Wang, Hyoungseop Kim, and Seiichi Serikawa. Motor anomaly detection for unmanned aerial vehicles using reinforcement learning. IEEE Internet of Things Journal, 5(4):2315-2322) 2018.
Yue Meng and Chuchu Fan. Signal temporal logic neural predictive control. RAL, 8(1):7719-77777 2023. ISSN 2377-3766. doi: 10. 20033333322
Luke Metz, C Daniel Freeman, Samuel $ Schoenholz, and Tal Kachman. Gradients are not all you need. arXiv preprint arXiv:2111.058833 2021.
Volodymyr Mnih, Koray Kavukcuoglu, David Silver, Andrei A. Rusu, Joel Veness, Marc G. Belle- mare, Alex Graves, Martin Riedmiller, Andreas K. Fidjeland, Georg Ostrovski, et al. Human-level control through deep reinforcement learning. Nature, 518(7540):529 -23--33,,, 2015.
Paavo Parmas, Carl Edward Rasmussen, Jan Peters, and Kenji Doya. Pipps: Flexible model-based policy search robust to the curse of chaos. In International Conference on Machine Learning, pp- 4065-4074. PMLR, 2018.
Haixia Peng and Xuemin Shen. Multi-agent reinforcement learning based resource management in mec-and uav-assisted vehicular networks. IEEE Journal on Selected Areas in Communications, 39(1):131-141 2020.
Mateo Perez, Fabio Somenzi, and Ashutosh Trivedi. PAC learning algorithm for LTL and omega- regular objectives in MDPs. 3AA,38811):21510221511 2024. ISSN 2374-3468. doi: 10. 1609 aaai.v38i19.30144
Yi-Ling Qiao, Junbang Liang, Vladlen Koltun, and Ming C Lin. Efficient differentiable simulation of articulated bodies. ICML, 2021. doi: 10448500arxxx2100..7777
Zengyi Qin, Kaiqing Zhang, Yuxiao Chen, Jingkai Chen, and Chuchu Fan. Learning safe multi- agent control with decentralized neural barrier certificates. ICLR, 2021. doi: 10.48550/arxiv. 2101.05436.
John Schulman, Filip Wolski, Prafulla Dhariwal, Alec Radford, and Oleg Klimov. Proximal policy optimization algorithms. arXiv preprint arXiv: 2017.
Daqian Shao and Marta Kwiatkowska. Sample efficient model-free reinforcement learning from Itl specifications with optimality guarantees. Proceedings of the Thirty- Second International Joint Conference on Artificial Intelligence, IJCAI '23, 2023. ISBN 978-1-955792--0-44, 10.24963/ijcai.222233 2023/44.. URL httpt::t///////t www.dii.ooo/iiooooo 10. 211.11..44391.1
Thirty-Second
doi:
2023/465
Salomon Sickert, Javier Esparza, Stefan Jaax, and Jan Křetínskýý Limit-determiniticc Büchi au- tomata for linear temporal logic. In Swarat Chaudhuri and Azadeh Farzan (eds.). Computer Aided Verification, pp. 312-332, Cham, 2016. Springer International Publishing. ISBN 978-3- 319-41540-6.
David Silver, Aja Huang, Chris J Maddison, Arthur Guez, Laurent Sifre, George Van Den Driessche, Julian Schrittwieser, Ioannis Antonoglou, Veda Panncershelvam, Mare Lanctot, et al. Mastering the game of go with deep neural networks and tree search. nature, 529(7587):484
2016.
David Silver, Julian Schrittwieser, Karen Simonyan, Ioannis Antonoglou, Aja Huang. Arthur Guez, Thomas Hubert, Lucas Baker, Matthew Lai, Adrian Bolton, et al. Mastering the game of go without human knowledge. nature, 350 2017.
14

---

Published as a conference paper at ICLR 2026
David Silver, Thomas Hubert, Julian Schrittwieser, Ioannis Antonoglou, Matthew Lai, Arthur Guez, Mare Lanctot, Laurent Sifre, Dharshan Kumaran, Thore Graepel, et al. A general reinforcement learning algorithm that masters chess, shogi, and go through self- play. Science, 362 1144, 2018.
Joar Skalse, Nikolaus Howe, Dmitrii Krasheninnikov, and David Krueger. Defining and character- izing reward gaming. Advances in Neural Information Processing Systems, 35:9460-9477, 2022.
Sanghyun Son, Laura Yu Zheng, Ryan Sullivan, Yi-Ling Qiao, and Ming C. Lin. Gradient informed proximal policy optimization. NeurlPS, 2023.
Adam Stooke, Joshua Achiam, and Pieter Abbeel. Responsive safety in reinforcement learning by pid lagrangian methods. In International Conference on Machine Learning, pp. 9133-9143. PMLR, 2020.
Hyung Suh, Max Simchowitz, Kaiqing Zhang, and Russ Tedrake. Do differentiable simulators give better policy gradients? In International Conference Machine Learning, pp. 20668- 20696. PMLR, 2022.
Daiying Tian, Hao Fang, Qingkai Yang, Haoyong Yu, Wenyu Liang, and Yan Wu. Reinforcement learning under temporal logic constraints as sequence modeling problem. Robotics and Au- tonomous Systems, 161:104351, 2023. ISSN 0921-8890. doi: 10.0066f.rbbot2222.143333
Rodrigo Toro Icarte, Toryn Q Klassen, Richard Valenzano, and Sheila A Mcllraith. Teaching mul- tiple tasks to an RL agent using I.TI.. Proceedings of the 17th International Conference on Autonomous Agents and MultiAgent Systems, pp. 452-461. International Foundation for Au- tonomous Agents and Multiagent Systems, 2018
Christos K. Verginis, Cevahir Koprulu, Sandeep Chinchali, and Ufuk Topcu. Joint learning of reward machines and policies in environments with partially known semantics. Artificial Intelligence, 333:104146, 2024. ISSN 0004-3702. doi: 10. 101610066..iiiinn 20...
Oriol Vinyals, Igor Babuschkin, Wojciech M Czarnecki, Michaël Mathieu, Andrew Dudzik, Juny- oung Chung, David H Choi, Richard Powell, Timo Ewalds, Petko Georgiev, et al. Grandmaster level in starcraft ii using multi-agent reinforeement learning. Nature, 575(7782)3350-23 2019.
Cameron Voloshin, Hoang M Le, Swarat Chaudhuri, and Yisong Yue. Policy optimization with linear temporal logic constraints. NewrIPS, 2022. doi: 10448550/arrixx2206.055552
Cameron Voloshin, Abhinav Verma, and Yisong Yue. Eventual discounting temporal logic counter- factual experience replay. ICML,, 2023. doi: 10-485500arxxx.2333322223
Yixuan Wang, Simon Sinong Zhan, Ruochen Jiao, Zhilu Wang. Wanxin Jin, Zhuoran Yang, Zhaoran Wang, Chao Huang, and Qi Zhu. Enforcing hard constraints with soft barriers: Safe reinforcement learning in unknown stochastic environments. In International Conference Machine Learning, 36593-36604. PMLR, 2023.
Min Wen and Ufuk Topcu. Probably approximately correct learning in stochastic games with tem- poral logic specifications. In Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI' 16, pp. 3630-3636. AAAI Press, 2016. ISBN 9781577357704.
Min Wen and Ufuk Topcu. Probably approximately correct learning in adversarial environments with temporal logic specifications. IEEE Transactions on Automatic Control, pp. 1-1, 2021.
Keenon Werling, Dalton Omens, Jeongseok Lee, Ioannis Exarchos, and Karen Liu. Fast and feature-complett differentiable physics for articulated rigid bodies with contact. RSS, 2021. doi: 10.44855/arxxv.2103...o
Jie Xu, Tao Chen, Lara Zlokapa, Michael Foshey, Wojciech Matusik, Shinjiro Sueda, and Pulkit Agrawal. An end-to-end differentiable framework for contact-aware robot design. RSS, 2021. doi: 00.48550arxii.22077777555
15

---

Published as a conference paper at ICLR 2026
Jie Xu, Viktor Makoviychuk, Yashraj Narang, Fabio Ramos, Wojeiech Matusik, Animesh Garg, and Miles Macklin. Accelerated policy learning with parallel differentiable simulation. ICLR, 2022. doi: (0448550kmxx.222040711.....
Zetong Xuan, Alper Bozkurt, Miroslav Pajic, and Yu Wang. On the uniqueness of solution for the bellman equation of Itl objectives. In 6th Annual Learning for Dynamics & Control Conference, pp. 428-439. PMLR, 2024.
Beyazit Yalcinkaya, Niklas Lauffer, Marcell Vazquez- and Sanjit Seshia. Compositional automata embeddings for goal-conditioned reinforcement learning. Advances in Neural Informa- tion Prucessing Systems, 37:72933-72963, 2024.
Cambridge Yang, Michael Littman, and Michael Carbin. On the (in)tractability of reinforcement learning for LTL objectives. I/CAI, 2022. doi: 10448500axiv.2111..2779
Chao Yu, Jiming Liu, Shamim Nemati, and Guosheng Yin. Reinforcement learning in healthcare: A survey. ACM Computing Surveys (CSUR), 55(1))1-36, 2021.
Dongjie Yu, Haitong Ma, Shengbo Li, and Jianyu Chen. Reachability constrained reinforcement learning. International conference on machine learning, pp. 25636-25655. PMIR, 2022.
Miguel Zamora, Momchil Peychev, Sehoon Ha. Martin Vechev, and Stelian Coros. PODS: Policy
optimization via differentiable simulation. ICML, 2021.
Sinong Zhan, Yixuan Wang, Qingyuan Wu, Ruochen Jiao, Chao Huang, and Qi Zhu. State-wise safe reinforcement learning with pixel observations. In 6th Annual Learning for Dynamics & Control Conference, pp. 1187-1201. PMLR, 2024.
16

---

Published as a conference paper at ICLR 2026
A REINFORCEMENT LEARNING WITH TEMPORAL LOGICS
Deep RL. The rapid progress in machine learning during the 201 Oss particularly in deep learn- ing (LeCun et al. 2015 Goodfellow et a 2016: Arulkumaran et al. (017). facilitated by improved neural architectures and enhanced computational capabilities, significantly advanced deep reinforce- ment learning (RL). This enabled solving complex, high-dimensional, and long-horizon sequential decision-making tasks previously considered infeasible (Mnih et al., 22055) Silver et al.) 2016 2017 2018 Vinyals et al.] 22019.. Such achievements have attracted growing interest from the control and robotics communities. Although deep RL has been effectively employed in structured, task-specific
robotic and autonomous systems (Kober et al., 2013 Levine et al., 2016]] Chen et al. 2017 Cui
al. 2017 Liu al., 2018 Lu et al. 2018 Hwangbo al. 2019 Cui al. 2019: Peng & Shen
2020
Andrychowicz et al.) 2020 Lee et al. 2020 Yu et al. 2021 Kiran et al. 202 Aradi 2022).
significant concerns around safety and reliability remain. In response, researchers have explored
integrating RL with formal methods. particularly temporal logics, to enhance system reliability and
verification.
Model-Based RL for LTL. Initial attempts combine linear temporal logic (LTL) with RL (Fu & Topcu 2014b; Brázdil et al. [2144] WWen & Topcu (016) relied on model-based approaches. These methods required precise knowledge the transition structure of the underlying Markov de- cision processes (MDPs) to precompute accepting components of a product MDP constructed using a Deterministic Rabin Automaton (DRA) based on LTL specifications. This approach transformed satisfying temporal logic constraints into reachability problems solvable via RL. Despite provid- ing probably approximately correct (PAC) guarantees, the complexity and frequent unavailability of accurate transition models limit their applicability, especially in deep RL contexts.
Model-Free RL for LTL. To address these limitations, model-free frree RL methods emerged, such as reward machines (RMs) (Toro Icarte et al.] 20188] [carte et al., 2018 Camacho et al., 2019 Icarte et al.) (022) for co-safe LTL and LTL,; fragments, which directly generate rewards from the accep- lance conditions of automata derived without explicit knowledge of transition dynamics. The in- troduction of limit-deterministic Büchi automata (LDBAs) (Hahn et al.] [2015) Siikkrt et al. (0166), simplifying model checking by utilizing simpler Büchi conditions instead of Rabin conditions, fur- ther facilitated structured reward design (Hasanbeig et al. [019:] (023). These advancements also resulted in improved correctness (Hahn et al.] 2019) and stronger convergence guarantees (Bozkurt
et al. 2020a).
STL and Other Temporal Logics. Researchers have also explored alternative continuous-time temporal logics to generate informative reward signals such as STL and truncated L.TL (TLTLL (Li et al., 2017: 2019). STL and TLTTL allow robustness scores to serve as rewards finite-horizon tasks (Aksaray al. (016). However, these scores typically depend on historical information, violating the Markov assumption and restricting their use in long-horizon, stochastic, or value-based RL settings. We note that the syntax of our differentiable LTL formalism coincides with TLTL as well as the STL fragment without time constraints; however, the semantics defined based on discrete-time observations, which allows for compact automaton construction rather than robustness scores, yielding an efficient memory mechanism.
Extended RL for LTL. Building on successful applications of LTL-based rewards in RL, re- searchers extended these methodologies into broader domains. These include stochastic games (Hahn et al.] 2020 Bozkurt et al. 20216: 2024), modular deep RL frameworks (Cai et al. 202 la Jackermeier & Abate 2025), reinforcement learning under workspace uncertainties (Cai et al. 2021b). secure planning against stealthy adversaries (Bozkurt et al. [2021a] Cui et al. (023). learn- ing within cluttered environments (Cai et al.) (023a). Additionally, recent developments include heuristic-driven learning (Kantaros] 2002), policy optimization strategies (Voloshin et al.) 2022) quantum-based action spaces (Cai et al.) 2023b), experience replay enhancements (Voloshin et al,
2023), transformer models (Tian et al. 2023). handling partially known semantics (Verginis et al.
2024 J. average reward formulations (Le et al. 2024). PAC guarantees (Perez et al. 2024). and goal- conditioned LTL-RL (Yalcinkaya et al. 2024). Theoretical analyses have explored computational intractability (Yang et al. discounting sensitivity (Xuan et al. 2024). and convergence prop- erties (Shao & Kwiatkowska 2023)
17

---

Published as a conference paper at ICLR 2026
B PATHS AND POLICIES
MDP Paths. An MDP begins in an initial state sampled from the initial state distribution so ~ po(+) and evolves by transitioning from current state to next state s' through action a, as determined by the transition function: s' = f(s, a). In each state 8, the policy observes a set of atomic propositions provided by the labeling function L(s). The sequence of visited states is called a path and is formally defined below:
Definition 3. A path of an MDP M is defined as infinite sequence of states a 8081 ...., where each 8, E S, such that po (80) > 0 and for every > O, there exists an action a₁ E A with f(st, ax) = 1-4-1- We denote the t-th state in the sequence
a ft). the prefix up to t a [ $6$1... St, and The corresponding sequence of labels for is referred as the trace, defined by L(o)= = L(8))
the suffix starting from t + as a [1:1:] = St4 18+18
Finite-Memory Policies
Definition 4. A finite-mmmory policy for an MDP M is defined tuple π =Wi, mo; I, a), where:
Mt a finite set of modes (memory states);
mo E Di is the initial mode;
I 21 x x M - [0, 1] is a probabilistic mode transition function such that for any current
mode and state s, the probabilities over next modes sum i.e., Emveon I(m' m, = 1;
[0, 1] is a probubilistic action selection function that assigns a probability to euch action given the current mode m E Dt and state E S.
a: ::Di
mnimey policy acts as a finite-state machine that updates its internal mode (memory state) as states are observed, and specifies a distribution over actions based on both the current state and mode. The action at each step is thus selected according not only the current state but also the current memory state of the policy. In contrast to standard definitions of finite-memory policies (c.g.. (Chatterjee & Henzinger 2012: Baier & Katoen (2088), which typically assume deterministic mode transitions, this definition permits probabilistic transitions between modes. For further details, please refer to (Bozkurt 2024).
C DIFFERENTIABLE REINFORCEMENT LEARNING
Differentiable Simulators. Deep reinforcement learning (RL) provides robust framework for learning control policies directly from high-dimensional, unstructured inputs without explicit hu- man supervision. However, this flexibility introduces high sample complexity. To mitigate this, re- searchers developed methods such as distributed RL, massively parallel GPU-based RL, and model- based RL approaches. Recently, there has been significant interest in accelerating model-based RL using differentiable simulators, which enable gradient-based based optimization by analytically auto- matically computing gradients of states and rewards with respect to actions (Carpentier Mansard, 2018 Geilinger et al. 2020 Qiao et al., [0221] Xu et al.) 2021 Werling et al. [2021; Heiden et al.,
Freeman et al. 2021). l). These simulators can be represented as differentiablee transition func- [st: ).), where and a, represent the state and action at time step t, respectively, and 8141 is the next state at time step + 1. In the context of reinforcement learning. a common choice for the differentiable loss function is the negative of the return, defined the sum of discounted re-
2021
lions St4-1
wards: C = G (ar - Et" TeT', where is the time horizon, = S0$1 ... is the trajectory, is the reward at time step t, and 7/2 is the discount factor applied at that step. The backward pass then computes the gradients as follows:
8G 0G 0f
0G
8G 0s
(11)
Ds: dst+1 ds,"
Do, ds Da.
By chaining these gradients, the optimization updates propagate effectively throughout trajectories.
Policy Gradient Objective. In policy gradient RL over finite horizon H, the goal is to find optimal parameters 0" argmax (0), such that:
((0) = Ea- [G
(12)
18

---

Published as a conference paper at ICLR 2026
where Mx, denotes the random trajectory drawn from the Markov chain Mx, induced by the policy ze parameterized by 8. If a differentiable model is available, optimization can leverage first-order gradients:
# J(0) = Eo-M-, [o
(13)
employ model-free zeroth-order gradients via the policy gradient theorem:
H-1
V ((O) Mo Gn(o)
Σ
Vo log (a(a)
(14)
Both gradients can be approximated through Monte Carlo sampling:
A J
voGn(o!0),
(15)
N
N
#-1
/ ((0) Σ
N (n
Vo log (a (4 (s())
(16)
D w- A-AUOMAATA
An LTL formula oo be translated into finite-state automaton that operates over infinite paths, known as an w-automaton. We denote the automaton corresponding to a specific formula yp by AAp An w-automaton Ap accepts path a if and only if }= ip, and rejects it otherwise. We begin by formally introducing a general type of w-automaton, called a nondeterministic Rabin automaton (NRA), which can be systematically derived from any LTL formula (Baier & Katoen 2008). We then focus on specific subclasses of NRAs that are particularly relevant to our work.
Definition 5. A nondeterministic Rabin automaton (NRA) derived from an LTL is defined as a tuple Av- = (Q, qo; E, 6, Acc), where:
Q is a finite set of automaton states;
E Q is the initial automaton state;
Σ 2a is the imput alphabet, where & is the set of atomic propositions:
8 x (EU(et) - 2 is the transition function, which is complete and deterministic on E (i.e., 1ō(q,t) w)] for any Q and w E), but may include nondeterministic e-transitions (i.e., is possible that (8(g,)) s) | = 0 or 18(4 e)] > 1);
Acc is of k accepting pairs [B, C.) where Bi, C2 C&S.C Q f1,...,
of the automaton is sequence of transitions T.r (4o, Wo, 41)) ), (2), W1, .2).... such that (++1 E 8(g,, w.) for 2 0. The word w is accepted if there exists such run and at least one accepting pair (Br, C.) satisfying the Rabin condition: the visits some states in B, infinitely often and all states in C2 only finitely often. This acceptance condition known as the Rabin condition, which can be formalized as w - o ( 3t Inf(TT)(BB, Inf(T.)) )CC;=@ where Inf( denotes the set of states visited infinitely many times in the run Tw- Similarly, path is considered accepted by the automaton if its trace L(o) forms word accepted by Ag.
Given infinite word
Wo ...
We focus on specific subclass of NRAs known as determitteriiiiticc Büchi automata (LDBAs), which feature simplified acceptance criterion. Despite their reduced complexity, LDBAs retain the full expressive power of general NRAs and can be systematically derived from LTI. formulas (Hahn)
al. 2015 Sickert al. 2016).
Definition 6. An LDBA is NRA defined A, (Q, go. Σ, 8, Acc) that satisfies the following:
The acceptance condition consists of a single pair with an empty second set, i.e., Acc = (B, Ø), meaning that the ran must visit some states in B infinitely often. This is known the Büchi con- dition, and for simplicity, we denote this acceptance condition by the set of accepting automaton states itself, Lee, Acc B.
19

---

Published as a conference paper at ICLR 2026
The state space Q is partitioned into two disjoint subsets: an initial component Q1 and accept- ing component Q. satisfying:
All accepting states are contained in Qa. i.e, - QQ:
All transitions within QA are deterministic (no E-transitions), for any QAQA. 0(g,
Transitions cannot go from QA to Q1. for all QA and w E Σ, 8(g, w) S QA-
The defining feature of LDBAs is that accepting runs must eventually enter the accepting com- ponent Q^ and remain there permanently. Once this transition occurs, all subsequent behavior is deterministic-this property is known limit-determinism. LDBAs can be constructed such that ev- ery e-transition leads directly into QΛ. which ensures at most one such transition occurs along any exccution path. This construction, combined with limit-determnnism, makes LDBAs particularly well-suited for quantitative model checking in MDPs (Sickert et al. (216)) unlike general nondeter- ministic automata. Thus, assume all LDBAs under consideration possess this structure. More information can be found in (Bozkurt 2024
E PARKING EXAMPLE: DIFFERENTIABLE RL VS NON-DIFFERENTIBLLE RL
Zeroth Order SGD
First Order SGD
5
(mls*)
Deceleration (mls?)
3
3
1
1
10a
10a
10a
10a
10a
10a
10a
10a
10a
Iterations (log scale)
Iterations (log scale)
Figure 3: Convergence speed comparison of stochastic gradient descent algorithms using V and
V #
for the parking example (N 10).
F LTL SPECIFICATIONS AND AUTOMATA
LTL Specifications used in the Experiments.
CartPole:
6("position_xe> 11- tonsition_x<l01 G=P=e10 "velocity_xc1..09 """"oa_tthtax--0.5 teoa_theeax00.")
Hopper:
@"torso_heightt-1111 "F"tooro_ cectorro_vlloottyyyoe ("torso_veloeityyce
Cheetah:
@"tip_height>>77.5 à or"tip_height>-7.e Fi"tip_.veoooty_yoo..0 F"tip_weloosty_xe""
Ant:
@"terao__eiight0000 hertorro
Fi"toree_veloccltyyx1..33 p"torao_welocity_.co0
20

---

Published as a conference paper at ICLR 2026
Illustration of the LTL Specification for Cheetah.
2m/s
m//
1i/ss
0 my/
Figure 4: Task Specification with LTL. This figure illustrates Cheetah policy learned by SHAC using differentiable rewards derived via our approach from the LTL formula Plegged which speci- fies accelerating forward, stopping, and maintaining safe tip-to-ground distance. Specifying the desired behaviors of robots using the high-level language LTL provides is an intuitive alternative to manually designing reward functions, which often require extensive domain expertise and risk un- intended behaviors. Enabling learning directly from LTL unlocks new possibilities for robust, safe, and flexible robotic applications. See the supplementary material for video.
Automata Derived from LTL Specifications for CartPole and Ant.
Figure 5: The w- a-automaton derived from Peartpole-
Tariu wwg.oeg Pe
Figure 6: The a--automaton derived from Plegged for the Ant environment.
Other example LTL formulas. LTL can be used to specify temporal properties of a wide range of robotics tasks:
safety: e.g.. "always avoid obstacles and remain below the joint angle and velocity thresholds":
= 0
dist.to oosttale,,, > O
joint. angle, < Amax
joint.vel, < (8mmx)
(17)
obstacle;
joint.nggee,
join.vel,
reachability; e.g.; "accelerate to target velocity in direction":
(torss_vel. vol. > Uunget
(18)
sequencing; e.g.; "move to the position 1, then move to the position 2, and after that move to the position 3"
P 0 diss..toppos < dua (dist.to.pos, < dml Oddssttto < 6wl))
(19)
repetition; e.g.: "repeatedly monitor the region and the region 2":
* Kodist region, < A TV (dist region, 6wa).
(20)
21

---

Published as a conference paper at ICLR 2026
G
REWARD MACHINE GENERALIZATION RESULTS
Table I: Comparison between differentiable RMs and discrete RMs for Cheetah.
TASK
TASK 2
Steps (K)
SHAC (ØRL)
CRM (ØRL)
SHAC (ØRL)
HRM+RS
RØL
500
7.5 3.5
5.0 K.7K
10.9 3.5
R 7.0 K
1000
1922199 K
1 0.4K
R 8.811 1.9 K
1500
11.9 + 2.8 2.8K
1.76 0.K
& 9 4 2.2 K
2000
13.7 K
0.0
1.94
R x9.1
K
2500
14.5 14.5 2.7K K
K.3
21.0=
R 8.77 2.6
3000
2..4
0.3
2191
& 9.1
H ABLATION STUDY RESULTS
We present ablation study results for differentiable LTL approaches in Figure 7 and Figure g spectively.
re-
Happer
Ant
AMAC
AP-CC
AMAC
0,2
0.2
0.2
0.6
0.0
0.0
0.0
Stops
Stups
Stoss (M)
Staps 01)
Figure 7: Ablation study for differentiability of L.TL rewards. The maximum returns obtained
after 100 M steps for SHAC and AHAC (ŌRLs) with discrete L.TL rewards. Returns (0 to 1) indicate LTL satisfaction probabilities. With discrete LTL rewards, ØRLs fail to learn near-optimal policies. However, as shown in Fig. 2 the with our differentiable LTL rewards, they can successfilly learn near-optimal policies.
Simplified LTL formulas:
ceappole = O pploleez-
=A'',
Pleggod == O'torso_xx>")
(21)
using 2g m, em for Cartpole, and 1i 50 cm/s for all the legged-robot environments.
CartPole
Hopper
Cheetah
Ant
11.0
Retum (LTL Sat. Prob.
.99
.98
(a)
(a)
(-a)
(-a)
Figure 8: Ablation study for complexity of LTL formulas. The maximum returns obtained after 100 M steps for simplified LTL formulas (2T). Returns to 1) indicate LTL satisfaction proba- bilities. Under these simpler specifications, both ØRLs and 0RLs successfully learn near-optimal policies. However, as shown in Fig. 2, the performance of discrete ØRLs degrades dramatically with increasing LTL complexity unlike differentiable 0RLs, which maintain reasonable performance by leveraging the LTL rewards differentiability.
22

---

Published as a conference paper at ICLR 2026
1 COMPARISON WITH OTHER LOGICS AND METHODS
111 CONSTRAINED OPTIMIZATION
The main advantage of logical specifications over constrained optimization techniques such as bar- rier functions or model predictive control (MPC) is that they provide a general, unified, and arguably more intuitive language with high expressive power, which can be used to specify not only safety and liveness, but also memory-requirin properties such as sequencing and conditioning. These can be concatenated into single objective formula using Boolean operators with well-defined probabilistic semantics. We note that these constrained optimization techniques might handle safety properties more effectively in a differentiable setting. However, emphasize that these techniques not mutually exclusive with our approach can be incorporated in a setting where safety constraints are prioritized over other specifications and handled by such techniques.
1.2 SIGNAL TEMPORAL LOGIC
History-Dependence.
Temporal logics such as signal temporal logic (STL) are designed for con- tinuous state variables and time constraints and thereby, generally, more compatible with differ- entiable systems. The main advantage of LTT., however, over these logics, is the compact memory mechanism provided as an automaton. Evaluating STL satisfaction or robustness, therefore, requires access to the full trajectory. as these metrics can only be computed after the trajectory ends. This necessitates storing entire trajectory histories, which directly violates the Markovian assumption fundamental to value-based RL techniques. Unlike LTL, this issue cannot be resolved by augment- ing the state space with a compact memory representation derived from automata. There are two common approaches to address this challenge. The first is to augment the state space with the full trajectory history, but this leads to prohibitively large and impractical state spaces for the longer horizon tasks consider in our work. For instance, with horizon of H 1024 used in periments, the state space for the Ant environment would be of size 1024 x 37 = 37, 887. The sec- ond approach involves applying policy optimization over the action history using backpropagation through time (BPTT). However, due to the well-known exploding and vanishing gradient problems, gradients quickly deteriorate and become unreliable beyond roughly 100 time steps. This issue is further exacerbated in stochastic environments, where optimization becomes ineffective even over a small number of steps. Using intermediate STL robustness scores, an approach sometimes adopted to address the sparse reward problem in practice, does not resolve this hard non-Markovian prob- lem of STL specifications. In fact, optimizing for the sum of such intermediate rewards can lead to incorrect RI. objectives, as it does not necessarily correspond to maximizing the satisfaction of the STI. specification.
Syntax and Semantics. We focus on a subset of LTL formulas where atomic propositions (APs) defined as bounds continuous signals (or their functions). This subset overlaps with the class of STL formulas that do not include real-time constraints. One advantage of these formulas that avoid the inherently discrete APs permitted by general LTL formulas, thereby ensuring differ- entiability of the system. For example, instead of relying on a discrete low-battery indicator (c.g., == low battery), we define APs as continuous thresholds (e.g.. == battery level < 20%). An- other advantage is that abstracting away the real-time constraints inherent in general STL formulas enables us to employ an aatomata-based compact memory mechanism rather than storing the entire trajectory history, substantially improving learning efficiency. We note that although STI. formu- las without real-time constraints are syntactically equivalent to the LTL. formulas we consider, STI. differs significantly at the semantic level. Specifically, STL places greater emphasis tative robustness score computed over the entire trajectory and does not aim to construct compact, automata- memory. This distinction also holds for other similar logics such as truncated LTL,, which are syntactically equivalent but similarly focus on robustness scores.
the quanti-
1.3 REWARD MACHINES
Background. The starting point of reward machine research is the construction of automata from LTL formulas specified as RL tasks (Icarte et al. (2018)). Early work focused on the co-safe frag- ment of L.T. Icarte et al. (2018) and [.T. over finite traces (LTTL.)Caaaae et al. (2019), for which
23

---

Published as a conference paper at ICLR 2026
deterministic finite automaton (DFA) can be constructed. These DFAs were later termed reward machines (RMs), as their accepting states can be used to assign positive rewards. Approaches tar- geting general LTL specifications instead use limit-deterministic Büchi automata (LDBAs). While structurally similar to RMs, LDBAs differ in their acceptance condition, which is based on infinite visitation of accepting states (suitable for continuous tasks), and thus require distinct discounting scheme for correctness and convergence. In this work, we focus on making automaton- baaeed reward signals differentiable, including those from DFAs and therefore RMs. When dealing with LDBAs, our approach additionally handles non non- non-deterministie transitions and infinite visitation objectives. Importantly, our method can be immediately applied, without modification, to any RM constructed from co-safe LTL LTL, formulas using the atomic propositions defined in Section 2. As result, our approach can directly accelerate learning with RMs. Furthermore, all existing techniques used with RMs, such as reward shaping Icarte et al. (022), can also be integrated into differentiable RL. We note that while reward shaping does not affect the optimality of policies, it may lead to incorrect estimates of satisfaction probabilities.
Discrete vs. Differentiable RMs. Differentiable reward machines will outperform discrete ones due to their inherent ability to propagate gradients across time steps, which provides additional derivative information about future rewards and states with respect to current actions. However, we would like to emphasize two important limitations. First, the additional gradients are not always useful practice, especially when they are backpropagated over a long horizon that may include sharp gradients caused by events such as collisions. There are illustrative examples of this issue in Suh et al. (2022) ) Therefore, the gradient flow should be carefully controlled by approaches, such as limiting the horizon (SHAC) or cutting off gradients sharp collisions (AHAC). Second, differen- tiable environments or simulators are not always available. Although physical systems can usually be modeled with differentiable simulators, this is not always possible for systems with inherently discrete states, actions, or transition structures, In such cases, a discrete-to-cominnuur conversion or approximation might be derived on a case-by-case basis, with additional challenges.
J LIMITATIONS AND EXTENSIONS
J.1 DISCRETE MDPs
An extension of our approach to discrete MDPs may be possible under certain assumptions. For example, if the MDP is a discretized version of a continuous environment, then any continuous state can be described as a probability distribution over the neighboring discrete states. As another example, discrete actions such as on/off switches could be expressed as a probability of switching. However, our approach cannot trivially extended to discrete MDPs with inherently discrete states, such as categorical variables.
J.2 STOCHASTIC TRANSITION FUNCTIONS
Our method is naturally compatible with stochastic environments. For consistency with existing dif- ferentiable simulators, we model the transition function deterministic. Nevertheless, probabilistic differentiable transition dynamics can also be incorporated using techniques such as the reparam- eterization trick. In the current implementation, the initial state distribution is the only source of randomness.
J.3 DIFFERENTIABLE STATE LABELS
We note that assuming a differentiable underlying system is, in general, strong requirement. How- ever, we view our additional assumption that state labels are differentiable as relatively minor, since it largely follows from the standard assumption that state variables and transitions are differentiable setiiiable-ssmulat--bbbaa
in all ther (i) arises from a separate discrete transition system that must be fused with the simulator for the Markov assumption, thereby already violating differentiability, ferentiable variables (c.g., positions, velocities, or time), in which case can usually be smoothed with respect to those variables as in our approach. Thus, while differentiable state labels are in-
approaches. For example, a label such as "the light is red" ei-
(ii) is discrete function of dif-
24

---

Published as a conference paper at ICLR 2026
deed a strong assumption, this limitation mainly stems from the differentiability requirement on the simulator's s transition function and shared by all coattiiaabbessmultooo based methods.
J.4 CHOOSING B
The choice of 3 can be critical, depending on the environment and task. From a theoretical perspec- tive, larger 3 is preferable for the correctness of the objective, whereas from practical perspec- tive, a smaller 3 generally improves convergence and stability. We therefore suggest starting with smaller 3 and gradually increasing it until the algorithm no longer converges begins to exhibit stability issues. Domain knowledge about the environment and task can also help guide this choice. For example, if we expect reaching tasks repetitive behaviors encoded in the LTL specifications to manifest within H time steps, then B can be chosen so that 3 remains reasonably large (c.g., 0.05).
J.5 EXPLOITING FREQUENCY OF VISITING ACCEPTING STATES
Tweaking the discount factors indeed result in policies that suboptimal in terms of LTL sat- isfaction. For example, if the discount factor is not large enough (leading to myopic behavior), a policy that visits accepting states frequently, say at every time step for the first 1000 steps and then never again, may be preferred over policy that visits an accepting state once every 1000 steps in- definitely, even though the latter should be preferred terms of formal LTL satisfaction. Therefore, we suggest choosing discount factors that are sufficiently large while still ensuring convergence and stability, as discussed above.
J.6 SIGNAL FUNCTIONS
We assume that designing signal functions part of requirement extraction and specification engi- neering, and therefore treat them as given in our approach. However, the signal functions can affect the performance of our approach. Specifically, gradients are backpropagated through the signal func- tions after the activation functions, and if the signal functions have sharp regions, they may produce gradients with very large magnitudes, which can in turn impede the learning updates. Therefore, smoother signal functions are preferable.
J.7 SLOPE SIGMOID ACTIVATION
The slope of the sigmoid function used in the labeling function can, in fact, be critical. A steeper slope induces gradients with large magnitudes around the boundary, which can affect stability, and gradients with small magnitudes away from the boundary, which can slow convergence. In contrast, a shallower slope can interfere with correctness. In practice, domain knowledge can significantly help in determining these parameters. For example, in approach considered lengths in centimeters, for which standard sigmoid function mostly transitions from to within about 10 cm, which was suitable for our tasks, we did not need to change the temperature parameter much. We believe, however, that a clipped version of the rectified linear unit, e.g., y min (max(temp.
0.5, 0), 1), would be better choice, although we did not have time to experiment with such alternative activation functions and will certainly do so in future work.
J.8 DIFFERENTIABLE MATRIX MULTIPLICATION
We assume that the transition matrices are small enough to be stored in GPU VRAM, where differ- entiable matrix multiplications can be performed efficiently in parallel using available tools such as PyTorch or TensorFlow. However, if the transition matrix too large to fit in VRAM; for example, due very long LTL specifications involving many state labels, the computation is not trivial.
PARTIAL D
A very interesting, necessary, and exciting future research direction, of the reviewers of this paper indicated, is to extend our approach to the systems with partial differentiability. We believe that approach cannot be readily extended, and that RI. algorithms required for such
25

---

Published as a conference paper at ICLR 2026
hybrid settings. One case to consider, however, is when the differentiable and discrete systems have their own separate states, actions, and transition systems; i.c., they are completely decoupled except through the rewards. In this casc, it becomes possible to obtain derivatives of future rewards with respect to the actions of the differentiable system.
J.10 COUNTERFACTUAL EXPERIENCE REPLAY AND REWARD SHAPING
Our approach can be extended to include counterfactual experience replay Voloshin al. (2023) and reward shaping techniques Icarte et al. 2022) under some caveats. First, additional rewards provided by shaping should be differentiable function of the state variables, and second, they should not compromise the formal objective of maximization of the satisfaction probabilities. The latter does not technically interfere with the learning algorithm, but violates the main goal of this paper to have formally sound objective. Counterfactual experience replay be integrated with the differentiable approaches SHAC and AHAC if the counterfactual trajectories are obtained by changing only the automaton states.
26


Reviews:
[{"review_id": "7eUSFMHvS4", "reviewer": "Reviewer_Ay51", "summary": "This paper presents a logic-based reinforcement learning (RL) framework that introduces differentiable LTL rewardsby employing probabilistic, or “soft,” atomic propositions within differentiable MDP environments. The key idea is to integrate logic-based specification methods into differentiable RL, thereby bridging symbolic reasoning and gradient-based optimization. The authors further extend the framework to differentiable generalizations of reward machines, providing a smooth relaxation of discrete logical rewards. Theoretical results show that by appropriately choosing the *softening parameter* $\\zeta$, the error between the discrete and differentiable logic-based RL formulations can be made arbitrarily small.\n\nEmpirical evaluations demonstrate that Short Horizon Actor-Critic (SHAC) and Adaptive Horizon Actor-Critic (AHAC) outperform discrete RL baselines such as PPO and SAC, confirming that the benefits of differentiable MDPs extend to logic-based rewards. The experiments also include a differentiable variant of reward machines, showing that differentiability continues to provide learning benefits even under structured quantitative objectives.", "questions": "1. Can the proposed approach be extended to discrete MDPs, perhaps via smooth approximations of the transition probabilities?\n2. How would reward shaping or counterfactual experience replay interact with differentiable logical rewards?\n3. Are continuous-time temporal logics such as MTL or STL more suitable for differentiable RL, and how might they affect interpretability or computational cost?\n4. Discrete reward machines, with their inherently sparse reward structures, can sometimes perform competitively when combined with reward shaping or counterfactual experiences. Do the authors expect differentiable reward machines to consistently outperform discrete ones, or could sparsity occasionally confer advantages?", "limitations": "", "rating": 6, "confidence": 5, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "1. The integration of logical specifications into differentiable RL is conceptually elegant and addresses an important challenge in combining symbolic reasoning with continuous optimization.\n2. The derivation of error bounds demonstrating convergence between discrete and differentiable logic-based RL formulations adds mathematical rigor to the approach.\n3. Experiments with SHAC and AHAC validate the framework’s benefits over standard baselines, showing improvements consistent with expectations from differentiable modeling.\n4. The paper clearly situates itself within state-of-the-art logic-based RL research and provides a helpful summary of related work on differentiable MDPs and reward machines.", "weaknesses": "1. It is unclear whether the proposed framework can be readily extended to discrete MDPs. Intuitively, a similar smooth approximation could be applied to the transition structure, but this is not discussed. Clarifying this would strengthen the paper’s generality.\n2. The paper does not explore whether inherently discrete methods such as reward shaping or counterfactual reasoning could complement, or interfere with, the differentiable automata framework. Including experiments or discussion in this direction would add practical depth.\n3. The paper focuses on LTL, but it would be helpful to discuss whether logics tailored to continuous systems, such as Metric Temporal Logic or Signal Temporal Logic, are more naturally suited to differentiable environments. A short comparison of their expressive and computational trade-offs would be helpful.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "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": "", "extra_scores": {}}, {"review_id": "9hXupHJbq4", "reviewer": "Reviewer_kd6k", "summary": "This paper introduces an end-to-end framework that combines Linear Temporal Logic (LTL) with differentiable simulators, allowing agents to learn directly from formal task specifications using gradient-based optimization. The authors argue that when LTL is used in reinforcement learning, it typically produces discrete and sparse rewards, which can slow down training and hurt performance. To address this, they “soften” the discrete automaton transitions through a soft-labeling technique, creating smooth, differentiable rewards while still maintaining the original task semantics. They also provide theoretical guarantees showing that the gap between the discrete LTL reward and the relaxed differentiable version is bounded under certain assumptions. Experiments compare their method against PPO and SAC agents trained with standard sparse LTL rewards, demonstrating improved performance.", "questions": "1. Page 3, the MDP formulation is more like a control formulation, generally we should have something like S x A x S -> Prob[0, 1] as transition dynamics.", "limitations": "", "rating": 6, "confidence": 3, "soundness": 4, "presentation": 3, "contribution": 3, "strengths": "The paper is clearly written and easy to understand. The authors do a nice job presenting their method.\n\nThe motivation is strong. LTL and other temporal-logic or formal-methods approaches often struggle with scalability and sparse rewards in RL, and this work tackles that important challenge.\n\nThe proposed approach appears sound. Using differentiable simulation creates a fully end-to-end training pipeline with gradient flow, which can speed up learning and potentially lead to better overall performance.\n\nThe authors include a theoretical analysis that bounds the difference between the original discrete reward and the relaxed differentiable version.\n\nThe experimental results are convincing and show promising improvements.\n\nThe related-work discussion is thorough and well-situated in the existing literature.", "weaknesses": "1. It is not fully clear how this method compares to other model-based RL approaches that also incorporate formal guarantees during training. For example, recent work that uses world models together with barrier certificates or STL can also be viewed as an end-to-end differentiable pipeline, since the world model acts as a differentiable simulator and the formal constraints guide policy learning. It would be helpful for the authors to discuss these connections more clearly and highlight the differences, including works like \nReference: State-Wise Safe Reinforcement Learning with Pixel Observations.\n\n2. Unlike LTL, STL signals are already continuous rather than purely discrete. Why do the authors focus on making LTL differentiable instead of using STL, which may naturally fit differentiable learning?\n\n3. The experiments do not include comparisons with model-based or STL-based RL baselines, which would help clarify the advantages of the proposed method.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "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": "", "extra_scores": {}}, {"review_id": "LmDexuXNdu", "reviewer": "Reviewer_QdnH", "summary": "The paper introduces a method to make logic-based specifications of rewards or constraints differentiable. Classical logic-specification frameworks rely on a formula that defines objectives through the truth values of Boolean predicates, which are then translated into an automaton and combined with an MDP to form a product MDP. The problem is that the resulting automaton produces non-differentiable states, as these depend on discrete Boolean propositions. This paper proposes a relaxation by introducing _soft labels_ that yield probabilities instead of Boolean values. Consequently, the automaton is represented by _probability vectors_ rather than one-hot encodings, enabling (i) differentiable reward signals and (ii) reduced reward sparsity, a well-known issue in the literature. The also formally prove the discrepancy between the discrete and differentiable returns. They provide empirical evaluation.", "questions": "- Regarding the claim on line 253 that \"this computation can be efficiently done through differentiable matrix multiplication\" can you comment on this? The transition matrix has size $|Q| \\times |Q|$ do you assume that $|Q|$ is small in practice? Otherwise, the operation may not be computationally trivial.\n- Can you elaborate on the point raised in weakness 1?\n- Given that the framework can only express continuous functions of the state as labels, what are the advantages of relying on logical specifications rather than classical approaches such as Model Predictive Control, which naturally handles continuous constraints (aside from the temporal abstraction advantage)?\n\nTypos:\n- Line 122: \"...The state space S (is) the...\"\n- Line 132: possible repetition of \"the return.\"", "limitations": "", "rating": 4, "confidence": 4, "soundness": 4, "presentation": 4, "contribution": 3, "strengths": "- The proposed idea is interesting and their contribution naturally mitigates reward sparsity while maintaining differentiability, making it compatible with differentiable RL controllers.\n- The mathematical formulation is sound and providing both differentiability and normalization.\n- The proposed approach bridge the temporal abstraction provided by the LTL framework to the differentiable control settings.", "weaknesses": "- I believe that limiting the labels to continuous functions of the state is a strong assumption, that restricts the benefits of logic specifications to consider only predicates that are expressible as continuous functions. For instance, $a$ = \"agent reached goal in $(x_g, y_g)$\" is captured by your assumptions, becasue it can be expressed as a distance, which is a continuous function of the state $x$. Instead, $a$ = \"the light is red\" is a boolean and condition. This assumption limits the expressive power of the logical specification framework to consider only continuous labels.\n- It would be nice to compare the performance of SHAC and AHAC with and without the LTL framework for a fair evaluation. Providing this comparison would clarify whether the observed improvements stem from the proposed LTL-based formulation or from the underlying algorithmic differences. Without this, is hard to tell what is the source of the improvement.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "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": "", "extra_scores": {}}, {"review_id": "qw8A6Xsonm", "reviewer": "Reviewer_h7aD", "summary": "Logical formalisms enable the specification of agents’ behaviors and offer correct-by-construction objectives. In RL, reward design often struggles to capture the user’s intended task, resulting in misaligned or sparse signals. Linear temporal logic (LTL) provides an expressive language to specify such trajectory-level objectives but leads to discrete, sparse rewards that hinder policy optimization. This paper introduces an end-to-end differentiable framework that integrates LTL with differentiable simulators, allowing gradients to flow through both the environment and the logical specification. The approach replaces hard labeling with smooth probabilistic labeling, yielding differentiable transitions and rewards. The authors prove a theoretical bound linking discrete and differentiable LTL returns and empirically demonstrate faster learning and higher returns on continuous-control benchmarks. The authors also note the results hold in stochastic settings. The method also generalizes to reward machines, thus covering co-safe LTL and LTLf tasks. Overall, the framework bridges formal methods and deep RL through differentiable logic-based objectives.", "questions": "- How should we tune $\\beta$ in practice? \n- Could the approach be extended to environments that are only partially differentiable or hybrid, where discrete transitions coexist with differentiable dynamics?\n- The proposed rewards depend on the frequency of visiting accepting states in the automaton. Could the authors clarify whether, by tweaking the discounts, agents might \"exploit\" repeated visits to accepting states to obtain high returns without maintaining long-term satisfaction of the LTL formula?\n- How sensitive is the method to the slope of the sigmoid activation used in the labeling functions, and how does this affect learning stability or correctness? Did you consider enriching the sigmoid function with a temperature parameter in practice? Would it be a good idea?", "limitations": "", "rating": 8, "confidence": 4, "soundness": 4, "presentation": 2, "contribution": 4, "strengths": "- The proposed use of differentiable labeling functions and probabilistic automaton transitions provides a clear and elegant means of propagating gradients through LTL objectives.\n- Theoretical contributions include a bound relating discrete and differentiable LTL rewards, ensuring that the relaxation remains faithful to the underlying specification.\n- The algorithmic exposition is quite clear; gradients, $\\epsilon$-actions, and update steps are explicitly shown in the final algorithm, supported by a detailed parking example that illustrates the difference between discrete and differentiable LTL rewards.\n- The experimental evaluation is broad, covering easy-to-challenging continuous-control benchmarks (from 5-/1-D to 37-/8-D state-action spaces) and including ablation studies that isolate the role of differentiability.\n- Comparisons between differentiable and discrete LTL baselines are convincing, showing consistent improvement in convergence and policy quality.\n- The experiments on reward machines and their comparison to existing algorithms are particularly valuable, as they demonstrate compatibility across formal-specification frameworks and situate the contribution in a wider research context.", "weaknesses": "- While Theorem 2 mentions the applicability of the approach to stochastic settings, the environments presented in the paper are solely deterministic.\n- The success of the approach largely relies on $\\beta$, which allows deriving the sole reward signal the agent gets and serves as a second discount factor. $\\beta$ is also critical in Theorem 2, providing a divergence between discrete and differentiable rewards. However, there is no discussion or intuition on how to choose $\\beta$ in practice to achieve the theoretical guarantees. \n\n*Remark*: I've had a hard time parsing the phrasing *\"Further, the rewards are discounted less in non-accepting states to reflect that the number of visitations to non-accepting states are not important.\"* Since $\\beta$ is a function of $\\gamma$ and the ratio in Theorem 1 should converge to zero, I understand that $\\beta$ should always be lower than $\\gamma$, but the phrasing (\"discounting less\") is confusing.\n- The signal functions $g_a$ underlying the soft labels remain heuristic and \"hard-coded\"; their design influence is not discussed.\n- The paper is visually extremely dense, relying heavily on negative `\\vspace` and compressed layout, which reduces readability.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "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": "", "extra_scores": {}}]

Author rebuttal:

Decision: Accept (Poster)