Directed Exploration in Reinforcement Learning from Linear Temporal Logic
Authors: Marco Bagatella
Andreas Krause
Georg Martius
Venue: Accepted by TMLR ()

Abstract: Linear temporal logic (LTL) is a powerful language for task specification in reinforcement learning, as it allows describing objectives beyond the expressivity of conventional discounted return formulations. Nonetheless, recent works have shown that LTL formulas can be translated into a variable rewarding and discounting scheme, whose optimization produces a policy maximizing a lower bound on the probability of formula satisfaction. However, the synthesized reward signal remains fundamentally sparse, making exploration challenging. We aim to overcome this limitation, which can prevent current algorithms from scaling beyond low-dimensional, short-horizon problems. We show how better exploration can be achieved by further leveraging the LTL specification and casting its corresponding Limit Deterministic Büchi Automaton (LDBA) as a Markov reward process, thus enabling a form of high-level value estimation. By taking a Bayesian perspective over LDBA dynamics and proposing a suitable prior distribution, we show that the values estimated through this procedure can be treated as a shaping potential and mapped to informative intrinsic rewards. Empirically, we demonstrate applications of our method from tabular settings to high-dimensional continuous systems, which have so far represented a significant challenge for LTL-based reinforcement learning algorithms.

Published in Transactions on Machine Learning Research (06/2025)
Directed Exploration in Reinforcement Learning from Linear Temporal Logic
Marco Bagatella
mbogatella@ethh..c
Deportment of Computer Science ETH Zürich, Zürich, Switzerland
Andreas Krausc
Department of Computer Science ETH Zürich, Zürich, Switzerland
Georg Martius
Mas Planck Institute for Intelligent. Systems Tübigen, Germany
Reviewed on OpenReview: https: // openreview.ee net/ forum? id= cfK52vP422
Abstract
Linear temporal logic (LTL) is a powerful language for task specification in reinforcement learning, it allows describing objectives beyond the expressivity of conventional discounted return formulations. Nonetheless, recent works have shown that LTL formulas can be translated into variable rewarding and discounting scheme, whose optimization produces policy maximizing lower bound on the probability of formula satisfaction. However, the synthesized reward signal remains fundamentally sparse, making exploration challenging. We aim to overcome this limilation, which can prevent current algorithms from scaling beyond low-dimensional, short-horizon problems. We show how better exploration can be achieved by further leveraging the LTL specification and casting its corresponding Limit Deterministic Büchi Automaton (LDBA) as Markov reward process, thus enabling form of high-level value estimation. By taking Bayesian perspective over LDBA dynamics and proposing suitable prior distribution, we show that the values estimated through this procedure can be treated as a shaping potential and mapped to informative intrinsic rewards. Empirically, we demonstrate applications of our method from tabular settings to high-cimensional continuous systems, which have so far represented a significant. challenge for LTI.-based reinforcement learning algorithms.
1 Introduction
Most reinforcement learning (RT) research has traditionally focused on a standard setting, prescribing the maximization of cumulative rewards in a Markov Decision Process (Puterman 2014 SStton & Barto 2018).
While this simple formalism captures variety of behaviors (Silver al.) 2021 J, its expressiveness remains limited (Abel et al.)
2021h. In pursuit of more natural and effective way to specify desired behavior, several
works have turned towards logic languages (Camacho et al. 2019 De Giacomo et al. 2020b Hasanbeig et al.
2018 Icarte et al.
2022: Li et al. 2017). Originally designed to describe possible paths of system (with
direct applications. e.g., in model checking (Baier & Katoen 2008 Linear Temporal Logic (I.TL.) (Pnueli
1977 has been found to strike an interesting balance between expressiveness and tractability.
A translation from LTL to reinforcement learning objectives is in general possible at the cost of optimality
Alur al. 2022 Nevertheless, several works (Bozkurt et al. 2020 Hasanbeig et al. 2020 Voloshin et. al.

---

Published in Transactions on Machine Learning Research (06/2025)
PL
Task Specification GF(a XFc) & G-b
build
Paa
inform
updote
LDBA
Prior P(K)
Posterior P(K)D)
MRP Distribution
compute
observe
train
EPCCD x
Trajectory D
Environment
Product MDP M
Policy =
Figure 1: Overview of DRL DRL2 leverages an LDBA representation of the task and a Bayesian estimate of its transition kernel to define a distribution over Markov reward processes, which can be used for high-level value estimation. Resulting values are mapped an intrinsic reward signal, which guides exploration in the product MDP.
2023 have proposed a reward and discounting scheme distill policy through reinforcement learning from LTL specification. In particular, the scheme proposed by VVloshin et al (0233 recovers policy that optimizes a lower bound on the probability of satisfying the specification: suboptimality can in practice be bounded through discretization arguments, or for finite policy classes. However, this scheme results in a sparse reward signal and a polentially flat value landscape, thus making exploration a. fundamental challenge.
The necessity for strong exploration algorithms when learning from LTL specification therefore evident. Existing methods rely on counterfactual data augmentation schemes (Voloshin et al.) 2023), which however do not directly guide the agent in the underlying MDP, on the availability of task distribution (Wang al. 2023), on heuristics (Hasanbeig et al., 2020). Closer in spirit to our work, task-aware reward shaping has briefly been explored in the context of finite logic (Camachoo et al. 2019 Icarte et al. 2022). but has not been scaled to w-regular problems and cannot adapt lo unknown environreent dynamics.
The main idea of our work is the distillation of an intrinsic reward signal from the structure of the LTL specification itself. In particular, we repurpose the Limit Deterministic Büchi Automata (LDBA) constructod from an LTL formula as a Markov reward process, by assuming transition kernel over LDBA states. We then leverage the reward process to perform a form of high-level value estimation and compute values for given LDBA states. These values can be naturally leveraged for potential-basel reward shaping, Crucially, we adopt Bayesian perspective on estimating the transition kernel over the LDBA: by choosing a suitable prior distribution, we ensure that intrinsic rewards are informative from the initial phases of learning, This is done by optimistically assuming that the agent is capable of transitioning to any adjacent LDBA state in a single step, although this might. not be easily afforded by the dynamics of the enviromment. Moreover, by updating the distribution according evidence, the assumed transition kernel can be adapted over time realistically represent the agent's 's bchavior and environment's 's dynamics.
Our method, named 2RL.2 (Directed Reinforcement Learning from Linear Temporal Logic), is illustrated in Figure D and is capable of driving deep exploration in reinforcement learning from LTL specifications. The contributions of this work can be outlined as follows:
we design and introduce a method for exploration reinforcement learning when learning from LTL specifications, by casting the LDBA as Markov reward process and leveraging it for value estimation and distillation of intrinsic rewards;
2. we analyse the proposed method and the suboptimality potentially induced by intrinsic rewards;
3. we evaluate the method across diverse settings, spanning from simple tabular cases to complex, high-dimensional environments, which pose a significant challenge for reinforcement learning from L.T. specifications.
Scction 2 provides an introduction LTL and its connection to reinforcement lcarning. Our method is described in Section and evaluated in Section discussion of related works and of the proposed one can be found in Sections and G respectively.
2

---

Published in Transactions on Machine Learning Research (06/2025)
2
Background
This section provides a brief introduction to LTT. and discusses connections to reinforcement learning. For complete introduction, we refer the reader to Baier & Katoen (2008)
Lincar Temporal Logic LTL formulas build upon a finite set of propositional variables (atomic propositions, AP), over which an alphabet is defined as the powerset Σ = 2AP, i.e. the combinations of variables evaluating to true.
As more conerete, illustrative example, let us consider a farming robot, which is tasked with continually weeding through any of three different fields. The presence of the robot in each field could be described by the set of atomic propositions {a, c,. When the robot is operating in the first field, would evaluate to true (T), while b and would evaluate to false (1).
Definition 2.1. (LTL Formula) An LTL formula is composition of atomic propositions (AP), logical operators not (-) and or (1) and temporal operators next (X) and until (U). Inductively:
if E AP, then p is an LTL formula; if é and are LTL formulas, then 010, X and @U 0 are LTT. formulas.
Intuitively, while logical operators encode their conventional meaning, the next operator evaluates to true if its argument holds true at the very next time step, and until is a binary operator which requires its second argument to eventually evaluate to true, and its first argument to hold true until this happens. From this sulficient set of operators, additional ones are often defined in order to allow more concise specifications. In the context of reinforcement learning for control, useful operators are fimally (F(ø) == TUØ) and globally (G(pp) := -)) Returning to example, they could be used to specify stability (FGa, i.e., reach and remain in the first field), or avoidance (G-a, i.e., never enter the first field). A more complex task, which requires the farming robot to visit. the first. and third fields, repeatedly, while always avoiding the second one, could be simply represented as (a& (c))&(G-b)) Through this work, we will refer to this task as To-
Each LTL formula can be satisfied by an infinite sequence of truth evaluations of AP (i.e., an w-word). While direct definition is also possible (Thomas 1990), for simplicity, satisfaction will be introduced through the acceptance of paths in an automaton built from the formula.
From Formulas to Automata A practical way of defining satisfaction involves the introduction of Limit Deterministic Büchi Automata (LDBAs). An LDBA can be constructed from any LTL formula Sickert et al. 2016 and is able to keep track of the progression of its satisfaction.
Definition 2.2. (Limit Deterministic Büchi Automaton - LDBA) An LDBA is a tuple L = (8,E, PB, ",,,b bu), where B is a finite set of states, Σ is an alphabet, p8 : B x - 2 is a non-deterministic transition function, B* C B is set of accepting states, and by E B is the initial state. There exists a mutually exclusive partitioning of B BD U BN such that B C BD and for (b, E (BD x Σ) then (B a) S Bp and [P8 a)l =
In LDBAs synthesized from LTL formulas, additional propertics hold (Sickert et al. 2016 First, the alphabot is over evaluations of alomie propositions Σ = 2AP Second, the non-determinism limited to a subset of so-called e-transitions, which arise for specific formulas, e.g. those encoding stability problems. As a consequence, this class of LDBAs is known Good-for-MDDPs (Hahn et al. 2020), since the non-determinism can be resolved on the fly in arbitrary MDPs without changing acceptance.
An infinite sequence of LDBA actions (a:)80 E I induces multiple paths, where a single path can be defined as a sequence of LDBA states p= (b:) The set of induced paths Px can be defined recursively: Po {(bg)} and P.- = {(bo...., b; bb))(bu...., b,,1) E P.-1. E p (bs-1,,;)). Intuitively, each path may split if the selected LDBA action transitions to multiple states.
Definition 2.3. (Acceptance) An LDBA accepts a path (bx) if and only if the path visits an accepting state b' 3 infinitely often, that is AL E N, 31 such that by B*.
3

---

Published in Transactions on Machine Learning Research (06/2025)
-aa|b]
(alb)
b
GF(a & XF.) G-b
Figure 2: Illustrative task To (left), and LDBA encoding the formula (right, with starting state marked as 0 and accepting state in green). The farming robot (in green) moves in a 2D plane, where three areas of different colors represent fields. fa, b, cf are atomic propositions that evaluate to true when the agent enters the yellow, blue and red field, respectively. trajectory satisfying the specification is shown.
By translating each LTL specification into an LDBA, it is now possible to tie formula satisfaction to the acceptance of a path: informally, an infinite sequence of AP evaluations (w-word) satisfies a formula yp if and only if the LDBA L synthesized from accepts a path (b:)0 induced by the w-word.
Let us consider the example in Figure [ for the illustrative task To and the LTL formula & (G)()))))))&&(GG))) The periodic LDBA path 20 is accepted, just as (0, 1,, although the latter takes average more steps to reach the accepting state. On the other hand, the paths (0) (0, (3)²) would not be accepted, neither ever reach the accepting state, with the second getling caught in sink state by violating the avoidance criterion in 4.
We note that this notion of success relics on conditions that are achioved eventually in the future, independently of temporal distance. While this leads to myopic behavior under naive optimization (Voloshin el al. 2023)
recent works (Bozkurt et al. 2020 De Giacomo et al.) 2020a Hasanbeig et al., 2020 Voloshin et al. 2023 propose an elegant rephrasing for formula satisfaction in an RI-friendly form, as we now describe.
Product MDPs and Policy Optimization The following part describes standard reinforcement learning terminology and then reconciles it with the introduced logic machinery.
Definition 2.4. (Markov Decision Process - MDP) A Markov Decision Process is tuple M = (S,A, P. probabilistic transition kerne(] R: S A + IR a reward function, y is a discount factor, and yo E A(S) is the initial state distribution.
where S and A are potentially continuous state and action spaces, P x A + A(S) is a
MDPs are the standard modeling choice for reinforcement learning environments; however, they are discon- nected from atomic propositions and unable to track progression over formula satisfaction. The semantics of APs can be grounded in MDP states through labeling function F S + Σ, which evaluates APs in each MDP state. On the other hand, progression over task satisfaction can naturally be stored in an LDBA, as its states encode sufficient information on the history of paths.
Finally, all three components (MDP, labeling function and LDBA) can be synchronized to ensure consistency between trajectories each of them and enable mapping policies to distribution over paths, and therefore likelihoods of formula satisfaction (Hasanbeig et al. 2018 Voloshin al. 2023). The first step to resolve the non-determinism by creating new action for each potential c-transition to state b B, thus defining new action set A = {ea/b E B} (Sickert et al. 2016). Then, can define product MDP, encompassing the underlying MDP and the LDBA.
Definition 2.5. (Product MDP) Given an MDP M and a LDBA L, their Product MDP is tuple
M" = ,* , px, Rx xx (10), where Sx = Sx Ax = AUAB, and po (s, b) = pn(s). 1s= Furthermore,
P(s'la,s): A.
px ((s', (s,b))
= 1 a a a= cb & = s
0
otherwise,
(A(S) represents the space of probability distributions over S.
4

---

Published in Transactions on Machine Learning Research (06/2025)
where b S b' indicates that there is e-transition between the two LDBA states b and V. Finally, the reward and discount factor are defined as
(b. E 3 0, otherwise
1,
% by B
R (b.)
(²())
(1)
1 otherwise.
Essentially, a policy learned over the product MDP has access to both low-level information (MDP states) and indicators of progress on the specified lask (LDBA states). The transition kernel over MM guarantees that both the underlying MDP and the LDBA evolve consistently. This synchronization achieved through the labeling function F. Through this construction, it is finally possible to connect trajectories (and, therefore, policies) to satisfaction of given LTL formula. Let us consider an LTL formula ş and its corresponding LDBA C, as well trajectory (s;, b2) in the product MDP MM Then, 7 += ip (r satisfies p) if and only if L accepts the path (6,)6", ie., the projection of to LDBA states. Finally, let us consider a policy т S - A(A*): the probability of π satisfying can thus be defined as the probability integral for trajectorics satisfying the formula: P(* F p) = Er-r +ppp. Optimizing policy и for salisfaction of an LTL specification ş can be expressed as finding x* E argmax,en P( + (p) Prior works (Hasanbeig et al. 2018 Voloshin et al. 2023 have proposed RL-friendly proxy objectives, which optimize a lower bound on the probability of LTL formula satisfaction:
(-1
TH E argmaax E TEI
ET, (== V2), where T' = P, = II 7 x (b.).
())
TIIT
Paraphrasing, nA maximizes the visitation count to accepting states in the LDBA under eventual discounting. For formal analysis of the policy recovered by this objective, we refer the reader to Voloohhn et al. 2003
Our work builds upon this formulation and devises an exploration method to compensate for its drawbacks.
That is, the reward function Rx is fundamentally sparse: the agent only receives feedback when significant amount of progress toward solving the task has been made, and thus an accepting LDBA state is visited. As a result, while naive exploration might reach several non-accepting LDBA states, the agent remains unable to evaluate them, as is largely uninformed of the yet unexplored parts of the LDBA. Our method distills the global known structure of the LDBA in a denser intrinsic reward signal for exploration.
3 Method: Directed Exploration in Reinforcement Learning from LTL
Our method relies on (i) repurposing the LDBA as a Markov reward process by assigning a transition kernel, as well as rewards and discount signals for each transition, (ii) defining a value estimation operator to compute high-level values for cach LDBA stato, and finally (iii) leveraging these values for potential-based reward shaping. This procedure is described in Section 3.1. It takes an LDBA and transition kernel as input and returns intrinsic rewards for each transition in the product MDP. A second and crucial component, discussed in Section 3.2 is the estimation of the LDBA transition kernel, which is essential for ensuring informative intrinsic rewards: by taking Bayesian perspective, we show that a symmetric prior can induce strong exploration. Finally, Section 3.3 connects each component and describes a practical instantiation of the algorithm.
3.1 High-level Value Estimation from LDBA
As described in Section 2 an LDBA can be naturally synthesized from given LTT. specification, through well-known schemes (Sickert et al.) 2016). We now show how an LDBA can be recast as Markov reward process, which can be leveraged for computing values for each LDBA state. This construction requires 2 ingredients, namely (i) an LDBA L, and (ii) a transition kernel K over LDBA states, where K is a stochastic matrix such that K2, ER,Px,, P(b' = by bz), i.c., an estimate of the probability for the LDBA transition to state by starting from by under some policy ग, assuming stationarity. The choice of the transition kernel K is crucial for the effectiveness of the method and is thus treated in detail in the following section.
Having access to these two ingredients, we can define a discrete Markov reward process L (B, R* RR,7"" ,>*,bu): the state space B and initial state by are left unchanged and coupled with the transition kernel K. Moreover,
5

---

Published in Transactions on Machine Learning Research (06/2025)
provide reward and discounting functions: Rx and 7x are projection of the eventual reward and discounting scheme to the IDBA, as they are only dependent on LDBA states (see Equation [ A trajectory 7 = (bo, bi....) can be sampled from the MRP according to p(T) = K As any Markov reward process, the newly synthesized one allows computing the value function under eventual discounting (b) = Ex :o== T, with b44 ~ ((b)). The Markov properly over the MRP induces the following
Bellman equation (Sutton & Barto 2018):
Vx= = R + yx @ (KVK),
33)
where matrix notation is adopted: VK. R and 7x are represented as [B]-dimensional vectors, and @ stands for the Hadamard product. As the LDBA (and thus the MRP) is discrete and finite D the Bellman equation defined over the MRP has closed-form solution (Sutton & Barto 2018
K = 7x O K)
(4)
where Il represents the identity matrix. As the MRP is closcly related to the product MDP M an analysis of Once value estimates Vx are computed, they can be treated as po-
their connection is provided in Appendix B
tential function for reward shaping [g et al. 1999 although under eventual discounting (Voloshin et al. 2023 :
Riner -b,0)= (b)Vv(1 Vx(()).
=
(5)
This reward signal can be added to the product MDP reward Rx and optimized with an arbitrary reinforcement learning algorithm. We note that, as an instantiation of potential-ban baseed reward shaping, the optimal policy in the product MDP remains invariant this reward transformation, eventual discounting converges zero
PR* Proposition 3.1. (Consistencyy) Let us consider the product MDP M (8*, A PX R* R², PO and R* + Rintr; 22,1,) Under eventual discounting, any optimal policy in
its modification M = M for which r, (=30 0 is also optimal in M
The proof follows the general scheme for potential-based reward shaping (gg et al. 1999 and extends it to the eventual discounting setting (see Appendix A}.
While this procedure allows the synthesis of an intrinsic reward signal for arbitrary logic specifications, the informativeness of this signal relies on two factors. The first factor is the existence of a sink state, which occurs across many (but not all) LDBAs constructed from LTL formulas (c.g., formulas involving global avoidance, as the illustrative lask To). Its absence can be remedied by augmenting the MRP state space with a virtual sink state, reachable from all other states and associated with an eventual reward and discount factors of 0 and 1, respectively (sce Appendix C for complete discussion and evaluation). The second factor lies in the transition kernel K. While Proposition 3.1 guarantees that no kernel perturbs the optimal policy, it does not quantify how chosen kernel affects learning efficiency. The following section outlines how a careful choice of its initialization and estimation is crucial to the practical effectiveness of the algorithm. Other alternatives are ablated empirically in Appendix F
3.2 Optimistic Priors for High Level Value Estimation
Lel us consider a naive approach to the choice of the transition kernel K, which simply computes the expected empirical transition probability of the current policy т. As shown at the top of Figure 3 for the illustrative task To, a randomly initialized policy can be exccuted in the product MDP, and K can be estimated through the empirical count of observed transitions in the LDBA. As long as the policy does not spontaneously visit the accepting state, values and rewards estimated through Equations 4 and are uniformly zero and fail to drive exploration. The method would thus be rendered ineffective.
In order to address this issue, we adopt a Bayesian approach to the problem of estimating the LDBA transition kernel K. Let us consider each row K,, which models a categorical probability distribution over future
We remark that the MRP is constructed from the LDBA, which discrete nature, and from the underlying MDP, which can be potentially continuous. In the rase of exceedingly complex specifications, and thus large LDBAs, iterative methods could be viable replacement.
6

---

Published in Transactions on Machine Learning Research (06/2025)
Trajectories
Empirical
Intrinsic Rewards Ruds
K
P(K)
D)
Posterior P(K
0.9
9.05
0.0
0.05
0.4
0.3
0.0
0.3
0.0
38
0.0
0.7
0.0
0.37
0.3
G6
0.0
0.0
0.0
1.0
0.0
0.0
0.0
1.0
Figure Left: a randomly initialized policy exccuted in the product MDP M for TO; its empirical transition kernel R results in uniformly zero value estimates Vx. Right: the expected value for K over posterior distribution estimated from symmetrie prior results in informative value estimates and intrinsic rewards.
LDBA states from cach LDBA state b; E B. At its corc, our method proposes a prior distribution over these categoricals, such that appropriate shaping of the prior controls and directs the exploration in the product MDP. As the conjugate prior to categorical distributions, we adopt a Dirichlet prior K; ~ P(K,) = Dir(a,,o...... (..0,00.....,0,111)--))) -1) The prior is informed of the LDBA structure by setting aij = if the LDBA does not allow transitions from b, to by. For the m remaining non-zero Dirichlet parameters, we adopt partially symmetric prior by setting them to shared value a where is hyperparameter controlling the strength of the prior: large values of a induce slower convergence of the posterior distribution to the empirical transition kernel.
We remark that the choice of symmetry corresponds to the assumption that, at each step, the agent is capable of transitioning to each adjacent LDBA state with equal probability. In practice, the agent might actually take several steps in the underlying MDP in order transition lo any different LDBA state; moreover, some LDBA transitions can be substantially harder achieve than others. Finally, for complex problems, naive exploration may not even result in observing the full set of possible transitions in a practical number of time steps. However, assuming that the agent is capable of transitioning under a max-entropy distribution allows reward signals to propagate to all states, thus resulting in informative estimates for the high-level value Vx and the intrinsic rewards shaping terms Rutr. For the illustrative example To, this is displayed in the bottom part of Figure 3
Furthermore, while the initialization of K is possibly unrealistic, the Bayesian framework provides a natural way to update it as an N-step trajectory D (b) is gathered the product MDP:
P(KID) & P(DIK))((K)
(6)
for each i E [O,.... "Q....,|B|], [B]] This update is tractable due to the choice of a conjugate Dirichlet prior for the categorical likelihood described by the transition kernel. As training progresses, a posterior distribution P(K) D) can be updated with collected evidence. In practice, the updated posterior for state by E B is simply P(K, Dir(a,, + C,o, .ao....,,.jpp |B- + C, BJ-1), where Cr2 is the count of LDBA transitions from state by to state by observed far. Moreover, instead of computing high-level values for specifie transition kernel K in Equation 4
compute the expected value V under the posterior distribution of transition kernels P(K)) and thus of MRPs:
E K~P(KID
VK] = E [T xx 2 K)- K-P(KID)
We remark that the maximization of V corresponds to the average-case MDP problem, while other procedures can be easily adapted to solve the Robust MDP (Xu & Mannor 2010) the Percentile Criterion MDP problems (Delage & Mannor 2010). In practice, the expectation in Equation 7 can be estimated by sampling, with the special case of Thompson Sampling when a single sample used. Our approach to estimating the transition kernel ablated empirically in Appendix a study of the hyperparaneter a controlling prior strength in Appendix G
7

---

Published in Transactions on Machine Learning Research (06/2025)
3.3 Practical Algorithm
This section combines the elements out- lined above into practical scheme for distilling an intrinsic reward, which is ro- ported in Algorithm ! On top of the abil- ity to sample trajectories from the prod- uct MDP and access to its LDBA, the algorithm only requires the specification of a prior distribution P(K) over LDBA transition kernels, which is proposed in Section 3.2 The output is a policy π op- timizing an eventually discounted proxy to the likelihood of task satisfaction.
Algorithm 1 DRL
Input: Product MDP M prior distribution P(K) for each iteration do
Execute policy in MM to collect data D for N steps
Updale posterior P(KID) with evidence D (Eq. 6
Compute high-level values V (Eq. 7
Sample training batch B (cither on- or off-policy)
Add intrinsic reward to batch B (Eq.
Train i with B through arbitrary RI. algorithm end for
4 Experiments
This section presents an empirical evaluation of the method by investigating the following questions:
Can 2RL2 drive deep exploration in reinforcement learning from LTT, specification?
How does DRL2 perform across different environments and specifications?
Can DRL2 be scaled to high-dimensional continuous scttings?
As the method is designed to handle the full complexity of L.TL, our evaluation considers several logic specifica- tions, encompassing reach-avoidance (e.g., Fa&G(-b6) and subtask sequences (e.g, To Ga&&&X F Fc)&G-6). In order to focus on exploration, the suite of formulas allows casily scaling the number of LDBA states, or the minimum number of steps required in the underlying MDP to induce a transition in the LDBA. To investigate the final question, perform an evaluation in both tabular and continuous domains. While the former avoids confounding effects arising from function approxination, the latter stresses the ability to scale to complex underlying environments. This also evaluates the versatility of DRL?; as it is in practice coupled with tabular Q-learning (Watkins & Dayan 1992) and Soft Actor Critic (Haarnoja et al. 2018a), respectively. In the first case, the environment involves navigation in a 2D gridworld, while in the latter we evaluate dexterous manipulation with a simulated Fetch robotic arm and locomotion of a 12DoF quadruped robot and 6DoF HalfCheetah. A detailed description of the benchmark environments and specifications is provided in Appendix M code is available at github..omm/maragg..
Baselines We compare DRL to:
1. a counterfactual experience replay schemne (LCER Voloshin et al. 2023
2. a novel count-based baseline P that relies on inverse square rool visitation counts of LDBA states to compute a potential function for reward shaping (Tang et al. 2017). If nbb) is the visitation count of I.DBA state e B from the beginning of training, the intrinsic reward for the high-level transition
b - b' is simply computed as Rmmr (b, b') = > (b) Vn(vT Vn(i)
3. the underlying learning algorithm with no additional exploration bomuses; this corresponds to simply DRL2
setting Rimtr (b, b')
All shared hyperparameterss are set to the ones maximizing the performance of the No exploration baseline; the prior strength is the main hyperparameter introduced by DRL?, and is simply set to 10 in all tabular experiments, and 105 in all continuous experiments. For a thorough discussion on hyperparameters, we refer to Appendix M We note that other promising approaches for exploration in the LTL domain exist, but they rely on meta-learned components or ad-hoc training regimes (Qiu et al. 2023 Wang et al. 2023 and are thus not suitable for a fair comparison.
"This baseline is, to the best of our kuowledge, novel, the application of standard RL exploration idcas the MRP/MDP derived from the LDBA has not been thoroughly investigated. We choose count-based approach as the MRP is discrete, and does not require hashing or contimuuus generalizations Burda al. (2019), while straightforward application reward-bass based optimistic methods
possible, the reward of the MRP known.

---

Published in Transactions on Machine Learning Research (06/2025)
Reach-avoid, easy
Reach-avoid, medium
Reach-avoid, hard
FaBC(-b)
Returns
Returns
Returns
2.5
2.5
2.5
0.8
0.0
200
50
100k
5ok
150
200
Steps
Steps
Steps
Sequential, easy
Sequential, medium
Sequential hard
60
Returs
Return
Returns
SO
100
150
200k
k
100
150
200
k
100
192 k
200
Steps
Steps
Steps
Circular, easy
Circular, medium
Circular, hard
GF(-8XF( (XF( BY)
Returns
10
Returns w
Returns
50k
100k Steps
k50
200
100 k
150
200
50k
100 k
150 k
200
Steps
Steps
DRL
2
LCER
Count-based
No exploration
Figure 4: Return for Q-learning under eventual discounting. The three rows display reach-avoidance, sequential and circular tasks, as illustrated on the right with optimal policies. Each atomic proposition evaluates to in cells of matching color; difficulty increases from left to right. Further details are available in Appendix M 2RL2 is able to drive exploration when naive exploration is insufficient.
4.1 Tabular Setting
We first evaluate the exploration performance of DRI, by coupling with tabular Q-learning (Watkins & Dayan 1992p when operating over discrete state and action spaces in the standard online episodic sctting (Sutton& & Barto 2018). The evaluation enviromment is deterministie 2D gridworld, in which the agent can move in each of the four cardinal directions by one unit at each timestep. The first row of Figure evaluates reach-avoidance task G(a&=b)), in which the agent needs to avoid large area that covers all but a corridor. The goal area is at the end of said corridor; and the difficulty of the task increases with the length of the corridor. In this case the benefit of DRL2 is evident, as it returns a negative reward whenever the agent leaves the corridor, and the LDBA thus transitions to a sink state. The agent can therefore direct its exploration towards fraction of the state space, resulting in improved sample efficiency. On the other hand, count-basod shaping can only penalize transitions to the sink state once it has been visited enough times. While L.CRR has the advantage of potentially ignoring failures by hallucinating counterfactual LDBA states during training, it cannot discourage exploration of the forbidden area. We remark that LCER remains a strong method significant when exploration of the underlying MDP is not necessary; a detailed discussion is provided in Appendix E
The second and third row of Figure evaluate sequential tasks. In both, the agent navigates a room with several zones. In the first case, the agent must reach a sequence of zones in a given order; in the second one, this must be repeated indefinitely while also avoiding the center of the room. While the standard reward under eventual discounting would be zero until the last zone in the sequence is reached, DRL? provides an informative reward at each LDBA transition, thus informing the agent to direct exploration towards promising directions. Therefore, as number and size of the zones grows (lo the right), DRI.2 results in more efficient exploration by encouraging LDBA transitions towards the accepting state. This encouragement is instead only dependent on visitation counts for the count-based bascline and absent in LCER. We additionally evaluate variations of these tasks in Appendix D
4.2 Continuous Setting
After verifying the effectiveness of DRL2 in interpretable scttings, this section investigates if the exploration signal can be scaled to high-dimensional, long-horizon environments requiring the application of deep reinforcement learning algorithms. For simplicity, we evaluate its application to Soft Actor Critic (SAC)
9

---

Published in Transactions on Machine Learning Research (06/2025)
Petch, avoid
Doggo, avoid
Cheetah, frontflip
Retums
Retums
60
10
100
300
200 k00k
120
200
400
Steps
Steps
Steps
Fetch, allgn
Doggo, navigate
Cheetah, sequential
33
Returns
Returns
23
13
Steps
Steps
Steps
DRL
LCER
Count-based
No exploration
Figure 5: Return for SAC under eventual discounting on Fetch (left), Doggo (center) and HalfCheetah (right), shown in renderings. DRL² confirms its ability to drive exploration in complex tasks when coupled with deep reinforcement learning.
(Harroja et al., 2018a), which stands as fundamental building block for many algorithms [Eyeebbahh et al, 2019 Haarnoja et al. 2018b; Iharz et al.) 2021 Kumar et al.) 2020). On the top of Figure 5 a simulated Felch robotic arm (de Lazcano et a 2023) is evaluated on two lasks, namely (i) moving its gripper to a specific location while avoiding lateral movements and (ii) gradually producing an horizontal alignment of three cubes. In the middle, an HalfCheetah receives specifications encoding, respectively, finite sequences of positions and infinite sequences of angles for its center of mass, resulting in precise horizontal locomotion, and in front flipping indefinitely. On the bottom, a 12DoF simulated quadruped robot (Ray et al. 2019) is tasked with (i) fully traversing narrow corridor, or with (ii) navigating through two zones in sequence. As in the tabular case, the four lasks can all be described through LTL formulas encoding reach-avoidance and sequential behavior. They are reported among further details on the environments in Appendix M
As expected, in this sctting the evaluation is significantly noisier and partially constrained by the learning algorithm. Nevertheless, we observe that DRL2 is competitive with the stronger baselines in simpler problems, and likely to outperform them when exploration in the underlying MDP becomes more challenging. Interestingly, we observe that counterfactual experience replay (LCER) is less effective in this sctting, We remark that LCER can generate unfeasible states for the product MDP, which can be harmful when the agent has the ability to interpolate between training samples.
5 Related Work
Logic for Task Specification in RL LTL among several logic languages for task specification in reinforcement learning: for instance, numerous related works have investigated Reward Machines (Camacho et al. 2019 Icarte al.] 20118 2022: Vaezipoor et al. 2021). While Reward Machines can handle regular expressions, LTL is designed to address a superset, namely w-expressions. As consequence, LTL gains the ability to reason about infinite sequences and tasks including liveness and stability.
For this reason, several works, including our own, have investigated LTL for task specification. Early attempts focused on reconciling logic and policy optimization through the definition of a product MDP and the design of a reward signal encouraging task satisfaction (Bozkurt et al., 2020 Camacho et al., 2017: 2019: Hasanbeig
ct al.] 2018 2020: Kantaros 2022; Li ct al.) 2017). Several works relied on houristic reward shaping schemes
iL et al. 2017 which gradually evolved lowards dynamic or eventual rewarding and discounting schemes
Cai et al. 2021 De Giacomo et al. 2020a Hasanbeig et al. 2018 2020 Voloshin et al. 2023). This led to
the development of principled approaches, proposing schemes that provably and directly optimize lower bound on the likelihood of formula satisfaction (Shao & Kwiatkowska
2023 Voloshin et al. 2023
As for the optimization of such schemes, while linear programming is sufficient for known dynamics and finite action spaces, Q-lcarning approaches have been adopted when a model of the environment is not available (Bozkurt al. 2020 Cai et al. 22021] Hasanbeig et al. 2018). A fundamental restriction of this approaches was lifted by adopting actor-critic (Hasanbeig et al.
2020 policy gradient (Voloshin et al.
10

---

Published in Transactions on Machine Learning Research (06/2025)
methods suited for contimuous action spaces. Nevertheless, in this case, empirical demonstration of LTI. -TTddddedd reinforcement learning have remained mostly constrained to low-dimensional setting.
2023
This work builds on top of these efforts, and adopts established rewarding and discounting schemes. We focus, however, on the specific problem of exploration, and propose a method to densify the reward signal. Furthermore, leveraging modern actor-critic methods, we extend our empirical evaluation to high-dimensional, complex environments.
Exploration in Logic-driven Reinforcement Learning A significant effort has been targeted at addressing the sparsity arising from existing rewarding schemes (Hasanbeig et al. |018: [Voloshin et al. 2023
involving the use of heuristics (T.i et al. 2017), an accepting frontier function (Hasanbeig et al.J 2018 2020
bonuses for first visitations (Cai et al.) 2021 , or the knowledge of additional information such as annotated
maps (Xiong et al.) 2023). Recently, Shah al. (2024) also propose heuristic scheme for shaping constraints expressed in LTL. This scheme is partially aligned with the shaping signal that DRL² naturally recovers, but only considers accepting paths and is restricted to on-policy methods. Directly within the LTL literature, another line of work leverages the discrete structure of automata and learns hierarchical (Hasanbeig et al., 2020 Icarte et al.) 2022; Jothimurugan et al.) 2021), goal-conditioned (Qiu et al.] 2023 or modular (Cai iet al. 2021) policies. While considerably improving sample efficiently, the approaches listed so far are known to potentially introduce suboptimality (Icarte et al. 2022). In contrast, DRL22 recovers the optimal policy
under mild assumptions, as described in Appendix
In the parallel direction of Reward Machines, several works investigate reward shaping for reinforcement learning from logic specification. Camacho et al. (0117) consider potential functions (s) of both the MDP and automaton states; among those, they invest igale counting the minimum number of steps to reach an accepting automaton state, which is equivalent to computing values under a specifie automaton transition kernel. Another work (Icarte et al.) 2022) explores an extension, which is also fundamentally related to our method: the authors investigate value iteration on an MDP synthetised from the automaton to compute a potential function for reward shaping, thus leveraging the semantics of the task. While motivated by a similar intuition to ours, a naive application of this method would not be viable in an eventually discounted setting, which involves w-regular problems, as we report in Appendix F. By adopting an LDBA instead of a DFA, and more importantly by integrating an eventual discounting scheme, our method is able to avoid myopic behavior while handling the full complexity of LTL. Futhermore, DRL2 docs not require assumptions on controllability by defining a Markov reward process instead. Values estimated in the MRP are thus softer than the optimal ones in a corresponding MDP, and we find them to be more informative for exploration. We validate this discussion empirically, by evaluating optimal transition kernels under eventual discounting in Appendix F By updating its distribution over MRP transition kernels, it is moreover capable of providing an adaptive and informative reward signal, rather than static one derived from a hard assumption.
Beyond reward shaping, some works leverage control over the automaton to produce synthetic experience by relabeling the LDBA states of collected transitions. Such schemes have been proposed in the context of Reward Machines (Tcarte et al. 2022) and L.TI. (Voloshin et al.] 2023); ; as they can produce off off-policy samples, they cannot be naively applied to on-policy methods, as discussed in Appendix [ Other relabeling techniques only larget the initial LDBA state (Wang al. (220)) or focus on optimality guarantees (Shao & Kwiatkowska, 2023). These methods are essentially orthogonal to DRL2 (see Appendix E and may be combined. Finally, we note that previous work have also led to strong exploration on unseen tasks, as the result of a meta-learning phase when a distribution over MDPs can be accessed ltt al. 2021).
León et al. 2022 Vaezipoor
To the best of our knowledge, our approach novel in its adaptive and informed estimation of the high-level Markov reward process, resulting in a directed exploration method that retains optimality.
Directed Exploration in Reinforcement Learning In this work, we use the word directed with a specific meaning, as 2RL2 directs the agent towards accepting LDBA states, by rewarding LDBA transitions towards them. In contrast, count-basod methods promote transitions to any unvisited LDBA state, and may thus be considered undirected. Nonetheless, this idea has parallels in non-logie-oonditonnd reinforcement learning, as direction can be given with respect to entities beyond accepting states. In this context, directed
11

---

Published in Transactions on Machine Learning Research (06/2025)
has been used in conjunction to the Bayesian notion of information, in order to promote exploration of states that are maximally informative of some quantity (e.g.. reward (Lindner et al.. 2021 D, value estimate
(Nikolov et al., 2019 or learned dynamics (Guo & Brunskill 2019)).
Another way to provide direction or guidance is in the context of action-masking methods (Stolz et al. 2024 Theile et al., 2024), which pose hard constraints on actions that can be selected by the agent. DRL provides milder feedback through an intrinsic reward term, and does not explicitly prevent actions from being taken. Finally, many works have explored goal-conditined RL as technique
guide and improve exploration Eysenbach et al. 2022), with several works at the intersection with LTL (Qiu et al. 2023 Yalcinkaya et all 2024). Similarly to goal-conditioned RL, our work extracts reward from specific task (in our case, a logic-formula); however, this task is unique, and we do not consider the standard multi-goal/ saaliiggal/uuivvraaalll value function formulation (Schaul et al. 2015) that is at the core of goal-conditioned RL.
6 Discussion
This work proposes DRL?, an exploration method for reinforcement learning from LTL specifications. By casting the LDBA encoding the specification as a Markov reward process, we enable a form of high-level value estimation, which can produce value estimates for each LDBA state. These values can be leveraged as a potential function for reward shaping and combined with an informed Bayesian estimate of the LDBA transition kernel lo ensure an informative training signal. As a result, DRL accelerates learning when non-trivial exploration of the underlying MDP is necessary for reaching accepting LDBA state, is often the case for complex specifications.
Limitations 2 generally capable of improving exploration in L.T--condiiooned RL; however, we do not expect it be useful for all tasks, and we suggest four such instances. First, while DRL² reduces sparsity in reward signal distilled from LTL specifications, the shaped reward is not entirely dense. Intuitively, instead of receiving a non-zero reward when accepting state is visited, the agent receives it at every LDBA transition. However, if naive exploration is insufficient to induce an LDBA transition, exploration remains challenging. For this reason, we expect our method to be insufficient in environments with extremely long horizons and rare LDBA transitions. Second, in tasks in which each MDP state can be associated with many LDBA states, or presenting e-transitions, a replay method such as LCER is often sufficient, and, while can be scamlessly combined, DRL² may not provide significant improvements (see Appendix E. Third, DRL,2 relies on an symmetric prior over LDBA transitions, which is in general effective, but could be misleading for specific tasks and MDP morphologies. Fourth, several other exploration schemes, we note that 2RL2 introduces slight non-stationarity in the reward signal, which needs to be addressed by the underlying learning algorithm and might be problematic in very stochastic environments, especially for off-policy algorithms. Nevertheless, this is a common issue of intrinsic exploration methods, which is in practice often neglectable Burda et al. (2019). Finally, and perhaps foremost, DRL" relies on the availability of a correct LDBA, and a ground-truthe accurate labeling function infer AP evaluations from states. While this assumption is shared by the bulk of works in LTL-conditioned RL, real-world deployment of such algorithms would require algorithms that are robust to partial obsorvability and noise, and capable of jointly inferring the labeling function from data, which we highlight as an important research direction.
Outlook This work opens up exciting future directions, including a formal analysis of which reward shaping terms would not only grant consistency, but also maximize sample efficiency. Moreover, as DRL2 leverages the LDBA structure, its effectiveness is dependent on it. Its applicability can thus further benefit by L.DAA construction algorithms that do not return arbitrary LDBA in its equivalence class, but rather the one which is most suitable for guiding a reinforcement learning agent.
Conclusion This work addresscs the fundamental problem of sparsity for complex LTL tasks by dircctly leveraging their structure. Thus, we believe that the evidence provided in this work further supports the effectiveness of reinforcement learning as a paradigm for extracting controller from a logic specification.
12

---

Published in Transactions on Machine Learning Research (06/2025)
Acknowledgments
We thank Nico Gürtler for precious discussions throughout the project, and the anonymous reviewers for their valuable leedback. Marco Bagatella is supported by the Max Planck ETH Center for Learning Systems. This project has received funding from the Swiss National Science Foundation under NCCR Automation, grant agreement 51NF40 180545. Georg Martius member of the Machine Learning Cluster of Excellence, EXC number 2064/1 Project mumber 390727645. We acknowledge the support from the German Federal Ministry of Education and Research (BMBF) through the Tübingen AT Center (FK7: 01T818039B).
References
David Abel, Will Dabney, Anna Harutyunyan, Mark K Ho, Michael Littman, Doina Precup, and Satinder Singh. On the expressivity of markov reward. Advances in Newral Information Processing Systems, 2021.
Rajeev Alur, Suguman Bansal, Osbert Bastani, and Kishor Jothimurugan. A framework for transforming specifications in reinforcement learning, In Principles of Systems Design: Essays Dedicated to Thomas A. Henzinger on the Occasion of His 60th Birthday. 2022.
Christel Baier and Joost-Picter Katoen. Principles of model checking. MIT press, 2008
Alper Kamil Bozkurt, Yu Wang, Michael M Zavlanos, and Miroslav Pajic. Control synthosis from lincar temporal logic specifications using model-free reinforcement learning. In 2020 IEEE Internalional Conference on Robotics and Automation (ICRA), 2020.
Yuri Burda, Harrison Edwards, Amos Storkey, and Oleg Klimov. Exploration by random network distillation. In International Conference on Learning Representations, 2019.
Mingyu Cai, Mohammadhosein Hasanbeig, Shaoping Xiao, Alessandro Abate, and Zhen Kan. Modular deep reinforcement learning for continuous motion planning with temporal logic. IEEE robotics and automation letters, 2021.
Alberto Camacho, Oscar Chen, Scott Sanner, and Sheila Mcllraith. Non-markovian rewards expressed in Itl: guiding search via reward shaping. In Proceedings of the International Symposium on Combinatorial Search, 2017.
Alberto Camacho, Rodrigo Toro Icarte, Toryn Q Klassen, Richard Anthony Valenzano, and Sheila A Mcllraith. Tul and beyond: Formal languages for reward function specification in reinforcement learning. In Proceedings of the Twenty-Eight International Joint Conference on Artificial Intelligence, 2019.
Giuseppe De Giacomo, Marco Favorito, Luca locchi, Fabio Patrizi, and Alessandro Ronca. Temporal logic monitoring rewards via transducers. Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning, 2020a.
Giuseppe De Giacomo, Luca Iocchi, Marco Favorito, and Fabio Patrizi. Restraining bolts for reinforcement learning agents. In Proceedings of the AAAI Conference on Artificial Intelligence, 2020b.
Rodrigo de Lazcano, Kallinteris Andreas, Jun Jet Tai, Scungjac Ryan Loe, and Jordan Terry. Gymnasium robotics. githuu, 2023. URL http::/gitthb.
Erick Delage and Shie Mannor. Percentile optimization for markov decision processes with parameter uncertainty. Operations research, 2010.
Benjamin Eysenbach, Abhishek Gupta, Julian Ibarz, and Sergey Levine. Diversity is all you need: Learning skills without a reward function. In International Conference on Learning Representations, 2019.
Benjamin Eysenbach, Tianjun Zhang, Sergey Levine, and Russ Salakhutdinov. Contrastive learning as goal- conditioned reinforcement learning. Advonces in Neural Information Processing Systems, 35:35603-3568
2022.
13

---

Published in Transactions on Machine Learning Research (06/2025)
Zhaohan Daniel Guo and Emma Brunskill. Directed exploration for reinforcement learning. orXiv preprint MXXi::106.0070000 2019.
Tuomas Haarnoja, Aurick Zhou, Picter Abbeel, and Sergey Levine. Soft actor-critic: Off Off-policy maximum entropy deep reinforcement learning with stochastic actor. In International conference on machine learning, 2018a.
Tuomas Haarnoja, Aurick Zhou, Kristian Hartikainen, George Tucker, Schoon Ha, Jie Tan, Vikash Kumar, Henry Zhu, Abhishek Gupta, Pieter Abbeel, al. Soft actor-critic algorithms and applications. arXiv preprint ar (tfe:1812.05900 2018b.
Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, and Dominik Wojtczak. Good-for-mdpp automata for probabilistic analysis and reinforcement learning. In Tools and Algorithms for the Construction and Analysis of Systems, 2020.
Charles R Harris, K Jarrod Millman, Stéfan Van Der Walt, Ralf Gommers, Pauli Virtanen, David Cournapeau, Eric Wieser, Julian Taylor, Sebastian Berg, Nathanicl Smith, et al. Array programming with numpy. Nature, 2020.
Mohammadhosein Hasanbeig, Alessandro Abato, and Daniel Kroening. Logically-constrained reinforcement learning. Xiv preprint arxiv: 1801: 881.00099, 2018.
Mohammadhosein Hasanbeig, Daniel Kroening, and Alessandro Abate. Deep reinforcement learning with temporal logics. In Formal Modeling and Analysis of Timed Systems: 18th International Conference, FORMATS 2020, 2020.
Shengyi Huang, Rousslan Fernand Julien Dossa, Chang Ye, Jeff Braga, Dipam Chakraborty, Kinal Mehta, and João G.M. Araújo. Cleanrl: High-quality single-file file implementations of deep reinforcement learning algorithms. Journal of Machine Learning Research, 2022.
Julian Ibarz, Jie Tan, Chelsea Finn, Mrinal Kalakrishnan, Peter Pastor, and Sergey Levine. How to train your robot with deep reinforcement learning: lessons we have learned. The International Journal of Robolács Research, 2021.
Rodrigo Toro Icarte, Toryn Klassen, Richard Valenzano, and Sheila Mcllraith. Using reward machines for high-level task specification and decomposition in reinforcement learning. In International Conference Machine Learning, 2018.
Rodrigo Toro Icarte, Toryn Q Klassen, Richard Valenzano, and Sheila A Mcllraith. Reward machines: Exploiting reward function structure in reinforcement learning. Journal of Artificial Intelligence Research, 2022.
Kishor Jothimurugan, Suguman Bansal, Osbert Bastani, and Rajeev Alur. Compositional reinforcement learning from logical specifications. Advances in Neural Information Processing Systems, 2021.
Yiannis Kantaros. Accelerated reinforcement learning for temporal logic control objectives. In 2022 IEEE/RS) International Conference on Intelligent Robots and Systems (IROS), 2022.
Jan Kietínský, Tobias Meggendorfer, Salomon Sickert, and Christopher Ziegler. Rabinizer 4: from Itl to your favourite deterministic automaton. In International Conference on Computer Aided Verification, 2018.
Aviral Kumar, Aurick Zhou, George Tucker, and Sergey Levine. Conservative q-learning for offline reinforce- ment learning. Advances in Neural Information Processing Systems, 2020.
Borja G León, Murray Shanahan, and Francesco Belardinelli. Agent, do you see it now? systematic generalisation in deep reinforcement learning. In ICLR Workshop Agent Learning in Open- Endedeed,,, 2022.
Xiao Li, Cristian-Ioan Vasile, and Calin Belta. Reinforcement learning with temporal logic rewards. In 2017 TEFE/RSJ International Conference Intelligent. Robots and Systems (TROS), 2017.
14

---

Published in Transactions on Machine Learning Research (06/2025)
David Lindner, Matteo Turchetta, Sebastian Tschiatschek, Kamil Ciosek, and Andreas Krause. Information directed reward learning for reinforcement learning. Advances in Neural Information Processing Systems, 2021.
Andrew Y Ng. Daishi Harada, and Stuart Russell. Policy invariance under reward transformations: Theory and application reward shaping. In International Conference on Machine Learning, 1999.
Nikolay Nikolov, Johannes Kirschner, Felix Berkenkamp, and Andreas Krause. Informatiio-ddirecte ex- ploration for deep reinforcement learning. In International Conference on Learning Representations, 2019.
Adam Paszke, Sam Gross, Soumith Chintala, Gregory Chanan, Edward Yang, Zachary DeVito, Zeming Lin, Alban Desmaison, Luca Autiga, and Adam Lerer. Automatic differentiation in pytorch. NIPS 2017 Workshop Autodiff, 2017.
Amir Pnneli. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science (sfes 1977), 1977.
Martin L Puterman. Markov decision processes: discrete stochastic dynamic progromminng. John Wiley & Sons, 2014.
Wenjic Qiu, Wensen Mao, and He Zhu. Instructing goal-conditioned reinforeement learning agents with temporal logic objectives. In Thirly-seventh Conference on Neural Information Processing Systems, 2023.
Paulo Rauber, Avinash Ummadisingu, Filipe Mutz, and Jürgen Schmidhuber. Hindsight policy gradients. International Conference on Learning Representations, 2019.
Alex Ray, Joshua Achiam, and Dario Amodei. Benchmarking safe exploration in deep reinforcement learning. gym 2019.
Tom Schaul, Danicl Horgan, Karol Gregor, and David Silver. Universal value function approximators. In International conference on machine learning, pp. 1312-1320. PMLR, 2015.
Ameesh Shah, Cameron Voloshin, Chenxi Yang, Abhinav Verma, Swarat Chaudhuri, and Sanjit A Seshia.
Deep policy optimization with temporal logic constraints. arXic preprint orXiv:2404.1157, 2024.
Daqian Shao and Marta Kwiatkowska. Sample efficient model-free reinforcement learning from specifications with optimality guarantces. In Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence, 2023.
Salomon Sickert, Javier Esparza, Stefan Jaax, and Jan Kictínský. Limit-deterministic büchi automata for linear temporal logic. In International Conference on Computer Aided Verification, 2016.
David Silver, Satinder Singh, Doina Precup, and Richard S Sutton. Reward is enough. Arlificial Intelligence, 2021.
Roland Stolz, Hanna Krasowski, Jakob Thumm, Michael Eichelbeck, Philipp Gassert, and Matthias Althoff. Excluding the irrelevant: Focusing reinforcement lcarning through continuous action masking. In The Thirly-eightt Annual Conference on Newral Information. Processing Systems, 2024.
Richard S Sutton and Andrew G Barto. Reinforcement learning: An introduction. MIT press, 2018.
Haoran Tang, Rein Houthooft, Davis Foote, Adam Stooke, OpenAI Xi Chen, Yan Duan, John Schulman, Filip DeTurck, and Pieter Abbeel. # exploration: A study of cosnt-based exploration for deep reinforcement learning. Advances in neural information processing systems, 2017.
Mirco Theile, Lukas Dirnberger, Raphael Trumpp, Marco Caccamo, and Alberto L Sangiovanni- Langiovamni-Vnnceneelle Action mapping for reinforcement learning in continuous environments with constraints. orXiv preprint 2:Xii:2412.04322 2024.
15

---

Published in Transactions on Machine Learning Research (06/2025)
Wolfgang Thomas. Chapter 4- automata on infinite objects. In Formal Models and Semantics, Handbook of Theoretical Computer Science, pp. 133-191. Elsevier, Amsterdam, 1990.
Mark Towers, Jordan K. Terry, Ariel Kwiatkowski, John U. Balis, Gianluca de Cola, Tristan Deleu, Manuel Goulão, Andreas Kallinteris, Arjun KG, Markus Krimmel, Rodrigo Perez- Virez-Vicente, Andrea Pierré, Sander Schulhoff, Jun Jet Tai, Andrew Tan Jin Shen, and Omar G. Younis. Gymnasium, 2023. URL https
Pashootan Vaczipoor, Andrew C Li, Rodrigo A Toro Icarte, and Sheila A Mcilraith. Lt12action: Generalizing Itl instructions for multi-task rl. In International Conference Machine Learning, 2021.
Cameron Voloshin, Hoang Le, Swarat Chaudhuri, and Yisong Yue. Policy optimization with linear temporal logic constraints. Advances in Neural Information Processing Systems, 2022.
Cameron Voloshin, Abhinav Verma, and Yisong Yue. Eventual discounting temporal logic counterfactual experience replay. In International Conference on Machine Learning, 2023.
Chuanzheng Wang, Yinan Li, Stephen Smith, and Jun Liu. Continuous motion planning with temporal logic specifications using deep neural networks. arXiv preprint arXi::204.002610 2020.
Jun Wang, Hosein Hasanbeig, Kaiyuan Tan, Zihe Sun, and Yiannis Kantaros. Mission-driven explo- ration for accelerated deep reinforcement learning with temporal logic task specifications. arXiv preprint
17X1092311.1705,, 2023.
Christopher JCH Walkins and Peter Dayan. Q-learning. Machine learning, 1992.
Zikang Xiong, Joe Eappen, Danicl Lawson, Ahmed H Qureshi, and Suresh Jagannathan. Co-lcarning planning and control policies using differentiable formal task constraints. arXiv preprint 2xXiv2333.0033/6 2023.
Huan Xu and Shie Mannor. Distributionally robust markov decision processes. Advances Neural Information Processing Systems, 2010.
Beyazit Yalcinkaya, Niklas Lauffer, Marcell Chanlatte, and Sanjit A Seshia. Compositional automata embeddings for goal-conditioned reinforcement learning. In The Thirtt-eighth Annual Conference on Newral Information Processing Systems, 2024.
16

---

Published in Transactions on Machine Learning Research (06/2025)
A Proof of Proposition 3.1 and Further Analysis
This section presents proof for Proposition 3.1 in Scction 3 which we also report in its entircty for case of reference, and further discusses how the intrinsic reward is informed by the lask.
Proposition A.1. (Consistency) Let us consider the product MDP M = (8* ils modification M = , ,,,,KRR* + Rintr, (,, Under eventual discounling, any optimal policy in M for which r, =0 0 also optimal in M
, mā and
The proof consists of simple extension of known results on potential-based reward shaping to account for eventual discounting. Let us consider an arbitrary state-action pair (so. ao) E Sx x and the optimal Q-function in M under eventual discounting:
(gg el al.
1999
(1 au) = E
(s,,0 + (intr a, (,,
(8)
t=
00
E
r R (5c, Ce. s1+1) + Σ I Rinee (st, ae, sc+1))
(9)
p',Px
t=
Q50 an)
rst Rine aes S6+1))
(10)
xx
1=0
(7
E
r' (8)+) ((bet)) V(b)))
(11)
px
x=
20
(so, an)
+ E
r x ((++1) Σ r'V(b)))
(12)
xx
1=
1=
(5, an) + lim
E
(b.( - 77%
(13)
1000
(5o, ao)
lim
E
[VV(bb)) - ((b))
(14)
7 Px
where Q is the optimal Q-function in M under eventual discounting. the assumption holds, and T, 52 0, then the second term fades, and we have
(16, an) = (sp an) - (sp))
(15)
The difference between the two Q functionss Q7 and Q7 is therefore constant at any given state. Thus,
* (s)
argmax (s, a) = argmax as) (s). aEAx*
(16)
oEAx
As stated above, this invariance relies on the assumption that the product of discounts converges to zero, which would happen in case an accepting state is visited infinitely often | Intuitively, once good policy is found, the contribution of the intrinsic reward fades, and there is no incentive for optimization algorithms to update the policy away from its optimum. While this assumption often holds for the optimal policy (e.g., in deterministic environments). there are cases in which this may not be true (e.g., in the stochastic case, if the LDBA features a sink state). Nevertheless, we note that the assumption holds for optimal policies in tasks considered in this paper, and in recent literature /Voloshin et al. 2023
infinitely many times over an infinite horizon, which occurs and only the policy satisfies the formula. In practice, decays exponentially fast as the number of visits until increases: 7 0.99 and an accepting state has been visited, say, 1000 times, then T2 10-4.
Formally, convergence to zero only happens if the agent visits accepting
17

---

Published in Transactions on Machine Learning Research (06/2025)
On the other hand, in cases in which the assumption does not hold (e.g.; often happens for random initialized policy): the intrinsic reward can in principle still bias the policy and drive exploration well. For instance, let us assume that the likelihood of visiting an accepting LDBA state under the current policy я is
exactly zero. This implics (-) = O, y*(+) (.) = 1 and r; = II yx (br) = 1. In this case, the value under
uventual discounting for an arbitrary stale 8g E S* is
V2 (30, 90) =
E
( (s,,,,,. + Rintr aes (t, ((+1))]
(17)
m px
E
Rintr (8t, aes S1+1))
(18)
x:
E
(84+4)((b241)) -V(ba)
(19)
Px
lim V(b.)) - Vbo)..
(20)
Px
Thus, policy optimizing the value function under eventual discounting with the intrinsic reward provided by DRL also maximizes the likelihood of eventually reaching the LDBA state with maximum high-level value V. It is easy to show that this corresponds to the accepting state by in the LDBA as the high-level value of any LDBA state b E B is (bb) = (1 - Pa (-bb)b))V((b)) < V(b*,, where P=(-b*(b) is the likelihood of never reaching the accepting state under the current policy.
We can thus conclude that a policy trained with DRL preserves its asymptotic optimality, while also benefiting from an informative exploration signal during carly stages of training.
B Connection Between MRP and Product MDP
This section discusses the relationship between product MDP (introduced in Section 2 and MRP (described in Section 3 in further detail. Let consider a trajectory in the product MDP T ((su, bu), b1),........ Due to the construction of the MRP, the return of the projection of 7 to the MRP state space (in this case, b1,.,), is the same the return of in the product MDP, evaluated according to R and yx. A similar argument can be made for a policy π given a fixed starting state (Sp, by). If the MRP transition kernel K is a projection of the transition kernel induced by æ in the product MDP, then the value Vx (bn) computed in the MRP matches the value computed in the product MDP (T bn)). Nonetheless, we remark that the MRP can be seen as a high-level approximation of the product MDP, and as such it loses information. Thus, it may not be straightforward leverage the MRP to accurately compute values for arbitrary MDP states, the best of our knowledge.
C Addition of a Virtual Sink State
As described Section 3.1 a design choice in DRT? involves the construction of a virtual sink state for LDBAs that do not feature one, where a sink state can be defined as an LDBA state b, e B such that (B b..
Let us consider LDBA featuring path from each state to accepting state. Moreover, let consider transition kernel K with full support over reachable LDBA states (as is the case for likely samples under the prior proposed in Section 3.2). In this case, the values computed under eventual discounting by solving Equation would be uniform: VK = - As a consequence, intrinsic rewards computed through Equation would be constantly zero until an accepting state is visited and thus uninformative. This natural consequence of the fact that, irreversible failure is not possible, any policy inducing transition kernel with good enough support will satisfy the specification, considering infinite horizon.
18

---

Published in Transactions on Machine Learning Research (06/2025)
Sequential, easy
Sequential, medium
Sequential hard
&
Returns
Returns
Returns
20
20
20
10
59
100 Steps
150
200
k
100k
150k
200
k
190 Steps
100k
200
Steps
DRL2 2
DRL2 w/o virtual sink
No exploration
Figure 6: Ablation of the addition of a virtual sink for DRL?. When a sink state is not featured nor added (e.g. in sequential tasks), the performance of the No-exploration baseline is recovered.
In order to provide an informative learning signal, DRL augments LDBAs that do not feature sink state with a virtual one and assumes that it can be reached from any other LDBA state. We note that this is equivalent with associating each LDBA state with a discount factor equal to the likelihood of transitioning to the virtual sink. While this can introduce myopic behavior (Voloshin et al.) 2023). we remark that DRL2 also learns and updates its estimate of the LDBA transition kernel. As any virtual sink state cannot in practice be reached, the likelihood of transitioning to it from each visited LDBA state converges to zero as the number of environment steps increases. Thus, as training progresses, any virtual sink is effectively removed, together with any degree of myopia introduced.
Among the tasks considered in Figure MRPs for sequential tasks do not naturally feature a sink state. To support the discussion, we additionally provide empirical evidence on the performance DRL,² these tasks when a virtual sink is not added. We note that performance on other tasks would not be affected, they naturally feature sink state.
In Figure e we observe that DRL2 without a virtual sink state recovers the performance of the No-exploration bascline, as expected. Experimental scttings are the same as those outlined in Section
D Additional Tabular Results
UMaze Optimal policies for the reach-avoidance tasks from Figure 4 (first row) would also solve a shortest- path reaching problem in the underlying MDP. In other words, linear path to the goal does not violate the constraints. We now evaluate variation of the original task, by reshaping the safe area of the reach-avoid task into a U-shape. In this case, the shortest path to the goal violates the avoidance constraints. Fortunately, changing the shape of the avoidance zone only results in a local change to the labeling function F. DRL?, as well as other baselines, can handle arbitrary relabeling functions; thus these methods can adapt to arbitrary environment layouts.
Results are reported in for all task variants (easy, medium and hard). In general, as the path length has now increased, performance globally decreases accordingly. Nevertheless, the overall relative performance of each methods is consistent with the original version of the task. We note that LCER (Voloshin et al. 2023 now outperforms the count-based baseline, as it can effectively ignore previous visits to the zone to avoid. In the extreme case in which the length of the U-maze is very large, but the starting position is very close to the goal if the avoidance constraint is ignored, we expect LCER to perform even better.
U-reach-svoid, easy
U-reach-avoid, medium
U-reach-avoid, hard
Fa8C(-b)
75
Returns
Returns
5.0
2.5
10
100 Steps
k50k
200
50
100k Steps
150
200
50k
100 k
150 k
200k
Steps
DRL2
2
LCER
Count-basee
No exploration
Figure 7: Alternative evaluation of reach-avoid task involving a conflict between reaching objectives and avoidance constraints. Results are consisted with those in Figure 4
19

---

Published in Transactions on Machine Learning Research (06/2025)
Maze, easy
Maze, medium
Maze, hard
10
Returns
Returns
Returns
k0
100k Steps
150
200
100 Steps
150K
200
50
100
150K
200
Steps
DRL
LCER
Count-based
No exploration
Figure 8: Alternative evaluation of sequential task in the shape of maze. Results are consistent with those in Figure 4
Sequential, distant
Sequential, close
Returns
Returns
50
100
150
200
50
100
190
200
Steps
Steps
DRL
LCER
Count-based
No exploration
Figure 9: Comparison of DRL?, LCER and additional baselines in the Sequential task from Figure (left) and an additional variation (right). LCER performs very well when significant exploration of the underlying MDP is not required, as is the case for the example on the right. To the left of each set of training curve, the task is represented, and an optimal policy is visualized.
Sequential maze We additionally evaluate alternative layout of the sequential task, which considers greater number of APs, and in which the sequence of zones to visit leads to the exit of a maze with several intersections (see Figure 5). We scale the difficulty by increasing the areas of each zone. As the reward signal syuthesized by DRL2 mostly depends on the structure of the LDBA, we observe consistent results with the sequential tasks in Figure
E
Comparison to LTL-guided Counterfactual Experience Replay (LCER)
The environments and tasks presented in Section 4 require significant exploration in the underlying MDP and stress the ability to leverage the semantics of LDBA states to accelerate this process.
LTL-guided Counterfactual Experience Replay (Voloshin et al. 2022 takes an orthogonal approach to the problem of exploration when learning from LTL formulas and represents a very strong baseline in specific environments. In particular, I.CER does not leverage the semantics of the LDBA, however it generates synthetic experience by fully controlling its dynamics. Transitions ((s, ()s,b),ar a, ()), with {(s, 6), (s', 6')3 C S* and A are relabeled by uniformly resampling the initial LDBA state and simulating the LDBA transition caused by action a, resulting in a new transition ((s,)), a, ('))
Generated transitions respect the transition kernel of the product MDP and are thus valid training samples. However, the method does not guarantee that relabeled product states (s, 6) are actually feasible, as the set of reachable product states might only consist of a manifold of the full Cartesian product of MDP and LDBA state spaces. For instance, let us consider the illustrative task To as displayed in Figure 2 at any step, if the agent is in the red field, the LDBA would necessarily be in its sink state and in no other state. Any relabeling of this particular state would thus not be relevant. Furthermore, LCER cannot generate on-policy data, as the on-policy action sampled in (s, b) might be different than the original action sampled in bs,b) (Rauber et al. 2019
form of state relabeling,
Nevertheless, LCER remains a very strong exploration method in environments in which each MDP state can be associated with several LDBA states; furthermore, in the presence of sink LDBA states, LCER can hallucinate their avoidance. In this merit, we report an additional experiment in Figure
0 evaluating DRL?, LCER and baselines in modified version of the Sequential environment from Figure 4 In its original version
20

---

Published in Transactions on Machine Learning Research (06/2025)
Reach-avold, medium
Sequential, medium
Circular, medium
7.5
Returns
Retums
Returss
20
2.5
60
100
50
100
150
200
50
120 Steps
150 200
Steps
Steps
DRL2
Partially informed prior
VT kernel
Empirical kernel
Figure 10: Ablation of kernel initialization and estimation methods. symmetric prior, as used by DRI?, performs reliably.
Results suggest that an informed
(on the left), the accepting LDBA state can only be visited once the distant final zone (in bright purple) is reached. In this case, LCER is not effective. However, if the zones are rearranged in way such that they be visited without excessive exploration in the underlying MDP (e-g., by placing them closer to the starting MDP state, as done on the right), the performance of LCER largely improves, fully bridging the gap with DRL We note that the modified version the task requires fewer steps to reach an accepting state from the starting one; the baseline without exploration incentives also solves the task, albeit less efficiently. For evaluations on additional variations of tabular tasks, we refer the reader to Appendix DarixxDaan and
LCER and DRL thus address different issues in exploration from logic formulas. Fortunately, the two methods are orthogonal and can be freely combined.
F Kernel Estimation Ablation
Proposition 3.1 states that, under specific assumptions, optimal policies are invariant to the proposed reward shaping. In fact, Proposition 3.1 holds for any choice of transition kernel K. In practice, the choice of kernel still impacts the quality of exploration and sample efficiency. We ablate this choice by comparing the effectiveness of kernels sampled by our methods with several others, to assert what constitutes "good" kernel for exploration.
We remark that DRL averages its values over transition kernels sampled from posterior distribution to a symmetric Dirichlet prior. We compare this choice to three additional ones:
kernels sampled from partially informed prior, which differs from the one used in DRL2 due to its lack of knowledge over the connectivity of the MRP/LDBA. except for its sink state. Tt essentially assumes that transition between any LDBA state pair is always possible.
transition kernel obtained using value iteration (VT), and that therefore represents the optimal policy under assumption of full controllability of an high level MDP. It represents a naive implementation of the reward shaping introduced in Icarte et al. (2022). This kernel has the lowest entropy possible, as value iteration outputs a deterministic policy.
an empirical kernel, which simply counts LDBA transitions performed by the policy in the product MDP. This kernel does not leverage the LDBA strueture, and is visualized in Figure 3
These ablations are evaluated in the medium variants of the three tabular tasks from Figure to highlight performance differences; all experimental parameters are unchanged.
Results are presented in Figure 10 We observe that a partially informed prior can recover part of DRL"'s performance, but suffers as the size of the LDBA increases (Sequential, medium). The transition kernel obtained through VI performs well in some tasks, and less in other: since the optimal policy under eventual discounting assigns similar values to non-sink LDBA states, reward shaping becomes less informative. Finally, choosing the empirical kernel generally leads to low performance, as discussed in Figure
21

---

Published in Transactions on Machine Learning Research (06/2025)
Reach-avoid, hard
Sequential, hard
Circular, hard
7.5
30
Returrs
Returns
Returns
5.0
50
0
53k
100k Steps
150
200
50
100 Steps
150
200k
130 Steps
200
100
10
a
10
10
a 104
Figure 11: Ablation of prior strength hyperparameter a.
G Prior Strength Ablation
This Section performs empirical evaluation of the effect of the hyperparameter a, which controls the strength of the prior over MRP transition kernels in DRT.2 We ablate the default choice (a 1000) in the hard variant of tasks from the tabular evaluation in Figure 4 Overall, in Figure 11 we observe that DRL is fairly robust to this hyperparameter. Performance is generally lower for weak priors (a < 100), which can be significantly affected by poor trajectories collected by the initial policy. As the prior informed by the LDBA structure, we find that it generally provides good guidance even for stronger priors. We note that, in case the prior is misinformed, weaker prior would indeed be favorable.
H Product MDP Ablation: States and Rewards
The product MDP formulation that our method builds upon (Voloshin et al. 2023) can be used to formally connect eventually discounted returns and likelihoods of formula satisfaction, but strictly requires a binary 1/0 reward signal. Morcover, the agent state space is defined as the product between LDBA and MDP states. In this section, we empirically evaluate trends that arise if these two properties are violated.
States In principle, the agent needs access to both high-level LDBA states (tracking formula satisfaction) and low-level MDP states, tracking fine-grained details. While this is necessary to provably recover an optimal policy for arbitrary MDPs and formulas, it also causes a blow-up of the state space, which makes exploration more difficult. As rewards are only defined as a function of the LDBA states, one might be tempted directly learn a policy (and value function) from LDBA states alone æ B Ax This decision has the large much smaller state space, and the disadvantage of losing information about low-level MDP information. This is evident in the empirical evaluation
advantage of operating
present for tabular tasks in Figure 12 (see curves for LDBA-only. Across all tasks, the optimal value function is not invariant with respect to the MDP state; thus, value estimates are inaccurate, and the policy does not solve any of the tasks for the entirety of training.
Reach-avoid, easy
Sequential, easy
Circular, easy
X.5
Returns
Returns
Returns
10
5.0
20
2.5
50
100k
150
50k
100
150k
200k
50k
100 Steps
150k
200
Steps
Steps
DRL
No exploration
LDBA-only
Reward-shift
Figure 12: Evaluation of additional basclines in easy tabular tasks: LDBA-onia trains a policy directly on the LDBA/MBL /RRP state, and Reward-shift shifts rewards to {-1/1]
22

---

Published in Transactions on Machine Learning Research (06/2025)
FGa
Reach-stabilize
Returns
100k
Steps
DRL
LCER
Count-based
No exploration
Figure 13: Evaluation of DRL and baselines on the task FGa in presence of jump transitions.
Rewards The eventual discounting framework manages to retrieve proxy to an infinite-horizon objective by adopting discount factor of exactly 1 for non-accepting transitions. As consequence, the reward function for such transitions needs to be exactly zero. If this assumption is violated, the value function of policy which does not visit an accepting transition infinitely often will diverge to (possibly negative) infinity. For this reason, from a formal perspective, the binary reward signal is crucial. However, in practical setting, one can apply an affine transformation to the reward signal, shifting it as (b) = 2R(b) - 1 E f-1,1), thus punishing each timestep that does not transition to an accepting state. We evaluate this heuristic solution in tabular settings and observe interesting results Figure 12 In simpler tasks (e.g., reach-avoid), this solution performs very well. This can be traced back to the fact that the Q-values are initialized zero: while under R they not updated until accepting state is visited by chance, in this case they will decrease soon the corresponding action is executed. This encourages the agent to prioritize yet unattempted actions, driving efficient exploration. This effect leads this bascline to match the performance of DRL in simpler tasks, but is less effective in more complex tasks (e.g, circular), in which struggles to learn and is outperformed by the existing No- fo-eepllration baseline.
Evaluation with e-transitions
This section evaluates application in presence of e-transitions. e-transitions oceur in a subset of automala, particular for stability specification; our method, as well as baselines considered, are compatible with theis existence. Thus, now evaluate the task FGa in reach-avoid tabular settings. This setup is similar to that of the correspouding experiment in recent work (Voloshin et al. 2023 Overall, as the structure of the LDBA is minimal, we observe that all considered methods perform reasonably well in Figure 13 In particular, DRL,2 and the count-based baseline slightly improve over the No-exploration baseline. LCER (Voloshin et al. 2023 works particularly well, as the task does not involve several substeps, but presents irrecoverable failures when 'jumping' at the wrong time. We refer to Appendix E for a further comparison between DRL2 and LCER.
J Evaluation under Stochasticity
Stochastic initial state Experiments in Figure 4 initialize the agent in a fixed state. Our evaluation does not however depend on this assumption. In order to verify this, we repeat the evaluation for the reach-avoid task, and sample the initial state uniformly from a rectangle in the leftmost part of the "corridor".
Reach-avoid,
Reach-avoid, medium
Reach-avoid, hard
10
Beturss
Beturns
Returns
50
100
200
50k
100
150k
200
50
150k Steps
100
200
Steps
Steps
DRL
LCER
Count-based
No exploration
Figure 14: Evaluation of 2RL2 and baselines on the task Fa&G-b with stochastic initial states.
23

---

Published in Transactions on Machine Learning Research (06/2025)
Reachravoid, medium
meduumm medium
Circular, medium
Retums
Returns
Returns
50
20
2.5
10
100
150
Steps
Steps
Steps
DRL
LCER
Count-based
No exploration
Figure 15: Evaluation of DRL and baselines on medium tabular tasks from Figure
with sticky actions.
Reothravoid, medium
Sequential, mediuum
Circular, medium
Retums
Returns
Returns
5.0
2.5
53k
100k
150 200
Steps
Steps
Steps
DRL
2
LCER
Count-basee
No exploration
Figure 16: Repetition of tabular experiments while replacing Q-learning with SARSA.
In Figure 14 results are consistent with those the original setting, with all methods being slightly more sample-efficient as they can be initialized in more favorable position in some episodes.
Sticky actions We additionally repeat the tabular evaluation while injecting a difference source of stochasticity; sticky actions. Inspired by evaluation protocols on ATARI, with probability 0.1 at each step, we force the environment to ignore the agent's 's action and simply repeat the action from the previous time-step. This induces both stochasticity, and a slight partial observability, as the transitions now depend on previous actions well. We report results in Figure 15] We observe that the overall trends from the original, deterministic variants are are largely reproduced, with an expected overall slight drop in performance. This suggests that the evaluated methods at least in part robust to stochasticity.
K
Evaluation under On-policy Learning
DRL2 is in principle agnostic the underlying RL algorithm, as it relies simply reward shaping. We further validate this property empirically, by re-evaluating tabular problems of medium difficulty from Figure g and replacing Q-learning for SARSA Sutton & Barto (2018). In Figure 16 we observe that the overall sample efficiency decreases for all method, which is consistent with the on-policy nature of SARSA. Nevertheless, the relative performance of all methods remains consistent with the results obtained with Q-learning.
L Additional Metrics
Reach-avoid, easy
Reach-avoid, medium
Reach-avoid, hard
Ratio viclationn
Ratio of viclationn
Ratio of villation
1.0
0.5
0.5
0.5
0.0
0.8
Steps DRL 2
Steps
Steps
LCER
Count-based
No exploration
Figure 17: Evaluation of DRL22 and basclines on the task Fa&G-b terms of violations of the avoidance constraind G-b.
24

---

Published in Transactions on Machine Learning Research (06/2025)
Sequential easy
Sequential, medium
Sequential, hard
1.0
1.0
1.0
Returns
Returns
Returns
0.5
0.5
0.5
0.0
Steps
Steps
Steps
DRL 2
LCER
Count-based
No exploration
Figure 18: Evaluation of the likelihood formula satisfaction in finite time for sequential tasks from Figure 4
DRL² satisfics the formulas from the carliest episodes, while its eventually discounted return grows during the initial stage of training. Intuitively, this means that the agent reaches an accepting state earlier and earlier.
Contraint violations While the standard evaluation in Figure Sigurerrppore reports returns under eventual discounting, this section additionally reports the ratio of training episode that violate the avoidance constraints in the task G-&G-b. In Figure 17 observe that, expected, this metric is largely negatively correlated with evaluation returns: in order to maximize the likelihood of formula satisfaction, constraint violations need to be minimized. We additionally note one interesting trend: the count-based baseline quickly compensates the high rate of violations for a randomly initialized policy and quickly minimizes the violations. However, it requires more training steps to also reliably reach the specified zonc
Formula satisfaction in finite time Our empirical evaluation mainly relics on eventually discounted returns as proxy for formula satisfaction. However, on some of the evaluation lasks, we can evaluate an additional metric. Namely, on sequential tasks without avoidance constraints, it is sufficient to visit an acceptance state once to satisfy the formula. While estimating the likelihood of visitation over infinite horizons remain intractable, we can evaluate the likelihood of a policy to visit an accepting state (and therefore satify the formula) within the episode length. We report an empirical estimate of this quantity in Figure [8] obtained by computing bootstrap confidence intervals of a satisfaction indicator across seeds. We observe that variance over seeds is limited: therefore, the plot closely resembles clipped version of the metrics reported in Figure 4
M Implementation Details
This section presents a thorough description of methods, tasks and hyperparameters. For the sake of reproducibility, we provide our full codcbase C
M.1
Environments and Tasks
Throughout the paper, experiments involve simulated environments.
M.1.1 Tabular Environments
The environments considered in tabular settings (Figure 4 are variants of the common gridworld, that is 2D grid, with one cell being occupied by the agent. The action space is discrete and includes 5 actions, four of which allow movement in cach of the cardinal directions, and a single no-op action. The observation space contains x and y coordinates of the agent and is therefore 2-dimensional. While dynamics are shared, the labeling function from MDP states to atomic propositions and task-dependent details differ across tasks and are reported below. We note that each task is also represented in the rightmost column of Figure 4 although not to scale for illustrative purposes.
Reach-avoidance Reach-avoidance is evaluated in a gridworld without obstacles (Figure top). The agent is initialized al one end of a thin corridor (of unit width). The other end of the corridor is not bounded;
fggthabb.oom/marraggg...o
25

---

Published in Transactions on Machine Learning Research (06/2025)
however, the AP evaluates to true in each cell of the corridor beyond a fixed distance from the starting cell. The AP I evaluates to true anywhere outside the corridor. The formula evaluated is Fa&G-b. The difficulty of the task can be scaled by increasing the distance to the zone to reach (7, 9 and 11 for easy, medium and hard task variants, respectively). Episodes have a duration equal to the minimum number of step to reach the final zone, plus 10 steps.
I also takes place in a gridworld without obstacles. Contiguons 7 x squares are aligned horizontally. The agent starts at the center the leftmost square; in each square to the right, a different AP evaluates to true, in alphabetical order. In the first square to the right of the starting one, evaluates to true, in the second b evaluates to true and so on. Difficulty can be scaled by specifying longer formulas: ([oX:XF(6
Sequential The second task in Figure
and F(b&:X((6 F(d are used, respectively, for easy, medium and hard tasks. Episodes have fixed length of 70 steps.
Circular Circular tasks (Figure bottom) present 5 contiguous 7 x squares, aligned a cross. The central zone represents obstacle: it is labeled to the AP e, and the agent cannot reach its central 6 6x6 6 cells. The other 4 zones are labeled as a, b, c, d in counterclockwise order, and the agent is initialized in proximity of the first one. The difficulty of the task can be controlled by scaling the number of zones involved in a and and hard lasks, respectively. An episode lasts for 70 steps.
loop: Fb) F( F(b&
for easy, medium
M.1.2 Continuous Environments
Section 4 also provides an evaluation on continuous, high-dimensional environments. Since evaluation of LuL-guided reinforcement learning has traditionally been mostly restricted to simple tabular (Icarte et al. 2022) or low-dimensional (Hasanbeig et al.) 2020 Voloshin et al. 2023) settings, we repurpose high-dimensional environments from safe and goal-conditioned reinforcement learning research.
Fetch Experiments reported in the first row of Figure 5 were developed on top of the common Fetch robotic benchmark dde Lazcano et al., 2023). and are also available as part of our codebase. We evaluate two tasks, in which the agent controls the end effector position of a 7DoF robotic arm with 4-dimensional actions over episodes of 50 steps. FetchAvoid reminiscent of the reach-avoidance task in tabular settings, and involves fully stretching out the arm while avoiding lateral movements (i.c., not entering red zones as shown in Figure 5 In this case, observations are 10-dimensional. In FetchAlign the agent has to interact with three cubes on one side of the table, and has to align them horizontally at the center of the table. In this case, observations include information on the cubes, and are 45-dimensional. The two tasks are specified, respectively, with the formulas Fa&GGm (reach the end of the table, and avoid lateral movements), and F( (position the first, second and then third block).
Doggo Doggo is 12DoF quadruped adapted from the most challenging tasks in SafetyGym (Ray et al, 2019). It is tasked with navigating a flat planc; observations are 66-dimensional, actions are 12-dimensional and the length of each episode is 500 steps. Similarly to other reach-avoidance tasks, DoggoAvoid involves navigation to a distant goal (shown in green Figure 5 ; in a straight line, while completely avoiding detours. On the other hand, DoggoLinear involves navigating through a sequence of 2 circular zones. These two tasks are encoded through the following two specifications: Fa&G-e and F(a&XFb). Episode length is set to 500.
HalfCheetah HalfCheetah (Towers al. 2023 involves controlling a 6DoF robot in a vertical 2D plane and is standard environments in the deep reinforcement learning literature. We define two tasks in this underlying environments. In CheetahSequential the agent is tasked with eventually reaching, in succession, 4 consecutive zoncs to its right, as encoded by the formula is reached, the task is solved and the agent can stop. In CheetahFrontflip the agent is informed by the formula (a(a& F(b::XF(ccxXX the main body of the robot, respectively when the Cheetah is its default position, standing on its front legs, upside down, and standing on its back legs. As a result, the formula is satisfied by an infinite sequence of front Notably, this task can not be satisfied by finite trajectories.
Once the last zone
where each variable evaluates to true for a given range of angles of
26

---

Published in Transactions on Machine Learning Research (06/2025)
M.2 Methods and Algorithms
The core of our method computes an intrinsic reward and is therefore applicable top of arbitrary reinforcement learning algorithms. Therefore, will first discuss the implementation of the method itself, well as relevant baselines, and then details involving reinforcement learning algorithms.
The proposed algorithm is detailed in Amgorithm 1 Its computational cost is dominated by the closed form solution the value in the Markov reward model (see Equation 7 which is cubic in the number of MRM states. However, since LDBAs for most common tasks in these settings are relatively small (< 20 states), the computational load is negligible, even when computing the expected value over the posterior via sampling.
The main hyperparameter introduced by DRL is a, which controls the strength of its prior as described in Section 3.2 It is set to 10x in tabular settings, and to 10a in continuous settings, where increased stability was found to be benefi- cial. The remaining hyperparameters for reward shaping are shared with the count-based baseline and are, respec- tively, the frequency of updates the potential function (set to 2000 environment steps), and scaling cocfficient to the intrinsic reward, which was tuned individually for each method in grid of [0.1, 10.0]. We found a coefficient of 0.1 to be optimal across all tasks for both methods in tabular settings, while contimous settings benefit from a stronger signal and a coefficient of 10.0. Intuitively, higher coefficients can lead to better value propagation during the exploration phase at the cost of stability in deep learning settings; however, we found their impact to be limited (especially in tabular settings), such that task-specific tuning was required. The two remaining baselines (relying LCER and no exploration techniques) introduce no additional hyperparameters on top of the learning algorithm.
Table 1: Hyperparameters for Q-learning and Soft Actor Critic.
Hyperparameter
Value
Y
0.99
Buffer size Batch size Initial exploration
4
64
103 steps
т (Polyak) Learning rate
5 10 for SAC
3 10-1 for SAC,
for Q-learning
The intrinsic reward is added to the extrinsic one and optimized under eventual discounting through one of two algorithms, depending on the setting. In practice, we rely on tabular Q-learning (Watkins & Dayan 1992) with an c-greddy policy (c=0.1) and Soft Actor Critic with automatic entropy tuning (Haarnoja et al., 2018b). In the tabular case, striet adoption of eventual discounting (Voloshin et al. 2023) results in a largely uniform policy, as in most states action would reduce the likelihood of task satisfaction. As a consequence, prohibitive number of steps would be required during evaluation for computing cunulative returns. For this reason, our practical implementation of tabular Q-learning does not apply eventual discounting, although this would be possible given a much larger computational budget. Our SAC implementation is partially based on that provided by Huang et al. 2022). Hyperparameters for each algorithm were tuned to perform best when no exploration bonus being used, and are reported in Tables D
They are kept fixed across tasks.
M.3 Metrics
Unless specified, the metric used to measure the methods' performance is cumulative return under eventual discounting, that is R = >' where 7 0.99 and N is the number of visits to an accepting LDBA state within episode. In the limit of N + co, this metric is a proxy for the likelihood of task satisfaction (Voloshin et al. 2023 All curves report mean performances estimated across 10 seeds, and shaded areas represent 95% simple bootstrap confidence intervals. They undergo average smoothing with a kernel size of 10.
M.4 Tools
Our codebase mostly relies on numpy (Harris et al. 2020 for numeric computation and torch Paszke et al. 2017 for its autograd functionality. Furthermore, we partially automate the synthesis of LDBAs from LTL formulas through rabinizer (Kretínský et al. 2018).
7 Available hwt...ooooommmaagg////222222
27

---

Published in Transactions on Machine Learning Research (06/2025)
M.5 Computational Costs
In principle, the distillation of the intrinsic reward according to DRL depends the size of the LDBA size. As we perform value estimation in the MRP built from the LDBA by computing the closed form solution of the Bellman equation, the complexity of this operation cubic in the LDBA size. This remains tractable for reasonably sized LDBAs with < 100 states, and the computational cost is in practice negligible for the LDBAs in our empirical evaluation. For very large LDBAs, sampling-based alternatives for approximate value estimations should be considered instead.
When considering the training times of the underlying RL agent, all methods have comparable runtimes within their setting (tabular or contimuuus). Each experimental run required 8 cores of modern CPU (Intel i7 12th Gen CPU or equivalent). Each run in tabular and continuous settings required on average ~30 minutes and 150 minutes, respectively.
28


Reviews:
[{"review_id": "ZORrzbQ4Pq", "reviewer": "Reviewer_Gef2", "summary": "", "questions": "", "limitations": "", "rating": null, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "Strengths:\n\n- Addressing exploration challenges in RL settings such as multi-stage tasks, safety constraints, and repeated goals, is both necessary and nontrivial.\n- The approach reframes the LDBA as an MRP (with eventual discounting), which is then leveraged for potential-based shaping. While reward shaping in automata-based RL is not entirely new, the Bayesian perspective on transition probabilities—along with an informed prior—fills a gap in earlier logic-driven RL research. Shaping based on “high-level” value estimates from the LDBA can counteract reward sparsity and direct exploration more effectively than prior baseline approaches.\n- The experiments are systematically split between tabular (discrete) and continuous (high-dimensional) settings, demonstrating that DRL2 is not restricted to small toy problems. Also, the tasks exhibit varied forms of LTL formulas (reach-avoid, repeated visitation (GF), multi-step sequences (U and X), and so on) which validate the generality of the proposed method. The paper’s chosen environments form a reasonable test bed: 1) They cover both discrete and continuous settings. 2) They systematically scale LTL complexity and environment difficulty. 3) They demonstrate that DRL2 can handle typical RL tasks (navigation, manipulation, locomotion) under LTL constraints, showing promise for broader adoption.\n\n- The paper offers a clear exposition of LDBAs, the product MDP construction, and the eventual discounting scheme. The derivations for potential-based shaping under eventual discounting are nicely explained, including references to prior work on policy invariance.\n\n\nWeaknesses:\n\n- Task Difficulty vs. Generalization: While the paper shows environments of varying sizes and complexities (e.g., gridworlds of different corridor lengths, continuous control tasks like Fetch and HalfCheetah), all tasks are still somewhat hand-crafted to highlight specific properties (reach-avoid, multi-step sequences, etc.). It would be interesting to see if DRL2 generalizes well to less structured or more chaotic environments—for instance, tasks that do not neatly separate into corridor vs. obstacle, or that involve a variety of sub-tasks simultaneously. As it stands, the suite focuses on “classical” logic tasks, which are helpful as controlled benchmarks, but don’t necessarily confirm how DRL2 would perform in truly open-ended or partially observable domains.\n\n-  LTL Formula Design: The chosen formulas (Fa&G¬b, GF(a&XFc), etc.) indeed represent classic temporal motifs (reachability, avoidance, repeated visits). However, they do not show certain other patterns (e.g., complex nesting of temporal operators, mixing multiple U operators, heavily nested G/F forms). While the “suites” let the authors systematically scale up the minimal number of steps or the number of subgoals, it might be that real-world LTL tasks have more subtle structures. A broader variety of formula types (or multiple deadlines, concurrency constraints, etc.) might further test DRL2’s flexibility.\n\n- Scalability and State Space: Although the paper does push beyond small toy settings to robotics tasks, it remains unclear how DRL2 scales if the LDBA itself becomes large (e.g., a formula with dozens of states). The authors do mention that typical LTL tasks yield relatively small LDBAs (< 20 states), so it may be a non-issue in practice. But if the environment is also massive (very high-dimensional), it might still be challenging. The method is presumably suitable for bigger grids or longer horizon tasks, but the paper’s largest discrete domain has episodes of maybe 50–500 steps. So the “scalability under extremely long horizons i.e. steps>1000” remains only partially tested. Even though the approach might remain feasible, it is worth clarifying or at least discussing if any modifications are required for stable learning in extremely long tasks.\n\n- Imperfect Prior: The experiments rely on a Bayesian prior over LDBA transitions (Dirichlet), which is a “symmetric, optimistic” assumption. It’s certainly a valid design, but in truly unknown or “messy” tasks, one might question if this prior is overly optimistic or if it could lead to misdirected exploration. The authors do present ablations on the prior’s hyperparameter  𝛼. However, for certain tasks, an incorrect or imperfect prior might hamper performance or cause needless exploration. Additional tasks that illustrate the “prior mismatch” scenario might have been instructive.\n\n- One-Step vs. Multi-Step LDBA Transitions: The paper acknowledges that in a real environment, multiple steps in the MDP might be required to induce a single LDBA transition (like going from one subgoal zone to another). The environment suite is still largely structured so that each subgoal region is fairly discrete. A more continuous or “scattered” environment, with partial observability or less direct transitions, could challenge the assumption that states are easily reachable.\n\n- Testing with a different algorithm might provide additional evidence of DRL2’s algorithm-agnostic nature.\n\n- In the reach-avoid tasks, failing the avoidance criterion immediately transitions to a sink state, effectively giving the agent a strong negative outcome. This helps with exploration in that domain, but it is a domain-specific design. In more general tasks (especially outside of gridworlds), “failure” might not be so clearly signaled. The paper could discuss whether DRL2 might struggle in tasks where the environment does not forcibly terminate upon failure, or if no well-defined “sink” LDBA state is reachable (e.g., in purely liveness tasks without avoid constraints).\n\n- Many of the discrete tasks revolve around corridor or “room” setups that funnel the agent in a straightforward path. This is typical of LTL-based RL papers but can be seen as somewhat contrived. One might wonder how DRL2 performs in a more branching or maze-like environment—would the agent still effectively find the correct path given more branching choices and no single corridor?\n\n- Although the continuous tasks (Fetch, HalfCheetah, Doggo) have different shapes—manipulation vs. locomotion—they still focus on fairly similar formula types (reach-avoid, finite or repeated subgoals). The authors do not explore, for example, tasks with nested ‘until’ operators or other formula structures that might yield more complex or less direct exploration demands.\n\n- The paper explicitly notes that the 2D gridworld environments are fully deterministic. While this makes analysis simpler (especially for LTL), it doesn’t test how DRL2 handles stochastic transitions. In real applications, environment dynamics may contain significant randomness, which can alter exploration requirements (e.g., some states might be visited unpredictably). An additional set of stochastic gridworld tasks (random wind, slippery actions, etc.) could validate DRL2’s robustness to stochastic MDPs.\n\n\n- The authors used cumulative return under eventual discounting as their metric to measure the method performance. This metric is not uncommon in LTL-based RL research, however, researchers seeking a direct measure of “policy satisfaction probability” or “percentage of episodes meeting the entire LTL formula” may prefer a binary satisfaction rate or an explicit horizon-based measure.\n\n- Summing 𝛾𝑖 for each visit to an accepting state can help rank policies better (more visits to acceptance = higher return), it may not be as transparent as “the fraction of time the formula is ultimately satisfied.” Certain LTL formulas (like repeated “GF” type goals) do require multiple visits to acceptance, so counting repeated visits makes sense. But for simpler tasks where you only need to reach acceptance once or you need acceptance in a final region, the “count repeated visits” approach may artificially inflate the score. Moreover, this metric does not reflect whether the agent got “close” to acceptance but did not quite make it—non-accepting runs effectively get 0 aside from discount accumulations. It is informative to use a more granular measure, such as distance to acceptance or partial subtask completion. A more direct measure might be: “What fraction of episodes actually satisfy the LTL formula?”, or “What is the agent’s estimated probability of infinite repeated satisfaction?” Those would be more straightforwardly connected to logic satisfaction. By comparison, “eventual discounting” plus repeated visits may require additional interpretation. \n\n- Although the authors compare against a few strong baselines (LCER, count-based shaping), there exist other exploration techniques in RL that might be adapted to LTL settings—e.g., intrinsic curiosity modules, hash-based exploration, or optimistic/pessimistic MDP approaches. A concise discussion of how DRL2 complements or differs from these more general exploration heuristics would strengthen the paper.\n\n- Some mention of potential state space blow-up is given, but clarifying the computational cost when LDBAs become large (e.g., dozens or hundreds of states) could be more detailed.\n\n- Currently, no direct experiment in the paper shows “the difference between using the full product MDP vs. using only the MRP.” The authors mention it conceptually: once you collapse environment states (𝑠∈𝑆) into a single LDBA state, you lose the detail of which environment state led there. The MRP lumps all transitions from (s,b) purely into a single next-b′ distribution. A potential experimental design could look like: Compare an approach that tries to plan or explore purely in the MRP (which sees only the LDBA states) vs. the normal RL in the product MDP. Show that certain distinctions in the environment get “blurred” in the MRP, leading to suboptimal or uncertain actions in some states. The authors do not have such an experiment in the paper; they only note the theoretical possibility. It could be a good extension if the authors want to highlight the magnitude of that “loss of information.”", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "Yes", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "paper_topic_and_main_contributions": "", "excitement": null, "reproducibility": null, "ethical_concerns": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "summary_of_contributions": "This paper presents DRL2, a new method for directed exploration in Reinforcement Learning (RL) from Linear Temporal Logic (LTL) specifications. The core idea is to use the LTL formula’s Limit Deterministic Büchi Automaton (LDBA) as a Markov reward process (MRP). Then, by placing a Bayesian prior over LDBA transition probabilities, one can (i) produce a high-level value estimation over the automaton states, and (ii) convert these values into potential-based shaping rewards that guide exploration in the RL agent’s “product MDP.” Empirical results suggest that DRL2 can handle tasks that combine both sequential subgoals and avoidance constraints in more complex, high-dimensional domains than previous LTL-based RL works. The authors show that their approach yields significant improvements in exploration whenever the environment or task structure demands nontrivial trajectories to reach the automaton’s accepting states.\n\nRecommendation: Accept with Minor Revisions", "claims_and_evidence_yn": "Yes", "claims_explanation": "", "audience_yn": "Yes", "audience_explanation": "", "requested_changes": "- In the “Background” or “Product MDPs and Policy Optimization” section, introduce a Definition 2.5 that fully specifies the product MDP: M^×=(S^×,A^×,P^×,R^×,γ^×,μ_0^×).Make it explicit that 𝑅^×(𝑠,𝑏) is 1 if 𝑏∈𝐵^∗(accepting) and 0 otherwise (or clarify if it’s -1 outside acceptance).\n\n- Consider or at least discuss the case 𝑅^×(𝑠 ,𝑏)=−1 outside acceptance to see whether it expedites exploration. A brief experiment or mention of potential side effects (like “rushing” to acceptance) would clarify the trade-offs.\n\n- The paper states the MRP is a high-level approximation and might lose information about the environment. Add a small experiment or at least a more detailed discussion showing how ignoring environment states can lead to suboptimal policy updates in certain corner cases.\n\n- Section 3.2 covers the intuition of a symmetric Dirichlet prior. A short example or pseudocode could help illustrate exactly how the posterior is updated each time data arrives and how the authors sample the MRP transitions for value computation. Although the text references the Dirichlet formula, a quick demonstration (e.g., small LDBA with 2–3 states) would improve accessibility.\n\n- In the main exposition, the authors consistently use 𝑅^× and 𝛾^×  for the product MDP. However, a few paragraphs define the “eventual discounting scheme” with slightly different notational approaches (e.g., Γ_𝑖). To streamline reading, double-check that all definitions align clearly.\n\n- In Section 3 (or Implementation Details), add a short statement on why certain reward scaling coefficients (like 0.1 in tabular tasks, 10.0 in continuous tasks) work well and how they influence training stability or final performance.\n\n- The paper states that the approach can introduce “slight non-stationarity” in the reward shaping signal, since the Bayesian posterior is updating. It might help to quantify or at least discuss how severely this might affect off-policy vs. on-policy algorithms.\n\n- In the \"limitations\" of section 6, authors might also want to mention that:  \n          - Dependence on correct LDBA: DRL2 can be sensitive if the LDBA construction is large or suboptimal (this was mentioned in the Outlook, but it’s also a limitation).\n          - Potentially unrealistic prior: The Bayesian approach can be powerful, but might rely on a prior that could mislead exploration in some tasks if not set carefully.\n          - Fully or partially stochastic environments: The current experiments are mostly deterministic in the discrete case.\n\n- The paper includes “No Exploration” (no shaping) vs. “Count-based” vs. “LCER” vs. “DRL2.” But they do not show a “purely MRP-based RL” scenario (where you ignore environment states altogether), nor a “−1 outside acceptance” scenario. The discussion in Appendix F + G shows different ways of building or initializing the kernel (empirical, partially informed, etc.). They do highlight that prior knowledge about the LDBA structure is crucial—DRL2 intentionally encodes knowledge that “the automaton might transition to any next state with uniform probability at the start.” That is prior knowledge. Indeed, a “good” exploration algorithm typically tries to minimize reliance on hand-crafted priors. DRL2 does rely on the knowledge of which LDBA states are reachable from which other states, plus the hyperparameter 𝛼. The authors do some ablations (varying 𝛼), but one could argue for further experiments with weaker or partially incorrect priors. Hence, it would be interesting if the paper had a dedicated section showing “No MRP,” “Only MRP-based shaping with no environment details,” or “Using −1/0 as a reward scheme.” But that is not included.\n\n- The paper only compares DRL2 with LCER, a count-based baseline, and “no exploration” conditions. Other curiosity or optimism-driven approaches (e.g., intrinsic curiosity modules or random network distillation) might also be adapted to LTL. A short discussion on how DRL2 relates to these would be beneficial.\n\n- In appendix A, if there is a notion of “time t” at which Γ_t≈0, it may be helpful to mention or suggest how large t typically is to yield the same policy in both \\tilde M^×and M^×. Even a theoretical or empirical bound might be insightful for practitioners.\n\n\nTypos:\n- Section 3.2: we adopt an partially symmetric prior ---> an partially", "broader_impact_concerns": "NA", "additional_comments": "", "extra_scores": {}, "extra_text": {}}, {"review_id": "I0J41fuCmt", "reviewer": "Reviewer_V9PM", "summary": "", "questions": "", "limitations": "", "rating": null, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "The method is relatively simple and seems to perform well. I am glad to see some\nexperiments in continuous domains: the main downside of the method is that the\nrepresentation of the transition kernel seems to be essentially tabular, using an\nexplicit distribution on transitions between pairs of states. I'll also note that\nthe environments are still pretty simple as far as exploration is concerned.\nThey were, nevertheless, sufficient to demonstrate improvement, so this is fine.", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "Yes", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "paper_topic_and_main_contributions": "", "excitement": null, "reproducibility": null, "ethical_concerns": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "summary_of_contributions": "The title of this work is slightly misleading. The work primarily concerns how\nreinforcement learning techniques can be used to construct policies that fulfill\nobjectives defined using LTL in an unknown MDP. This is still an interesting\nproblem, though it is not really about exploration in reinforcement learning per\nse (note that otherwise a different selection of baselines and benchmarks would\nhave been necessary). In any case, the work shows how a reward signal can be\ngenerated for the LTL specification that, together with Bayesian updating in an\nepisodic setting, asymptotically corresponds to (bounds on) the probability of\nthe LTL objective being satisfied in the MDP. (There is an analysis of asymptotic\nconvergence, though it does not provide explicit bounds on the convergence rate.)\nIn a handful of simple benchmarks, the method is demonstrated to generally yield\nmuch faster convergence than e.g. counterfactual experience replay from prior\nwork by Voloshin et al.", "claims_and_evidence_yn": "Yes", "claims_explanation": "", "audience_yn": "Yes", "audience_explanation": "", "requested_changes": "I'd like to see the approach to learning continuous environments clarified -- I\ndon't see a discussion here (maybe I missed it) so I am assuming that the\nstates of continuous environment are simply discretized as a grid. (Hence, in\npart, my concern about scaling.) I would like to see this made explicit if so.\n\nOtherwise, a handful of things could strengthen the work, though they are not\ncritical: for one, an environment that requires more exploration than the U, such \nas a maze, would be an interesting demonstration of the ability of the method\nto actually drive exploration. For two, bounds on the convergence rate and\ntime complexity (beyond merely asymptotic convergence) would be helpful.\nI guess these would just be polynomial in the number of states, but it would be\ngood to show this if so.", "broader_impact_concerns": "I don't have any concerns here.", "additional_comments": "", "extra_scores": {}, "extra_text": {}}, {"review_id": "lPe2vJBPui", "reviewer": "Reviewer_GUGh", "summary": "", "questions": "", "limitations": "", "rating": null, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "Strengths:\n\n- The reward shaping method proposed is relevant and seems to be very performant \n- The evaluation is overall through and encloses many different settings\n\nWeaknesses:\n\n- The discussion, especially the limitations, is insufficient, i.e., too short, very limited information\n- The literature review should be improved, i.e., the distinction or novelty in contrast to other approaches is not clear, especially to goal-directed RL", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "Yes", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "paper_topic_and_main_contributions": "", "excitement": null, "reproducibility": null, "ethical_concerns": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "summary_of_contributions": "The paper introduces a novel reward-shaping approach based on LTL task specifications. The LTL specification is transformed in a Limit Deterministic Büchi Automaton that is combined with the environment MDP to a product MDP. Based on observed trajectories a value function can be computed that can be used to compute an \"intrinsic reward\" which is added to the sparse rewards from the product MDP.  The reward-shaping approach is evaluated in discrete and continuous spaces and compared to relevant baselines. The reward shaping leads to faster convergence and partially to enabling task solving.\n\nThe paper is well written. However, the abbreviations (e.g., RL, LTL, GridWorld) are not consistently used and some figures are not consistent with the template by not spanning the full column.", "claims_and_evidence_yn": "Yes", "claims_explanation": "", "audience_yn": "Yes", "audience_explanation": "", "requested_changes": "- The more common term for similar methods would be goal-conditioned instead of directed reinforcement learning. Directed can be viewed as strong guidance as present in action masking methods. Please engage with this literature [1,2] and the goal-conditioned RL literature [3-5] more and clarify the distinctions in the related work section (and introduction).\n- Related work:\n\na) As stated in the previous comments, some very related literature is not well enough discussed, which should be improved. Additionally, the related work section does not clarify the advantages or distinctions of your approach in contrast to existing work. Please add this information\n\nb) It is unclear what the criteria are for the extended literature review and most references are presented in the main paper anyway. So please merge this in the main content.\n\n- Discussion:\n\na) The limitations are not sufficiently discussed. Please answer the following questions: What interpretation limitations are present due to your experimental setup, i.e., what could be issues on other tasks? What if tasks are more stochastic than your current selection? How would more uncertainty, e.g., in the evaluation of atomic predicates, affect your approach? How does the potential mismatch of your prior distribution assumption with reality affect the approach? Where do you see the main weaknesses ofyour approach for future extensions or applications, e.g., what if parts of the task specification have to be always ensured (safety/avoid unsafe) and others are less relevant, how would you approach that, etc.? \n\nb) The message of your last sentence is not clear. Please rephrase.\n\nc) I would suggest you restructure the Discussion to a clear discussion section that mainly addresses limitations and gives ideas how they can be mitigated. After that, you can have a clear conclusion paragraph. Right now the information is a bit convoluted.\n\n- Doesn't the virtual sink state change the task notion for cyclic tasks? How does this affect the resulting policies?\n- \"DRL2 drive deep..\" -> You mainly show convergence rates evidence for that. Did you also check other metrics, e.g., how often irrelevant states are visited?\n- the count-based and no exploration baseline could be introduced in a bit more detail or with more clarity (1-2 sentences) in the main part of the paper. Right now the description is vague\n- the discrete environments seem to be overfitting for one specific initial state. Is this correct? Also, the sequential task seems to have complicated specifications that could be reduced to F(c). Why did you not place the colored fields somewhere in the grid?\n- Can you comment on your hyperparameter tuning? I would highlight the information that \\alpha is an additional hyperparameter for DRL2  in the main text and that you use the same hyperparameters for all approaches.\n- The first sentence in the second paragraph of 4.2. is unclear and potentially incorrect since the continuous results seem to be significantly noisier.\n\nMinor comments:\n- The background section is very well written.\n- You could make it a bit more obvious that R_{intr} is the reward shaping \n\nReferences:\n\n[1] Theile, Mirco, Lukas Dirnberger, Raphael Trumpp, Marco Caccamo, and Alberto L. Sangiovanni-Vincentelli. \"Action Mapping for Reinforcement Learning in Continuous Environments with Constraints.\" arXiv preprint arXiv:2412.04327 (2024).\n\n[2] Roland Stolz, Hanna Krasowski, Jakob Thumm, Michael Eichelbeck, Philipp Gassert, and Matthias Althoff. Excluding the Irrelevant: Focusing Reinforcement Learning through Continuous Action Masking. NeurIPS 2024 \n\n[3] Beyazit Yalcinkaya, Niklas Lauffer, Marcell Vazquez-Chanlatte, and Sanjit A. Seshia, Compositional Automata Embeddings for Goal-Conditioned Reinforcement Learning. NeurIPS, 2024\n\n[4] David Lindner, Matteo Turchetta, Sebastian Tschiatschek, Kamil Ciosek, Andreas Krause. Information Directed Reward Learning for Reinforcement Learning.  Part of Advances in Neural Information Processing Systems 34 (NeurIPS 2021) \n\n[5] Directed Exploration for Reinforcement Learning. Zhaohan Daniel Guo, Emma Brunskill. https://arxiv.org/abs/1906.07805", "broader_impact_concerns": "N/A", "additional_comments": "", "extra_scores": {}, "extra_text": {}}]

Author rebuttal:

Decision: Accept (poster)