DeepLTL: Learning to Efficiently Satisfy Complex LTL Specifications for Multi-Task RL
Authors: Mathias Jackermeier
Alessandro Abate
Venue: ICLR 2025 Oral (2025)
Keywords: reinforcement learning
linear temporal logic
ltl
generalization
Primary area: reinforcement learning

Abstract: Linear temporal logic (LTL) has recently been adopted as a powerful formalism for specifying complex, temporally extended tasks in multi-task reinforcement learning (RL). However, learning policies that efficiently satisfy arbitrary specifications not observed during training remains a challenging problem. Existing approaches suffer from several shortcomings: they are often only applicable to finite-horizon fragments of LTL, are restricted to suboptimal solutions, and do not adequately handle safety constraints. In this work, we propose a novel learning approach to address these concerns. Our method leverages the structure of Büchi automata, which explicitly represent the semantics of LTL specifications, to learn policies conditioned on sequences of truth assignments that lead to satisfying the desired formulae. Experiments in a variety of discrete and continuous domains demonstrate that our approach is able to zero-shot satisfy a wide range of finite- and infinite-horizon specifications, and outperforms existing methods in terms of both satisfaction probability and efficiency. Code available at: https://deep-ltl.github.io/

Published as a conference paper at ICLR 2025
DEEPLTL: LEARNING TO EFFICIENTLY SATISFY COMPLEX LTL SPECIFICATIONS FOR MULTI-TASK RL
Mathias Jackermeier, Alessandro Abate
Department of Computer Science, University of Oxford (mathias jackeejcceeeee rmeier, elessandro... abate @cs wx..accu.
ABSTRACT
Linear temporal logic (LTL) has recently been adopted as a powerful formalism for specifying complex, temporally extended tasks in multi-task reinforcement learning (RI.. However, learning policies that efficiently satisfy arbitrary specifications not observed during training remains a challenging problem. Existing approaches suffer from several shortcomings: they are often only applicable to fimitehhrizoon fragments of LTL,, restricted to suboptimal solutions, and do not adequately han- dle safety constraints. In this work, we propose a novel learning approach to address these concerns. Our method leverages the structure of Büchi automata, which ex- plicitly represent the semantics of LTL specifications, to learn policies conditioned sequences of truth assignments that lead to satisfying the desired formulae. Experiments in a variety of discrete and continuous domains demonstrate that our approach is able to zero-shot satisfy wide range of finite- and -ifiite-horizon specifications, and outperforms existing methods in terms of both satisfaction probability and efficiency. Code available at: https: dedp/eeeppltteee 1t1, gi thtb. io/
INTRODUCTION
One of the fundamental challenges in artificial intelligence (AI) create agents capable of following arbitrary instructions. While significant research efforts have been devoted to designing reinforcement learning (RL) agents that can complete tasks expressed in natural language (Oh et al., 2017; Goyal et al., 2019; Luketina et al., 2019), recent years have witnessed increased interest in formal languages to specify tasks in RI. (Andreas al., 2017: Camacho et al., 2019; Jothimurugan et al., 2021). Formal specification languages offer several desirable properties over natural language, such as well-defined semantics and compositionality, allowing for the specification of unambiguous, structured tasks (Vaezipoor et al., 2021; León et al., 2022). Recent works have furthermore shown that it is possible to automatically translate many natural language instructions to formal languages, providing interpretable yet precise representations of tasks (Pan et al., 2023; Liu al., 2023).
Linear temporal logic (LTL) (Pnueli, 1977) in particular has been adopted as a powerful formalism for instructing RI. agents (Hasanbeig et al., 2018; Araki et al., 2021; Voloshin et al., 2023). LTL is an appealing specification language that allows for the definition of tasks in terms of high-level features of the environment. These tasks can utilise complex compositional structure, are inherently temporally extended (i.e. non-Markovian), and naturally incorporate safety constraints.
While several approaches have been proposed learning policies capable of zero-shot executing arbitrary LTL specifications in a multi-rask RL setting (Kuo et al., 2020; Vaezipoor et al., 2021; Qiu al., 2023: Liu et al., 2024), they suffer from several limitations. First, most existing methods are limited to subsets of LTL and cannot handle difiite-horizon (i.c. w-regular) specifications, which form an important class of objectives including persistence (eventually, a desired state needs to be reached forever), recurrence (a set of states needs to be reached infinitely often), and response (whenever a particular event happens, a task needs to be completed) (Manna & Pnueli, 1990). Second, many current techniques are myopic, that is, they solve tasks by independently completing individual subtasks, which can lead to inefficient, globally suboptimal solutions (Vaezipoor et al., 2021). Finally, existing approaches often do not adequately handle safety constraints of specifications, especially when tasks can be completed in multiple ways with different safety implications. For an illustration of these limitations, see Figure 1.

---

Published as a conference paper at ICLR 2025
(a) w-regular tasks
(b) Optimality
(c) Safety
Figure I: Limitations of existing methods, illustrated via trajectories in the ZoneEnv environment. The initial agent position is denoted handle infinite-horizon tasks, such as G F blue A G green. (b) Given the formula (blue A ggreen), myopic approach produces suboptimal solution (orange line). We prefer the more efficient green trajectory. (c) Given the task (F green v F yellow) A G Gbbue, the agent should aim to reach the yellow region instead of the green region, since this is the safer option. Many existing approaches unable to perform this sort of planning.
orange diamond. (a) Most existing approaches cannot
In this paper, we develop novel approach to learning policies for zero-shot execution of LTL specifications that addresses these shortcomings. Our method exploits the structure Büchi automata to non-myopically reason about ways of completing (possibly infinite-horizon) specification, and to ensure that safety constraints are satisfied. Our main contributions are as follows:
we develop the first non-myopic approach to learning multi-task policies for zero-shot execution of LTL specifications that is applicable to Shinite-horizon tasks;
we propose novel representation of LTL formulae based reach-avoid sequences of truth assignments, which allows us to learn policies that intrinsically consider safety constraints;
we propose a novel neural network architecture that combines DeepSets and RNNs to condition the policy on the desired specification;
lastly, we empirically validate the effectiveness of our method on a range of environments and tasks, demonstrating that outperforms existing approaches in terms of satisfaction probability and efficiency.
2 BACKGROUND
Reinforcement learning. We model RL environments using the framework Markov decision processes (MDPs). An MDP is tuple M AS P, H4, 7), where S is the state space, A is the set actions, P: S x A + (SS) is the unknown transition kernel, μ E (SS) is the initial state is the reward function, and
distribution, r: S A S
[0, 1) is the discount factor.
We denote the probability of transitioning from state 8 to state s' after taking action a as P(s' a, A (memoryless) policy S > ((A) is map from states probability distributions Executing policy π in an MDP gives rise to a trajectory 7 (so, ag. To, . ..,,..). where 5o ~ μ. de T( 5t), 5 P St: ar), and r. r(sr, ar, 8t+1). The goal of RL is find policy x² that maximises the expected discounted return J(T) = Ersr IE Yrrz]. where we write indicate that the distribution over trajectories depends on the policy π. The value function of policy (*()) E,-= 1Et= 7²r, so x] is defined as the expected discounted return starting from state s and following policy æ thereafter.
actions.
Linear temporal logic. Linear temporal logic (LTL) (Pnueli, 1977) provides formalism to precisely specify properties of infinite trajectories. LTL formulae are defined over a set atomic propositions AP, which describe high-level features of the environment. The syntax of LTL formulae is recursively defined as
true a A =p Xip pplppt
where a E AP and &o and & are themselves LTL formulae. A and - are the Boolean operators conjunction and negation, which allow for the definition of all standard logical connectives. The temporal operators and intuitively mean "next" and "until". We define the two temporal modalities F ("eventually"" and G ("always") as F true U & and G -F -
2

---

Published as a conference paper at ICLR 2025
The semantics of LTL align with the intuitive meanings of its operators. For example, in the Enn environment depicted in Figure 1, the atomic propositions AP correspond to coloured regions. We can naturally express many desirable tasks as LTL specifications, such reaching blue region (F blue), avoiding blue until yellow region is reached (-blue U yellow), reaching and remaining in green region (F G green), oscillating between blue and green regions while avoiding yellow (G F green A Flue A G -yellow). The latter two examples represent infinite-horizon specifications, which describe behaviour over an infinite time horizon.
Formally, the satisfaction semantics of LTL are defined via a recursive satisfaction relation w } on infinite sequences w of truth assignments' over AP (i.e. w-words over 2 2AP) (see Appendix for details). To ground LTL specifications in an MDP, we assume access to a labelling function I: S + 2AP, which returns the atomic propositions that are true in a given state. trajectory mapped to sequence of assignments via its trace Tr(r)= L(1))
and we write т | yp as shorthand for Tr(T)) }= s. The satisfaction probability of an L.TL formula yp under policy x is then defined as Pr( } pp) Ersr 1[T = -l|.
Büchi automata. A more practical way of reasoning about the semantics of L.T. formulae is via Bücci automata (Büchi, 1966), which are specialised automata that can be constructed to keep track of the progress towards satisfying specification. In particular, in this work we focus on limit-deterministic Bütch automata (LDBAs) (Sickert et al., 2016), which are particularly amenable to be employed with MDPs. An LDBA is a tuple B = (Q. qo. Σ, 8, F, F)E,, where Q is finite set of states, 9o E Q is the initial state, E= 2 is a finite alphabet, 6: Q x (EUE) - Q is the transition function, and F is the set of accepting states. Additionally, Q is composed of two disjoint subsets Q = QN te 2n such that F S Ωn and a( E 2n for all E 2n and a E Σ. The set & is an indexed set of e-transitions (a.k.a jump transitions), which transition from 2N to QD without consuming any input, and there are no other transitions from ON to QD.
run of B on the w-word w is an infinite sequence of states in Q respecting the transition function. An infinite word w accepted by B if there exists run r of B on that visits
b
b
an accepting state infinitely often. For every LTL formula s. we can construct an LDBA B that accepts exactly the words satisfying yp (Sickert et al., 2016).
start
Eas
Example 1. Figure 2 depicts an LDBA for the formula (a) Fbb. The automaton starts in state go and transitions to the accepting state qı upon observing the proposition b. Once has reached F1, it stays there indefinitely. Alternatively, it can transition to the accepting state 42 without consuming any input via the g-transition. Once in g2, the automaton accepts exactly the words where a is true at every step.
Figure 2: LDBA for the formula (FGa) V F.b.
PROBLEM SETTING
Our high-level goal is to find specifcaaion-connitionee policy π by that maximises the probability of satisfying arbitrary LTL formulae yp. Formally, we introduce an arbitrary distribution & over LTL specifications yp, and aim to compute the optimal policy
arg max
IE Go T~
[1[T + r]]
We now introduce the necessary formalism to find solutions to Equation 1 via reinforcement learning.
Definition (Product MDP), The product MDP M of an MDP M and an LDBA B, synchronises the execution of M and B. Formally, M has the state space S = Sx Q, action space A AxE, initial state distribution μ (f,(s) ().g) q) = p(s) 1[q = qo]. and transition function
P(s' () if E AA = 5 I(s)), if Eg A = a) A& =
PP ((s',
otherwise.
An assignment a subset of AP. Propositions p a are assigned true, whereas p assigned false.
3

---

Published as a conference paper at ICLR 2025
The product MDP M extends the state space of M in order keep track of the current state of the LDBA. This allows us to consider only memoryless policies that map tuples (s, q) of MDP and LDBA states to actions, since the LDBA takes care of adding the memory necessary to satisfy (Baier & Katoen, 2008). Quite importantly, note that in practice we never build the product MDP explicitly, but instead simply update the current LDBA state q with the propositions T(()) observed at each time step. Also note that the action space in M is extended with & to allow the policy follow s-transitions in B without acting in the MDP. Trajectories in M are sequences .),
T ((so, go), 4u ($1, 91) ......), and we denote as by the projection of T onto the LDBA states qu Q1...... We can restate the satisfaction probability of formula yp in M as
Pr(T - up) E [1 [in nFF + 0]]
where (Ty) denotes the set of states that occur infinitely often in Ty--
An optimal policy can be found via goal-conditioned reinforcement learning in the product MDP as follows: given some probability distribution & over LTL formulae, sample o É and trajectories T ~ xlp,, assigning a positive reward of whenever the policy visits an accepting state in the s, and 0 otherwise. To ensure that the reward-maximissng policy TRL indeed maximises Equation I, one can employ eventual discounting (Voloshin et al., 2023) and only discount visits accepting states in the automaton and not the steps between those visits (for further discussion, see Appendix B.1). With this, we obtain the following bound on the performance of Tkz.
LDBA corresponding
Theorem (Corollary of Voloshin et al. (2023), Theorem 4.2). For any 7 E (0, 1) we have
sup E [Pr(T F p)] - E gou
[Pr(TRI F x) S 2 log( supp sup On. gog
Emp-g 14 E Q FI, V4 xp] is the expected number of visits to accepting states for trajectories that do not satisfy specification.
where Oz =
Proof. The proof follows from (Voloshin et al., 2023, Theorem 4.2) by repeated application of the linearity of expectation and triangle inequality. A detailed proof is given Appendix B.2.
However, while eventual discounting provides desirable theoretical guarantees, it does not take into account any notion of efficiency of formula satisfaction, which an important practical concern. Consider for example the simple formula Fa. Eventual discounting assigns the same return to all policies that eventually visit s with a E L(s). regardless of the number of steps required to materialise In practice, we often prefer policies that more efficient (require fewer steps make progress towards satisfaction), even if their overall satisfaction probability might be slightly reduced. A natural way to formalise this tradeoff is as follows:
Problem (Efficient LTL satisfaction). Given an unknown MDP M, a distribution over LTL formulae g, and LDBAs B,p for each y supp(E) (the support &), find the optimal policy
n²' arg max
I P
Σ 1'1 FBy)
(2)
Here, we discount all time steps, such that more efficient policies receive higher returns. While solutions to Problem are not guaranteed to be probability-optimall (as per Equation 1), they will generally still achieve a high probability of formula satisfaction, while also taking efficiency into ac- count. We consider Problem for the rest of this paper, since we believe efficiency to be an important practical concern, but note that our approach is equally applicable to the eventual discounting setting (see Appendix B.3). There is an interesting connection to discounted LTL (Almagor et al., 2014 4; Alur et al., 2023) (see Appendix C for details), but we leave a full investigation thereof for future work.
METHOD
Solving Problem I requires us to train policy conditioned on the current MDP state and the current state q of an LDBA constructed from given target specification yp Our key insight is that we can extract useful representation of q directly from the structure of the LDBA. by reasoning about the possible ways of satisfying the given formula from the current LDBA state This representation is then used to condition the policy, and guide the agent towards satisfying given specification.
4

---

Published as a conference paper at ICLR 2025
Training
Testing
Figure 3: Overview of our approach. (Left) During training, we train a general sequence-conditione policy with reach-avoid sequences a. (Right) At test time, we construct an LDBA from the target specification s.. We then select the optimal reach-avoic sequence o* for the current LDBA state according to the value function (*(s, o), and produce an action from the policy conditioned on a².
4.1 REPRESENTING LTL SPECIHICATIONS AS SEQUENCES
Computing accepting cycles. An optimal policy for Problem must continuously visit accepting states in By-- Since By is finite, this means that the agent has to reach an accepting cycle in the LDBA. Intuitively, the possible ways of reaching accepting cycles are an informative representation of the current LDBA state g, as they capture how to satisfy the given task. We compute all possible ways of reaching an accepting cycle using an algorithm based on depth-fite first search (DFS) that explores all possible paths from g to an accepting state 9 E F, and then back to state already contained in the path (see Appendix E for details). Let P, denote the resulting set of paths from q to accepting cycles.
Remark. In the case that corresponds to task that can be completed in finite time (e.g. Fa), the accepting cycle in B, is trivial and consists of only a single looping state (see e.g. q1 in Figure 2). We note that our algorithm compute accepting cycles is similar to previous work reward shaping (Shah et al., 2024); however, we use the accepting cycles for an altogether different purpose.
From paths to sequences. A path p Pa an infinite sequence of states (4ı, 22. in the LDBA. Let AT {a 5(g., a) 96+1) denote the set of assignments a E 2AP that progress the LDBA from state qi to q++1. We furthermore define the set of negative assignments A {a a Att A ö(g;,0 a) + 4: that lead from qi different state in the LDBA (excluding self-loops). In order to satisfy the LTL specification via the policy has to sequentially visit MDP states s, such that L(st.) A for some tú while avoiding assignments in A, We refer to the sequence
o ((AT AT), (A5. 45)....)
as the reach-avoid sequence corresponding p. and denote as So {op E Pa} the set of all reach-avoid sequences for q.
Example 2. The first two steps of = (({{a)), {(b, ()))),(((i)))) (e)). .).... require the agent to achieve while avoiding states with both b and d, and subsequently achieve
4.2 OVERVIEW OF THE APPROACH
See Figure 3 for overview of our method. Representing the current LDBA state & set of reach-avoid sequences allows us to condition the policy on possible ways of achieving the given specification. On high level, our approach works follows: in the training stage, learn general cocuuuccc-coniitionn policy ): S Ç + A(A) together with its value function V" S x - R to satisfy arbitrary reach-avoid sequences E Ç over AP, following the standard framework of noal-conditioned RI. (Liu et al., 2022). Note that we do not assume access to a distribution & over formulae, since we are interested in satisfying arbitrary specifications. At test time, we are now given a target specification oo and construct its corresponding LDBA. We keep track of the current LDBA state q, and select the optimal reach-avole sequence follow in order to satisfy yp according to the value function of π, i.e.
= arg max V (7((8,0 a). eEC,
We then execute actions o() until the next LDBA state is reached.
For now, assume that there e-transitions p. We revisit e-transitions in Section 4.5.
5

---

Published as a conference paper at ICLR 2025
DeepSets
ANN
a= = ((4 (1), (22, A2)....)
(RΛzlles; BAz (a:1ee77...
Co
Figure 4: Illustration of the sequence module. The positive and negative assignments in the truncated reach-avoid sequence a are encoded using the DeepSets architecture, which produces embeddings A These are then concatenated and passed through RNN, which yields the final sequence representa- tion Co.
The rest-time execution of our approach can be equivalently thought of as executing policy स in the product MDP MY, where 7(x, 7) = x (8, o²). That is, मे exploits и to reach an accepting cycle in the LDBA of the target specification, and thus approximates Problem Next, describe the model architecture of the sequence-conditiones policy, and give a detailed description of the training procedure and test-time execution.
4.3 MODEL ARCHITECTURE
We parameterise the sequence-conditioned policy и using a modular neural network architecture. This consists of an observation module, which processes observations from the environment, a sequence module, which encodes the reach-avoid sequence, and actor module, which takes input the features produced by the previous two modules and outputs a distribution over actions.
The observation module is implemented as either a fully-connected (for generic state features) or convolutional neural network (for image-like observations). The actor module is another fully connected neural network that outputs the mean and standard deviation of Gaussian distribution (for continuous action spaces) or the parameters of categorical distribution (in the discrete setting). Finally, the sequence module consists of a permutation-innariaa neural network that encodes sets of assignments, and a recurrent neural network (RNN) that maps the resulting sequence to a final representation. We discuss these components further detail below and provide an illustration of the sequence module in Figure 4.
Representing sets of assignments. The first step of the sequence module consists in encoding the sets of assignments in reach-avoid sequence. We employ the DeepSets architecture (Zaheer et al., 2017) to obtain an encoding e of set of assignments A. That is, we have
Σ p(a) AEE
e =
where s(a) is learned embedding function, and p is a learned non-linear transformation. Note that the resulting encoding е permutation comuutttion-imvaiinn,, i.e. it does not depend on the order in which the elements in A are processed, and Equation 4 is thus well-defined function on sets.
Representing reach-avoid sequences. Once we have obtained encodings the sets A and A for each element in the reach-avoid sequence a,, we concatenate these embeddings and pass them through an RNN to yield the final representation the sequence. Since a is an infinite sequence, we approximate it with finite prefix by repeating its looping part k times, such that the truncated sequence visits an accepting state exactly & times. We apply the RNN backwards, that is, from the end of the truncated sequence to the beginning, since earlier elements in are more important for the immediate actions of the policy. The particular model of RNN we employ is a gated recurrent unit (GRU) (Cho al., 2014).
4.4 TRAINING PROCEDURE
We train the policy π and the value function V using the general framework of goal-conditioned RL (Liu al., 2022). That is, we generate random reach-avoid sequence the beginning of each training episode and reward the agent for successfully completing it. In particular, given training sequence ((47, 47), ....... (A
A,),, we keep track of the task satisfaction progress via an
index [n] (where initially 1). We say the agent satisfies set of assignments A time step if [(x)) A. Whenever the agent satisfies A,t. increment i by one. If +

---

Published as a conference paper at ICLR 2025
give the agent reward of and terminate the episode. If the agent any point satisfies A,, also terminate the episode and give it a negative reward of -1. Otherwise, the agent receives zero reward. By maximising the expected discounted return, the policy learns efficiently satisfy arbitrary reach-avoid sequences. In our experiments, we use preximal policy optimisation (PPO) (Schulman al., 2017) to optimise the policy, but our approach can be combined with any RL algorithm.
Curriculum learning. To improve the training of in practice, we employ simple form of curriculum learning (Narvekar et al., 2020) in order to gradually expose the policy to more challenging tasks. A curriculum consists of multiple stages that correspond to training sequences of increasing length and complexity. For example, the first stage generally consists only of simple reach-task of the form ((f (((()))) }.0)) 4)) for p E AP, while later stages involve longer sequences with avoidance conditions. Once the policy achieves satisfactory performance on the current tasks, we move on to the next stage. For details on the exact curricula we use in our experiments, see Appendix F.4.
4.5 TEST TIME POLICY EXECUTION
At test time, we execute the trained sequence-conditoon policy to complete arbitrary task y. As described Section 4.2, we keep track of the current LDBÁ state in B,, and use the learned value function V to select the optimal reach-avoid sequence o² follow from q in order to satisfy (Equation 3). Note that it follows from the reward of our training procedure that
(=(s,o)
E TNOT
Σ ~11i=
80 =
i.e the value function is lower bound of the discounted probability of reaching an accepting state k times via (where & is the number of loops in the truncated sequence). As k oc, the sequence a* that maximises V thus maximises a lower bound on Problem for the trained policy т. Once o* has been selected, we execute actions a T [t. until the next LDBA state reached.
Strict negative assignments. Recall that negative assignment in reach-avoid sequence op is any assignment that leads to an LDBA state other than the desired next state in p. In practice, we find that trying avoid all other states in the LDBA can be too restrictive for the policy. We therefore only regard as negative those assignments that lead to a significant reduction in expected performance. In particular, given threshold X, we define the set of strict negative assignments for state qi E p as the assignments that lead to a state q' where
(s max
E'E
We then set A to be the set of strict negative assignments for q. Reducing À leads to a policy that more closely follows the selected path p, whereas increasing À gives the policy more flexibility to deviate from the chosen path.
Handling s-transitions. We now discuss how to handle e-transitions in the LDBA. As described in Section 2, whenever the LDBA is in state g with e-transition to o', the policy can choose to either stay or transition to of without acting in the MDP. the sequence a* chosen at g starts with an e-transition (i.e. A = {s)), we extend the action space of æ to include the action If .A is discrete, we simply add an additional dimension to the action space. In the continuous case, we learn the probability p of taking the e-action and model (-|ss, a²) as mixed continuous/discrete probability distribution (see e.g. (Shynk, 2012, Ch. 3.6)). Whenever the policy executes the E-action, we update the current LDBA state the next state in the selected path. In practice, we additionally only allow e-actions if ((s) & Ag since in that case taking the e-transition would immediately lead to failure.
4.6 DISCUSSION
We argue that our approach has several advantages over existing methods. Since we operate on accepting cycles of Büchi automata, our method is applicable to fifnite-horizon (i.e. w-regular) tasks, contrary to most existing approaches. Our method is the first approach that is also non-myopic, as it is able reason about the entire structure of specification via temporally extended reach-avoid
7

---

Published as a conference paper at ICLR 2025
0.6
0.6
Discounted return
0.4
0.3
0.3
0.3
DeepLTL GCRL-LTL
DeepLTL
0.2
DeepLIL
0.2
GCRL-LTL
0.1
LTL2Action
0.1
LTLZAction
0.1
LTLZAction
0.2
0.6
1.0
0.6
1.0
1.4 1e7
0.2
0.6
1.0
1.4
Number steps
1e7
Number steps
Number of steps
1e7
(a) LetterWorld
(b) ZoneEnv
(c) FlatWorld
Figure 5: Evaluation curves on reach/avoid specifications. Each datapoint collected by averaging the discounted return of the policy across 50 episodes with randomly sampled tasks, and shaded areas indicate 90% confidence intervals over 5 different random seeds.
sequences. This reasoning naturally considers safety constraints, which are represented through negative assignments and inform the policy about which propositions to avoid. Crucially, these safety constraints considered during planning, i.e. when selecting the optimal sequence to execute, rather than only during execution. For a detailed comparison of our approach to related work, see Section 6.
EXPERIMENTS
We evaluate our approach, called DeepLTL, in a variety of environments and on a range of LTL specifications of varying difficulty. We aim to answer the following questions: (1) Is DeepLTT. able to learn policies that can zero-shot satisfy complex LTL specifications? (2) How does our method compare to relevant baselines in terms of both satisfaction probability and efficiency? (3) Can our approach successfully handle infinite-horizon specifications?
5.1 EXPERIMENTAL SETUP
Environments. Our experiments involve different domains with varying state and action spaces. This includes the LetterWorld environment (Vaezipoor et al., 2021), a 7 x 7 discrete grid world in which letters corresponding atomic propositions occupy randomly sampled positions in the grid, We also consider the high-dimensional ZoneEnv environment from Vaezipoor et al. (2021), in which robotic agent with a continuous action space has navigate between different randomly placed coloured regions, which correspond to the atomic propositions. Finally, we evaluate our approach on continuous Fla World environment (Voloshin et al., 2023), in which multiple propositions can hold true at the same time. We provide further details and visualisations in Appendix F.I.
LTL specifications. We consider a range tasks of varying complexity, Reach/avoid specifications randomly sampled from task space that encompasses both sequential reachability objectives of the form F (p1 A (F A (F pa)) and reach-avoid tasks -p1 U (P2 A (-ps Pt)), where the p; randomly sampled atomic propositions. Complex specifications are given by more complicated, environment-specfft. LTL formulae, such as the specification ((a V b V c d) = (e (F (f A Fg)))) U (h A Fi) in LetterWorld. We also separately investigate infimite-horizon tasks such as GFa A GFb and F G.. The specifications we consider cover a wide range of LTL objectives, including reachability, safety, recurrence, persistence, and combinations thereof. Details on the exact specifications we use in each environment are given in Appendix F.2.
Baselines. We compare DeepLTL to two state-of-the-ard approaches for learning general LTL- satisfying policies. LTT12Action (Vaezipoor et al., 2021) encodes the syntax tree of target formula via a graph neural network (GNN) and uses a procedure known as I.TI. progression to progress through the specification based the observed propositions. The second baseline, GCRL-LTL (Qiu et al., 2023), instead learns propsitionncondiiiin using a weighted graph search on the Büchi automaton of a target specification.
policies and combines them compositionally
Evaluation protocol. In line with previous work, the methods are trained for 15M interaction steps each environment with PPO (Schulman et al., 2017). Details about hyperparameters and
8

---

Published as a conference paper at ICLR 2025
Table Evaluation results trained policies on complex finite-horizon specifications. We report the success rate (SR) and average number of steps to satisfy the task (n)) Results are averaged over 5 seeds and 500 episodes per seed. "+" indicates the standard deviation over seeds.
LTI22Actoon
GCRL-IITL
DeepI.TI
SR (1)
(L)
SR (f)
J (L)
SR (*)
(L)
LetterWorld
SP1
0.75
29.48
0.94-0.05
15.29_0.70
+.000
9.66++0.5
iP2
2.79
19.04
0.94=00.0
=.
0.98 20.00
2.26
IPs
0.41 2.41
40.31 12.68
1.00
20.72
1.00
12.23
A44
0.72+0.17
28. 28.83+44.47
0.82=0.07
14.60_1.68
0.97 +0.00
12.13+0.58
0.44
31.84
1.00
25.63
1.00
9.48 10.78
96 0.60
424. #14.9
0.85 0.85=0.0z
452.19
0.92
303.38-219...
ZoneEnv
4P7
1.14
416.78.166.8
0.85 0.0 0.00
451.18
0.91 10.03
299.95
100.447
AP8
0.67
414,48.268
0.89
449.70.
0.96
259.75
SPo 2..92
331.55
0.87
303.13
0.90 +0.03
203.36
14.90
Pi0 0.66
293.22
0.85
290.73
0.91 +0.02
187.13
P111
0.931
123.89 107.30
0.89 .01
137,42108.80
0.98
106.21
FlatWorid
PP1
1.000
83.32.01157
0.82
78.21
1.00 10.00
79.69.102.0
4P13
0.63
94.43 139.30
0.00
0,00
1.00 20.00
52.822203.00
PP14
0.71 0.71 40.40
96. 16.164428.4
0.73
74.60
0.98
71.76
P15
1.002
32.37 101.63 13.
0.73
41.30
1..61
43.87 43.87.101.45
P10
0,56+0.35
48 48.85
0.64
17.76
1.00
37.04_206.28
neural network architectures can be found in Appendix F.3. We report the performance in terms of discounted return over the number of environment interactions (following Equation 2) on randomly sampled reach/avoid tasks, and provide tabular results detailing the success rate (SR) and average number of steps until completion (n) of trained policies on complex tasks. All results are averaged across 5 different random seeds. Furthermore, we provide visualisations of trajectories of trained policies for various specifications in the Env and FlarWorld environments Appendix G.9.
5.2 RESULTS
Finite-horizon tasks. Figure 5 shows the discounted return achieved on reach/avoid tasks across environment interactions. DeepLTL clearly outperforms the baselines, both in terms of sample efficiency and final performance. The results in Table further demonstrate that our method can efficiently zero-shot satisfy complex specifications (see Appendix F.2 for details on the tasks), achieving higher success rates (SR) than existing approaches, while requiring significantly fewer steps (μ). These results highlight the performance benefits of our representation based on reach-avoid sequences over existing encoding schemes, and show that our approach learns much more efficient policies than the myopic baseline GCRL-LTL. The higher success rates of our method furthermore indicate that it handles safety constraints better than the baselines.
Infinite-horizz tasks. Figure 6 shows example trajectories of DeepLTL on infinite-horizon tasks in the ZoneEm environment. In Figure 6e furthermore compare the performance of our approach on recurrence, i.e. GF, tasks (see Appendix F.2 for details) to GCRL-LTL, the only previous approach that can handle hnrizot specifications. We report the average number of visits to accepting states per episode, which corresponds to the number of completed cycles of target propositions (e.g. the number of times both blue and green have been visited for the specification G blue A G green). Additional results on F G tasks can be found in Appendix G.I. Our evaluation confirms that DeepLTL can successfully handle w-regular tasks, and significantly outperforms the only relevant baseline.
Further experimental results. We provide further experimental results in Appendix G. These include more results on tasks with safety requirements (G.2), an investigation of the generalisation capabilities of DeepLTL to longer sequences (G.3), two ablation studies on the impact of curriclum learning (G.4) and our model architecture (G.5), investigations on the performance impact of the number of atomic propositions (G.6) and specification complexity (G.7), and a comparison RAD- embeddings (Yalcinkaya et al., 2024), a recent automata-come conditiiooniiioonedd RL method (G.8). Finally, we show trajectories of trained policies in the ZoneEny and Flat World environments in Appendix G.9.

---

Published as a conference paper at ICLR 2025
GCRL-IIT..
DeepI.TI.
6.74
17.84
LetterWorld
4/2
1.49
3.05
ZoneEnv
1/a
3. 3.14110.18
4.16.1061
6/4
1.31 20:05
1.71
FlatWorld
6/s
1.208
12.12
6/
4.64
6.98+1.00
(a) G F blue/ G F green
(b) F G blue
Figure 6: Results on infinite-horizon tasks. (a), (b) Example trajectories for infinite-horizon speci- fications. (c) Performance various recurrence tasks. We report the average number of visits to
accepting states over 500 episodes (i.e. completed cycles), with standard deviations over 5 seeds.
RELATED WORK
RL with tasks expressed in LTL has received significant attention in the last few years (Sadigh et al., 2014; De Giacomo et al., 2018; Camacho et al., 2019; Kazemi et al., 2022; Li et al., 2024). Our approach builds previous works that use LDBAs augment the state space of the MDP (Hasanbeig et al., 2018: Hahn et al., 2019; 2020; Bozkurt et al., 2020; Voloshin et al., 2022; Hasanbeig et al., 2023; Bagatella et al., 2024; Shah al., 2024). However, these methods are limited to finding policies for single, fixed specification. In contrast, our approach is realised in a multi-task setting and learns a policy that can zero-shot generalise arbitrary specifications at test time.
Among the works that consider multiple, previously unseen specifications, many approaches decom- pose a given task into subtasks, which are then individually completed (Araki et al., 2021; León et al., 2021; 2022; Liu et al., 2024). However, as noted by Vaezipoor et al. (2021) this results in myopic behaviour and hence potentially suboptimal solutions. contrast, our approach takes the entire specification into account by reasoning over temporally extended reach-avoid sequences. Kuo et al. (2020) instead propose to compose RNNs in a way that mirrors formula structure, which however requires learning non-stationary policy. This is addressed by LTL.2Action (Vaezipoor et al., 2021), which encodes the syntax tree of a target specification using a GNN and uses LTL progression (Bacchus & Kabanza, 2000) make the problem Markovian. A similar approach is proposed by Yalcinkaya et al. (2024), who use a GNN to encode tasks represented by deterministic finite automata. We instead extract reach-avoid sequences from Büchi automata, which explicitly lists the possible ways of satisfying given specification. Furthermore, due to its reliance on LTL progression, LTL2Action is restricted to the finite-horizon fragment of LTL, whereas our approach is able to handle infinite-horizz tasks.
The only previous method we are aware of that can deal with infinite-horizon specifications GCRL- LTL (Qiu et al., 2023). However, similar to other approaches, GCRL-LTL relies on composing policies for sub-tasks and therefore produces suboptimal behaviour. Furthermore, the approach only considers safety constraints during task execution and not during high-level planning. Recently, Xu & Fekri (2024) proposed future dependent options for satisfying arbitrary LTL tasks, which are option policies that depend future goals. Their method is only applicable not support conjunction nor infinitehhrrizn specifications, and does not consider safety constraints during planning. See Appendix D for an extended discussion of related work.
fragment of LTL that does
CONCLUSION
We have introduced DeepLTL, novel approach to the problem of learning policies that zero-shot execute arbitrary LTL specifications. Our method represents a given specification as a set of reach- avoid sequences of truth assignments, and exploits general sequeece-condittioned policy execute arbitrary LTL instructions at test time. In contrast to existing techniques, our method can handle fiinite-horizon specifications, is non-myopic, and naturally considers safety constraints. Through extensive experiments, we have demonstrated the effectiveness of our approach in practice. This work contributes the field of LTL-conditioned RL, which has the potential to pave the way towards general Al systems capable of executing arbitrary, well-defined tasks.
10

---

Published as a conference paper at ICLR 2025
ACKNOWLEDGEMENTS
We are grateful for the valuable feedback from the anonymous reviewers. This work was supported by the UKRI AI Hub (EP/Y028872/1) and the ARIA TAI project SAINT. MJ is funded by the EPSRC Centre for Doctoral Training Autonomous Intelligent Machines and Systems (EPIS024050/1).
REFERENCES
Shaull Almagor, Udi Boker, and Orna Kupferman. Discounting in LTL. In Tools and Algorithms for the Construction and Analysis of Systems, pp. 424-439, 2014, ISBN 978-3-642-5486--8 doi: 10.1007/978- (-1----644---6666
Rajeev Alur, Osbert Bastani, Kishor Jothimurugan, Mateo Perez, Fabio Somenzi, and Ashutosh Trivedi. Policy Synthesis and Reinforcement Learning for Discounted LTL. In Computer Aided Verification, pp. 415 435, 2023. ISBN 978-3-831-37706-8 doi: 10. 10.11077978-330011-11
Jacob Andreas, Dan Klein, and Sergey Levine. Modular Multitask Reinforcement Learning with Policy Sketches. In Proceedings of the 34th International Conference on Machine Learning, pp. 166-175, July 2017.
Brandon Araki, Xiao Li, Kiran Vodrahalli, Jonathan Decastro, Micah Fry, and Daniela Rus. The Logical Options Framework. In Proceedings of the 38th International Conference Machine Learning, pp. 307-317, July 2021.
Fahiem Bacchus and Froduald Kabanza. Using temporal logics to express search control knowledge for plamning. Artificial Intelligence, 116(1):123-19)) 2000. ISSN 0004-3702. doi: 10.1016/
80004-37722/9900007555
Marco Bagatella, Andreas Krause, and Georg Martius. Directed Exploration Reinforcement Learning from Linear Temporal Logic. In Seventeenth European Workshop Reinforcement Learning, October 2024.
Christel Baier and loost-Piete Katoen. Principles of Model Checking. MIT Press, 2008. ISBN 1i2-0-222-02699--1
Alper Kamil Bozkurt, Yu Wang, Michael M. Zavlanos. and Miroslav Pajic. Control Synthesis from Linear Temporal Logic Specifications using Model-Free Reinforcement Learning In 2020 IEEE International Conference Robotics and Automation (ICRA), pp. 10355, May 2020. doi: 10.1 N0.1109/ICAA0094 2.9.C...000440022...... 207...9999.....99996
Alper Kamil Bozkurt, Yu Wang, Michael M. 7avlanos, and Miroslav Pajic. Learning Optimal Strategies for Temporal Tasks in Stochastic Games. IEEE Transactions on Automatic Control, 69 (11):7387-7402, November 2024. ISSN 1558-2523, doi: 10. 10.11099TAA.2222333999444
Tomá' Brázdil, Krishnendu Chatterjee, Martin Chmelik, Vojtëch Forejt, Jan Kietínský, Marta Kwiatkowska, David Parker, and Mateusz Ujma. Verification of Markov Decision Processes Using Learning Algorithms. In Automated Technology for Verification and Analysis, pp. 98-114, 2014. ISBN 978-3-319-11936-5 doi: 10.1007/978-3-3 3-319-11993-99 8.
Büchi. Symposium on Decision Problems: On Decision Method Restricted Sec- ond Order Arithmetic. In Studies in Logic and the Foundations of Mathematics, volume 44 of Logic, Methodology and Philosophy of Science, pp. 1-11. Elsevier, January 1966. doi: 10. (0016//0009-23700070000
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, 6(4):7973-7980. October 2021. ISSN 2377-3766. doi:
10.1109/RRA.222.3111155...
Alberto Camacho, Rodrigo Toro Iearte, Toryn Q. Klassen, Richard Anthony Valenzano, and Sheila A. Mcllraith. LTL and beyond: Formal languages for reward function specification in reinforce- ment learning. In Proceedings of the twenty-Eight International Joint Conference on Artificial Intelligence, IJCAI 2019, pp. 6065 2019. doi: 10.24963/UCAA1.2119/88
11

---

Published as a conference paper at ICLR 2025
Kyunghyun Cho, Bart van Merrienboer, Dzmitry Bahdanau, and Yoshua Bengio. On the Properties of Neural Machine Translation:
Approaches. In Proceedings of SSST-8, Eighth Workshop Syntax, Semantics and Structure in Statistical Translation, pp. 103-111. Association for Computational Linguistics, 2014, doi: 10.31 15/v1/W14-4011
Joëlle Cohen-Chesnot. On the expressive power of temporal logic for infinite words. Theoretical Computer Science, 8312):01-312,, June 1991. ISSN 0304-3975. doi: 10.1016/0304-397599) 90281-6.
Giuseppe De Giacomo and Moshe Vardi. Linear temporal logic and linear dynamic logic on finite traces. In Proceedings the Twenty-Third International Joint Conference on Artificial Intelligence, IJCAI 13, pp. 860, August 2013, ISBN 978-1-57735-633-2.
Giuseppe De Giacomo, Luca Tocchi, Marco Favorito, and Fabio Patrizi. Reinforcement learning for LTL goals. arXiv, 2018.
Giuseppe De Giacomo, Luca locchi, Marco Favorito, and Fabio Patrizi. Foundations for Restraining Bolts: Reinforcement Learning with L.T.f/LLDII Restraiing Specifications. Proceedings of the International Conference on Automated Planning and Scheduling, 29:128-1368 136, 2019. ISSN
2334-0843, doi: 10.1609/capss. 10.1609/raps..291..5555 v29i1.359.
Jie Fu and Ufuk Topcu. Probably Approximately Correct MDP Learning and Control With Temporal Logic Constraints. Robotics: Science and Systems X, July 2014. ISBN 978-0-9923747-0-9, doi:
2..15667/RSS.221.....2
Prasoon Goyal, Scott Nickum, and Raymond Mooney. Using natural language for reward shaping in reinforcement learning. In Procedingss of the 28th Intermational Joint Conference on Artificial Intelligence, IJCAI' 19, pp. 2385-238 2391, 2019. ISBN 978-0-99924111 11-4-1.
Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, and Dominik Objectives in Model-Free Reinforcement Learning. In Tools and Algorithms for the Construction and Analysis of Systems, pp. 395 412, 2019. ISBN 978-3-030- 07462-0-777422.77
Wojtczak.
17462-0. doi:
Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, and Dominik Wojtczak. Faithful and Effective Reward Schemes for Model-Free Reinforcement Learning of Omega-Reguus Regular Objectives. In Automated Technology for Verification and Analysis, pp. 108 124, 2020. ISBN 978-3-030-59152-6 doi:
3-030-59152-664
Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, and Dominik Wojtezak. Mungojerrie: Linear-Tine Time Objectives in Model-Free Reinforcement Learning. Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, pp. 527-545, 2023. ISBN 978-3-031-30823-9) doi: (1007/97--3-0313006 27.
Hosein Hasanbeig, Daniel Kroening, and Alessandro Abate. Certified reinforcement learning with logic guidance. Artificial Intelligence, 322:103949, 2023. ISSN 0004-3702. doi: 10.1016/j 2023.103949.
Mohammadhosein Hasanbeig, Alessandro Abate, and Daniel Kroening. Logically-Constrainee Reinforcement Learning. arXiv, 2018. doi: 1a..5500/rxxiv.181..0555
Jiaming Ji. Jiayi Zhou, Borong Zhang, Juntao Dai, Xuehai Pan, Ruiyang Sun, Weidong Huang, Yiran Geng, Mickel Liu, and Yaodong Yang. OmniSafe: An Infrastructure for Accelerating Safe Reinforcement Learning Research. In arxiv. arXiv, 2023. doi: 10448500arXx..22055.0000
Kishor Jothimurugan, Rajeev Alur, and Osbert Bastani. A Composable Specification Language for Reinforcement Learning Tasks. In Advances in Neural Information Processing Systems, volume 32, 2019.
Kishor Jothimurugan, Suguman Bansal, Osbert Bastani, and Rajeev Alur. Compositional Rein- forcement Learning from Logical Specifications. In Advances in Neural Information Processing Systems, volume 34, pp. 10026-10039, 2021.
12

---

Published as a conference paper at ICLR 2025
Milad Kazemi and Sadegh Soudjani. Formal Policy Synthesis for Continuous-Stan Systems via Reinforcement Learning. In Integrated Formal Methods: 16th International Conference, pp. 3-21, November 2020. ISBN 01----030-34460-- doi:
030-63461-2 1.
Milad Kazemi, Mateo Perez, Fabio Somenzi, Sadegh Soudjani, Ashutosh Trivedi, and Alvaro Specifications to Average Objectives for Model-Free Reinforcement Learning. In Proceedings of the 21st International Conference Autonomous Agents and Multiagent Systems, AAMAS '22, pp. 732-741, May 2022. ISBN 978-1-4503-9213-4
Velasquez. Translating
Diederik P. Kingma and Jimmy Ba. Adam: method for stochastic optimization. In Yoshua Bengio and Yann LeCun (eds.), 3rd International Conference Learning Representations, 2015. doi: 10. 10.48550/arXiv. 101550//rXiv.11226966 1412.690.
Yen-Ling Kuo, Boris Katz, and Andrei Barbu, Encoding formulas as deep networks: Reinforcement learning for zero-shot execution of LTL formulas. In 2020 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), pp. 5604-5610, October 2020. doi: 1094444330 2020.9341325.
Xuan-Bach Le, Dominik Wagner, Leon Witzman, Alexander Rabinovich, and Luke Ong. Rein- forcement Learning with LTT. and w-regular Objectives via Optimality-Preservii Translation to Average Rewards. In The eighth Annual Conference on Neural Information Processing Systems, November 2024.
Borja G. León, Murray Shanahan, and Francesco Belardinelli. Systematic Generalisation through Task Temporal Logic and Deep Reinforcement Learning. In arXiv. arXiv, 2021. doi: 10.48550/ arXiv.2006.08767.
Borja G. León, Murray Shanahan, and Francesco Belardinelli. Nutshell, the Human Asked for This: Latent Goals for Following Temporal Specifications. In International Conference Learning Reprexentations, 2022.
Andrew C. Li, Zizhao Chen, Toryn Q. Klassen, Pashootan Vaezipoor, Rodrigo Toro Icarte, and Sheila A. Mcllraith. Reward Machines for Deep RL in Noisy and Uncertain Environments. In 38th Conference on Neural Information Processing Systems, 2024.
Jason Xinyu Liu, Ziyi Yang, Ifrah Idrees, Sam Liang, Benjamin Schornstein, Stefanic Tellex, and Ankit Shah. Grounding Complex Natural Language Commands for Temporal Tasks in Unseen Environments. In Proceedings of The 7th Conference on Robot Learning, pp. 1084-1110, 2023.
Jason Xinyu Liu, Ankit Shah, Eric Rosen, Mingxi Jía, George Konidaris, and Stefanie Tellex. Skill Transfer for Temporal Task Specification. In 2024 IEEE International Conference on Robotics and Automation (ICRA). pp. 2535-2541 2024. doi: 10. N0.110///CRA55747.200444 106144.02222241111433313
Minghuan Liu, Menghui Zhu, and Weinan Zhang. Goal-Conditioned Reinforcement Learning: Problems and Solutions. In Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, pp. 5502-55111 5511, July 2022. ISBN 978-1-956792-00-3. doi: 10.24963/jccai. 2022/770.
Jelena Luketina, Nantas Nardelli, Gregory Farquhar, Jakob N. Foerster, Jacob Andreas, Edward Grefenstette, Shimon Whiteson, and Tim Rocktäschel. A survey of reinforcement learning informed by natural language. In Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, pp. 6309-6311 2019. doi: 10.24963/ICCA.2219/885
Zohar Manna and Amir Pnueli. A hierarchy of temporal properties. In Proceedings of the Ninth Annual ACM Symposium on Principles of Distributed Computing, PODC '90, pp. 377-410, 1990. ISBN 978-0-89791-40442 doi: 10.1145/93385.93442.
Sanmit Narvekar, Bei Peng. Matteo Leonetti, Jivko Sinapov, Matthew E. Taylor, and Peter Stone. Curriculum Learning for Reinforcement Learning Domains: A Framework and Survey. Journal of Machine Learning Research. 21(181): 2020. ISSN 1533-7928.
Junhyuk Oh, Satinder Singh, Honglak Lee, and Pushmeet Kohli. Zero-Shot Task Generalization with Multi Task Deep Reinforcement Learning. In Proceedings of the 34th International Conference on Machine Learning, pp. 2661-2670 July 2017.
13

---

Published as a conference paper at ICLR 2025
Jiayi Pan, Glen Chou, and Dmitry Berenson. Data-Efficient Learning of Natural Language to Linear Temporal Logic Translators for Robot Task Specification. In 2023 IEEE International Conference Robotics and Automation (ICRA), pp. 11554-11561, 2023. doi: 10.1109/CCRA4889122222
10161 125.
Amir Pnueli. The temporal logic of programs. In 18th Anmual Symposium on Foundations of Computer Science (SFCS 1977), pp. 46-57, October 1977. doi: 10.1 1,.119//FCS..97..322
Wenjie Qiu, Wensen Mao, and He Zhu. Instructing Goal-Conditioned Reinforcement Learning Agents with Temporal Logic Objectives. In Thirty-Seventhh Conference Neural Information Processing Systems, November 2023.
Dorsa Sadigh, Eric S. Kim, Samuel Coogan, S. Shankar Sastry, and Sanjit A. Seshia. A learning based approach to control synthesis of Markov decision processes for linear temporal logic specifications. In 53rd IEEE Conference Decision and Control, pp. 1091-1096, December 2014. doi: 10. 1..119//CC2220140035557
John Schulman, Filip Wolski, Prafulla Dhariwal, Alec Radford, and Oleg Klimov. Proximal Policy Optimization Algorithms. In arXiv, August 2017. doi: 10.48550/arXiv.10000 170..000..7770477.....
Ameesh Shah, Cameron Voloshin, Chenxi Yang, Abhinav Verma, Swarat Chaudhuri, and Sanjit A. Seshia. LTL-Coostrained Policy Optimization with Cycle Experience Replay. In arXiv, 2024. doi:
10.485500/rXxi..444..555
Daqian Shao and Marta Kwiatkowska. Sample efficient model-free reinforcement learning from LTL specifications with optimality guarantees. In Proceedings of the Thirtt-Second International Joint Conference on Artificial Intelligence, pp. 4180-4189, 2023, doi: 10. N0.24963/UCAA..2234455
John J. Shynk. Probability, Random Variables, and Random Processes: Theory and Signal Processing Applications. John Wiley & Sons, 2012. ISBN 978- 778-1-118-39995-4
Salomon Sickert, Javier Esparza, Stefan Jaax, and Jan Kietínsky. cimittDetermmnistic Büchi Automata for Linear Temporal Logic. In Computer Aided Verification, Lecture Notes in Computer Science, pp. 312-332, 2016. ISBN 978-3-319 778-3-319-41540-6 doi:
Rodrigo Toro Icarte, Toryn Q. Klassen, Richard Valenzano, and Sheila A. Mcllraith. Teaching Multiple Tasks an RI. Agent using L.T... In Proceedings of the 17th International Conference on Autonomous Agents and MultiAgent Systems, AAMAS 18, pp. 452-461 July 2018a.
Rodrigo Toro learte, Toryn Q. Klassen, Richard Valenzano, and Sheila A. Mcllraith. Using Reward Machines for High-Level Task Specification and Decomposition in Reinforcement Learning. In Proceedings of the 35th International Conference on Machine Learning, pp. 2107-2116, July 2018b.
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, 73:173 738 January 2022. ISSN 1076-9757. doi: 10. 1..111//jair... 1.12440.
Pashootan Vaczipoor, Andrew C. Li, Rodrigo Toro Icarte, and Sheila Meilraith. LTL2Action: Generalizing LTL Instructions for Multi-Tase RL. In Proceedings of the 38th International Conference on Machine Learning, pp. 10497-10508, July 2021.
Ashish Vaswani, Noam Shazeer, Niki Parmar, J Jakob Uszkoreit, Llion Jones, Aidan N Gomez, ukasz Kaiser, and Illia Polosukhin. Attention is All you Need. In Advances in Neural Information Processing Systems, volume 30, 2017.
Cameron Voloshin, Hoang Le, Swarat Chaudhuri, and Yisong Yue. Policy Optimization with Linear Temporal Logic Constraints. Advances in Neural Information Processing Systems, 35: 17690-17702, December 2022.
Cameron Voloshin, Abhinav Verma, and Yisong Yue. Eventual Discounting Temporal Logic Coun- terfactual Experience Replay. In Proceedings of the 40th International Conference on Machine Learning, pp. 35137-35150, July 2023.
14

---

Published as a conference paper at ICLR 2025
Christopher J C H Watkins. Learning from Delayed Rewards. PhD thesis, University of Cambridge, 1989.
Christopher J. C. H. Watkins and Peter Dayan. Q-learning, Machine Learning, 8(3):279-292, May 1992. ISSN 1573-0565. doi: 10.1007/BF00099668.
Duo Xu and Faramarz Fekri. Generalization of temporal logic tasks via future dependent options. Machine Learning, August 2024. ISSN 1573-0565. doi: 1..10077/109944-0440666144
Beyazit Yalcinkaya, Niklas Lauffer, Marcell Vazquez-Chanlatte, and Sanjit Seshia. Automata Conditioned Reinforcement Learning with Experience Replay. In NeurIPS 2023 Workshop on Goal Condiiondd Reinforcement Learning. 2023.
Beyazit Yalcinkaya, Niklas Lauffer, Marcell Vazquez-Chanlatee and Sanjit A. Seshia. Compositional Reinforcement Learning. In The Thirty-eighth Annual
Automata Embeddings for Conference on Neural Information Processing Systems, 2024.
Manzil Zaheer, Satwik Kottur, Siamak Ravanbakhsh, Barnabas Poezos, Russ R Salakhutdinov, and Alexander J Smola. Deep Sets. In Advances in Neural Information Processing Systems, volume 30, 2017.
15

---

Published as a conference paper at ICLR 2025
A LTL SATISFACTION SEMANTICS
The satisfaction semantics LTL. are defined in terms of infinite sequences of truth assignments 24P (a.k.a. w-words over 2AP). The satisfaction relation -= yp specifies that w-word satisfies the specification s. it recursively defined as follows (Baier & Katoen, 2008):
true W a F P A
E wo iff yp and J
W F mp
w + 4
- X p
iff w | |
W = p U e
if 2 s.t. wij wlj...] - s and v0 <i<j. wlt...] =
As noted in the main paper, we can equivalently define the satisfaction semantics via (limit- deterministic) Büchi automata. Formally, for any LTL specification of we can construct Büchi automaton that accepts exactly the set Words({p) = fw E (2^P)) p
B LEARNING PROBABILITY-OPTIMAL POLICIES
B. EVENTUAL DISCOUNTING
The technique of eventual discounting (Voloshin al., 2023) can used find optimal policy for a given (single) LTL specification y in terms of satisfaction probability via reinforcement learning. It optimises the following objective:
RL = max
E Erale FF,1
r, r0
Σ [ax E FByl. k=
where & counts how often accepting states have been visited up to time step t.
To why eventual discounting is necessary, consider the product MDP M depicted in Figure 7, and adapted from Voloshin et al. (2023). The policy starts state so and can choose either action action b. Action always leads to infinite cycle containing accepting state, and is thus optimal. Action b on the other hand also leads to an infinite cycle with probability 0.99, but may lead to sink state with probability 0.01.
Let Ta be the (deterministic) policy that chooses a and Ty be the policy that chooses b. Without eventual discounting, have:
1
0.99
((T.)
and ((m)) 1-7'
1 --
and thus J(T)) > (raa) for all y E (0.01, 1). Hence, maximising (standard) expected discounted return produces suboptimal policy in terms of satisfaction probability.
start
80
0.99
0.01
#1
S3
T
82
Figure 7: Example product MDP.
16

---

Published as a conference paper at ICLR 2025
Eventual discounting addresses this problem by only discounting visits to accepting states, and not the steps in between. In the previous example, this means that ((Ta) > ((T)), in line with the satisfaction probability. See Voloshin al. (2023) for formal derivation of bound on the performance of the return-optimal policy under eventual discounting. We next extend this result to the setting of distribution over L.TL. specifications yp
B.2 PROOF OF THEOREM 1
Given probability distribution & over LTL specifications s, employ the standard formulation of goal-conditioned RL to obtain the multi-task eventual discounting objective:
TRL
arg max
E
Σ
Tala: E FF.
Tr T==11 7t, a
E1le 1um E FB,... k=
(5)
JONE, Trust Ap
Theorem provides bound on the performance of the policy TRL- Our proof closely follows the structure of the proof of (Voloshin et al., 2023, Theorem 4.2). We begin with the following Lemma:
Lemma 1. For any T, 7 E (0, 1), and supp(E), we have
1(1 - >) Pr(x F x) S log )
where Oz E -l lg T4 FB. H /f= sp] is the expected number of visits to accepting states for trajectories that do not satisfy a specification.
Proof. The proof follows exactly along the lines of the proof of (Voloshin et al., 2023, Lemma 4.1) with our modified definition of Og, which includes the expectation over yo.
We are now ready to prove the main result:
Theorem 1. For any E 1) we have
sup E [Pr(T } p)] g
[Pr(TRL F v)) < 2 log ) angg
E
sup Or.
Proof. Let (mr) be sequence of policies such that
Pr( + sup
Pr(m + 4)]
you
By the linearity of expectation, we have
E [Pr(T, --]= E [Pr(TRL F v) g-_g
p~
E Pr((T; - 4) 1 -Pr(Tă. F v) wn5
We add and subtract the terms (1 VR and (1 - - and apply the triangle inequality obtain
< E Pr(me = vー
+ E Pr( } Fx) - - (1-7)VV V
(6)
+
E
(1
V² - -(1 (1-
The last term is negative since
(1 ))=))
= (1 - 7) E yuu m
(1 >) - V
0
(by the definition of )T)
17

---

Published as a conference paper at ICLR 2025
Note that for any random variable X, again by the triangle inequality,
[[X]| Σ P = 2)
S Σ Pr(X = z) E|
and we can hence continue from Equation 6 by applying Lemma 1 as follows (where we utilise the fact the expectations respect inequalities):
- E (6)
log 10 + +0rim)
10 7
2 log( Ox E
2 log sup O
which, together with taking the limit as - oc, concludes the proof.
B.3 DEEPLTL WITH EVENTUAL DISCOUNTING
DeepLTL can be readily extended with eventual discounting for settings which satisfaction probability is the primary concern, and efficiency is less important. In this case, we want to use our approach to approximate a solution to Equation
To do only need to assume access to the distribution over LTL formulae. During training, we sample specifications ~ E and train the eqquence-conditions policy using all reach-avoid extend each step of a reach-avoid sequence include an additional Boolean flag that specifies whether the corresponding LDBA transition leads to an accepting state. These flags given as input to the policy network, and are used to compute the eventual discounting objective. The rest of our approach remains unchanged. We leave an experimental investigation of this scheme for future work.
sequences extracted from 3 Crucially,
C DISCOUNTED LTL
Discounted LTL (Almagor et al., 2014) extends LTL with discounting semantics. This allows one to specify not only that a system should satisfy given specification (as in classical LTL), but also how well should so. The main idea is to replace the "until" operator with a discounted version that assigns quantitative satisfaction value in [0, to system trace. Intuitively, the longer the system takes to satisfy a requirement, the smaller the assigned satisfaction value.
The problem of finding optimal policy with respect discounted LTL formula in an unknown MDP has been thoroughly investigated by Alur et al. (2023), and is closely related to our problem of efficient LTL satisfaction (Problem 1). Indeed, for simple formulac such as & F,, (where F,, denotes the 7-discounted version of the F operator) exactly to maximising the quantitative satisfaction value of s. We leave fuller investigation of the relationship between discounting rewards from accepting LDBA states and the semantics of discounted LTL, well an integration of our approach with the reward scheme proposed by Alur et al. (2023), for future work.
casy to see that Equation corresponds
D EXTENDED RELATED WORK
The field of RL with LTL specifications has attracted significant attention in the last few years. Here we provide more detailed overview of work in this domain and discuss how it relates to our approach.
RL with a single LTL specification. Early works on RL with LTL specifications relied on esti- mating model of the underlying MDP, and then solving this model for probability probabilit--mxximisin policy (Fu Topcu, 2014; Brázdil et al., 2014; Sadigh et al., 2014). A model-fres approach based on Q-learning (Watkins, 1989; Watkins & Dayan, 1992) was introduced by Hasanbeig et al. (2018), who
18

---

Published as a conference paper at ICLR 2025
proposed to use LDBAs keep track of formula satisfaction. Subsequent works extend this approach, providing stronger convergence guarantees (Hahn et al., 2019; Bozkurt et al., 2020; Hahn et al., 2023; Voloshin et al., 2023), improved sample efficiency (Hahn et al., 2020; Kazemi & Soudjani, 2020; Cai et al., 2021; Shao & Kwiatkowska, 2023; Shah et al., 2024; Bagatella et al., 2024), or guarantees in adversarial environments (Bozkurt al., 2024). Alternative methods reduce the problem to an RL objective with limit-average rewards instead of the standard discounted setting (Kazemi et al., 2022; Le et al., 2024). variety of works also consider LTL, (De Giacomo & Vardi, 2013) or similar specification languages over finite traces, such as reward machines (Toro Icarte et al., 2018b; De Giacomo et al., 2018: 2019; Jothimurugan et al., 2019; 2021; Toro Iearte al., 2022).
These approaches all consider only a single, fixed LTL specification, i.c. they learn policy that maximises the probability of satisfying a given formula y. contrast, our approach is realised in multi-task RL setting: we focus on learning a task-conditional policy that can zero-shot execute arbitrary LTL specifications at test time.
Generalising to multiple tasks. Toro Icarte al. (2018a) were among the first to consider the problem of training a policy to complete multiple different tasks expressed in LTL. They propose a hierarchical algorithm based on Q-Jearning, which composes policies trained on subtasks. However, their approach is not able to generalise to novel formulae at test time, since these might consist of subtasks that the agent has not seen during training. Kuo et al. (2020) instead propose leverage condiconnd RL with a compositional RNN architecture that consists of one RNN for every element in the syntax tree of given LTL formula. While this method is shown to be able generalise to tasks outside of the training distribution, it requires learning a non-stationary policy, which is known to be challenging (Vaezipoor et al., 2021).
León et al. (2021) introduce different method for tasks expressed in sub-fragment of LTL,. They first employ a reasoning module to extract propositions that make progress towards solving the given task. These propositions are then achieved by a trained goal-conditioned policy. Similarly, Liu et al. (2024) propose a transfer algorithm that first trains a number of options on a set of training instructions, and then composes them at test time to achieve novel tasks. However, Vaezipoor et al. (2021) these approaches are inherently myopic: they do not take future propositions into account when executing the next subtask, and hence can produce suboptimal solutions. Instead, Vaezipoor et al. (2021) propose to directly encode the syntax tree of a given L.TL formula using a GNN and predict actions based on the learned representations. To deal with the non-Markovian nature of LTL, they employ LTL progression (Bacchus & Kabanza, 2000). A more direct modification to the work of León et al. (2021) is proposed by Xu & Fekri (2024), who train dependent options for every proposition. These option policies are conditioned not only on the proposition to be achieved next, but also on the remaining propositions that need to be satisfied in the future. Qiu et al. (2023) introduce the first approach that can handle w-regular specifications. Their technique is based on training goal-conditioned policies x(-1s,)) p) to achieve arbitrary propositions p E AP in the environment. At test time, they employ planning procedure to select sequence of propositions to satisfy and finally execute the according low-level policies.
noted by
Our approach differs in variety of ways from these previous methods: we leverage the structure of Büchi automata to find possible ways of satisfying a given specification. By operating on Büchi automata, our method can naturally handle w-regular specifications, which only GCRL-LTL is also capable of. However, in comparison to GCRL-LTI. our method is non-myopic, since it incorporates the temporally extended structure of tasks via sequences of reach-avoid assignments. Additionally, compared to other methods that employ a high-level planning procedure (Qiu et al., 2023; Xu & Fekri, 2024) our approach considers safety requirements when selecting the optimal reach-avoid sequence. yielding plans that are more likely to be able to be executed without safety violations by the policy.
Automata-conditiones RL. A recent line of work related to LTL objectives is automata- conditioned RL (Yalcinkaya et al., 2023; 2024). Instead of using LTL to specify tasks, this line of research directly employs (compositions of) deterministic finite automata (DFAs). Yalcinkaya et al. (2024) explore this setting in multi-tasi RL context, and propose to train conlicondi policy conditioned on learned embeddings of DFAs. They also introduce the class of avodd derived (RAD) DFAs, which they use for pre-training the automata embeddings.
19

---

Published as a conference paper at ICLR 2025
Compared to approach, ioooomtaa-ondiiionne RL is strictly less expressive, since every DFA can trivially be represented as an LDBA (including objectives not expressible by LTL (Cohen- Chesnot, 1991)). but the converse is not true. In particular, DFAs camnot capture infinite-horizon tasks. Additionally, in contrast to RAD-embeddings (Yalcinkaya et al., 2024), we do not compute an embedding for the entire automaton, but instead extract satisfying reach-avoid sequences and select the optimal one according to the learned value function. This separates high-level reasoning (how satisfy the specification) from low-level reasoning (how act in the MDP) and allows the goal-conditioned policy to focus on achieving one particular sequence of propositions. We experimentally compare our approach RAD-embeddings in Appendix G.8.
E COMPUTING ACCEPTING CYCLES
The algorithm compute paths accepting cycles listed in Algorithm 1. The algorithm is based on depth-first search and keeps track of the currently visited path in order to extract all possible paths accepting cycles.
Algorithm 1 Computing paths to accepting cycles
Require:
An LDBA B = (2, 40, E, F, F, and current state
1: procedure DFS(q, p. i) i in the index of the last seen accepting state, -1 otherwise
2:
P+
if q E then
4:
i t- lpl
5:
end if
6:
for all E 2AP do
7:
p' + (p.g]
8:
g' a(
9:
o' E p then
10:
if index of q' in p then
11:
P= PUPPR (r')
12:
end if
13:
else
P PU DFS(G.....
15:
end
end for
17:
return P
end procedure
19:
if i 0f 4 E F else 4- -1
20: return DFS(g, []. i)
F EXPERIMENTAL DETAILS
F.I ENVIRONMENTS
Letter World. The LetterWorld environment has been introduced by Vaezipoor et al. (2021). it 7 x grid world that contains 12 randomly placed letters corresponding atomic propositions. Each letter appears twice, i.e. 24 out of the 49 squares are occupied, and there are thus multiple ways of solving any given task. The agent observes the full grid from an egocentric view. At each step, the agent can move up, right, down, or left. If it moves out of bounds, the agent is immediately placed on the opposite end of the grid. See Figure 8a for an illustration of the LetterWorld environment.
We adapt the ZoneEny environment introduced by Vaezipoor et al. (2021). The environ- ment a walled plane with 8 circular regions ("zones")) that have four different colours and form the atomic propositions. Our implementation is based the Safety Gymnasium suite (Ji et al., 2023) and uses the Point robot. which has a continuous action space for acceleration and steering. The environment features high-dimensional state space based lidar information about the zones, and
ZoneEnv.
20

---

Published as a conference paper at ICLR 2025
h
h
a
b
b
(a) LetterWorld
(b) ZoneEnv
(c) FlatWorld
Figure 8: Visualisations of environments.
data from other sensors. Both the zone and robot positions are randomly sampled the beginning of each episode. If the agent any point touches wall, it receives penalty and the episode is immediately terminated. A visualisation the ZoneEmy environment provided in Figure 8b.
FlatWorld. The FlatWorld environment (Voloshin et al., 2023; Shah al., 2024) consists of twoddimensional continuous world (S = [ with discrete action space. Atomic propositions are given by various coloured regions. Importantly, these regions overlap in various places, which means that multiple propositions can hold true at the same time. The initial agent position is sampled randomly from the space in which no propositions are true. each time step, the agent can move in one of the 8 compass directions. If it leaves the boundary of the world, the agent receives penalty and the episode terminated prematurely. Figure Se shows visualisation the FlatWorld environment.
F.2 TESTING SPECIFICATIONS
Tables and 3 list the finite and infinite-horizon specifications used in our evaluation, respectively.
F.3 HYPERPARAMETERS
Neural network architectures. Our choice of neural network architectures is similar to previous work (Vaezipoor et al., 2021). For DeepLTL and L.T.2Action, we employ a fully connected actor network with [64, 64, 64] units and ReLU as the activation function. The critic has network structure [64, 64] and uses Tanh activations in LetterWorld and ZoneEnv, and ReLU activations in Flar World. The actor is composed with a softmax layer in discrete action spaces, and outputs mean and standard deviation of Gaussian distribution in continuous action spaces. GCRL-LTL uses somewhat larger actor and critic networks with structure [512, 1024, 256] and ReLU activations the ZoneEny environment.
The observation module is environment-specife. For the ZoneEnv and FlarWorld environments, consists of simple fully connected network with [128, 64] units and Tanh activations, or [16, 16] units and ReLU activations, respectively. GCRL-LTL instead uses a simple projection of the input dimensionality 100 in ZoneEnv. For LetterWorld, the observation module is CNN with 16, 32, and 64 channels in three hidden layers, a kernel size of 2 x 2, stride of 1, no padding, and ReLU activations.
Finally, the sequence module consists of learned embeddings 6 of dimensionality 32 in LetterWorld, and 16 in ZoneEnv and FlarWorld. The non-linear transformation p fully connected network with [32, 32] units in Letter and [32, 16] units in ZoneEm and FlarWorld. We use ReLU activations throughout for the sequence module. For the baselines, we use the hyperparameters reported in the respective papers (Vaezipoor al., 2021; Qiu et al., 2023).
The hyperparameters for PPO (Schulman et al., 2017) are listed in Table We use the Adam optimiser (Kingma & Ba, 2015) for all methods and environments.
PPO hyperparameters.
Additional hyperparameters. LTL2Action requires an LTL task sampler to sample a random training specification at the beginning of each episode. We follow Vaezipoor et al. (2021) and
21

---

Published as a conference paper at ICLR 2025
Table 2: Complex
specifications used in our evaluation.
LetterWorks
4P2
(-f (dAFb)
4P
((lVvV)))FF) F(CAFd) FICA "a U (bA (d (d
PP4
4P
(avbbvvvd) ((e F(EA
U (hA
4P6
F (green A (-blue U yellow)) A F magenta
ZZonEEn
4P7
F blue A (-blue U (green A yellow))
498
(blue V green) A F yellow F magenta
4Po
- (magenta V yellow) U (blue green)
4P10
green U ((blue V magenta) A (-green U yellow))
4P11
((green V blue) (-yellow U magenta) ) U yellow
1212
F ((red A magenta) F ((blue A green) A Fyellow))
FlatWorld
4P1
F (orange (-red U magenta))
1114
( (-red (green A blue A aqua))
(orange (F (red magenta)))
PP15
(( ((-yellow A -orange) U (green A blue)) A (-green U magenta)
PP16
(blue + F magenta) V (yellow V ((green blue) A F Foangee)
Table 3: Infinite-horizon specifications used in our evaluation.
GF(eA(-aUF))
LetterWorld
1/2
GFAAGFDAGFCAGFAAGG-EN
4/3
G A G green
ZoneEny
G blue A G green A Felloow A G G-magenta
4/5
GF (blue green) G (red magenta)
FlatWorld
V/
G F (aqua ^ blue) A F red A Feelow A G -gren
22

---

Published as a conference paper at ICLR 2025
Table 4: Hyperparameters for PPO. Dashes (-) indicate that the hyperparameter value is the same across all three methods.
LTL2Action
GCRL-LTL
DeepLTL
Number processes Steps per process per update Epochs
128
8
Batch size
256
LetterWorld
Discount factor
0.94
GAE-À
0.95
Entropy coefficient
0.01
Value loss coefficient
0.5
Max gradient norm
0.5
Clipping (c)
0.2
Adam learning rate
0.0003
Adam epsilon
le-08
Number processes
16
Steps per process per update Epochs
4096
3125
4096
10
Batch size
2048
1000
2048
ZonesEnv
Discount factor
0.998
GAE-À
0.95
Entropy coefficient
0.003
Value loss coefficient
0.5
Max gradient norm
0.5
Clipping (e)
0.2
Adam learning rate
0,0003
Adam epsilon
Ic-08
Number of processes
16
Steps per process per update
4096
Epochs
10
Batch size
2048
Forl
Discount factor
0.98
GAE-À
0.95
Entropy coefficient
0.003
Value loss coefficient
0.5
Max gradient norm
0.5
Clipping (c)
0.2
Adam learning rate
0.0003
Adam epsilon
le-08
23

---

Published as a conference paper at ICLR 2025
Table Evaluation results of trained policies on persistence tasks. We report the average number of time steps for which the policy successfully remains in the target region after executing the e-action. Results are averaged over seeds and 500 episodes per seed. "4" indicates the standard deviation over seeds.
GCRL-LTL
DeepLTL
G blue G blue A (yellow A F green)
265.53
562.81 136.28
178. 62.88
336.81 _069.43
F G magenta A G -yellow
406.52
587.98
123.63
G (ggree V yellow) F Filue) A (green magenta)
380.49
570.37 138.98
sample specifications from the space of reach/avoid tasks. We also experimented with sampling more complex specifications, but found this detrimental to performance. For GCRL-LTL, we set the value threshold a to 0.9 the ZoneEnv environment, and 0.92 in LetterWorld and FlarWorld. The threshold À for strict negative assignments in DeepLTLL is set to 0.4 across experiments.
F.4 TRAINING CURRICULA
We design training curricula in order to gradually expose the policy to more challenging tasks. The general structure of the curricula is the same across environments: we start with simple and short reach-avoid sequences, and move to more complicated sequences once the policy achieves satisfactory performance.
LetlerWorld. In the LetterWorld environment, the first curriculum stage consists of reach-avoid tasks of depth with single propositions, e.g. (faa), {(b)))) Once the policy achieves an average satisfaction rate of 95% on these sequences, we move to the next curriculum stage, which the depth is still I, and |A] < |A < 2. The next stage consists of the same tasks with length of 2. The final curriculum stage consists of length-3 sequences with | < 2, |AT 3.
ZoneEnv. For ZoneEnv, the first stages consist of first only reach-sequences of length up (i.e. A, = 0) and then reach-avoid sequences of length up to 2. We then increase the cardinality of the positive and negative assignments, while introducing sequences aligned with reach-stay tasks, e.g.
((fggreen)) 2.4P (green)).....
FlatWorld. In FlarWorld, first sample mixture of reach- and reach-avoid sequences of depth up to 2. Once the policy achieves a success rate of 80%, we increase the cardinality of the positive and negative assignments up to
G FURTHER EXPERIMENTAL RESULTS
G.1 RESULTS ON PERSISTENCE TASKS
Persistence (a.k.a. reach-stay) tasks of the form F G specify that proposition needs to be true forever from some point on. We evaluate our approach on these tasks in the ZoneEnv environment, which features continuous action space and is thus particularly challenging for reach-stay specifications. Table 5 compares the performance of our approach to the relevant baseline GCRL-LTL. where we report the average number of steps for which the agent successfully remains in the target region after executing the e-action as the performance metric.3 The results confirm that our method can successfully handle complex persistence tasks, and performs better than the baseline.
'When the policy executes the e-action, this indicates that the target proposition should from then on be true forever (see e.g. in Figure 2). Since GCRL-LTL does not explicitly model the e-actions required for F G specifications, we employ an approximation and execute the e-action upon entering the target region for the first. time, i.e. when the agent first enters the blue region for the task F blue.
24

---

Published as a conference paper at ICLR 2025
Table 6: Evaluation results of trained policies on long reachability (R-12) and reach-avoid (RA-6) tasks. We report the success rate (SR) and average number of steps to satisfy the task (f)). Results are averaged over 5 seeds and 500 episodes per seed. "+" indicates the standard deviation over seeds.
1.T1 Acction
GCRL-LITI
DeepI.TI.
SR (t)
p (()
SR (1)
/ (L)
SR (1)
1 (L)
R-12
0.
47.80
0.93
60.15_2.58
0.98
43.33
RA-6
0.13
56.37 #0.89
0.62
30.64
00.00
24.94
G.2 ADVERSARIAL. TASKS WITH SAFETY CONSTRAINTS
We next demonstrate the advantages of our approach terms of handling safety constraints on an adversarial task. This task is specifically designed require considering safety requirements during high-level planning. We consider the configuration of the ZoneEnv environment depicted in Figure and the specification yp = -blue U (green V yellow) A magenta.
Figure 9 shows a number of sample trajectories generated by DeepLTL (top row) and GCRL-LTL (bottom row). Evidentl,, GCRL-LTL fails at satisfying the task, since it decides on reaching the green region during high-level planning without considering the safety constraint -blue. In contrast, DeepLTL. considers this safety requirement when selecting the optimal reach-avoid sequence, and hence chooses to reach the yellow region instead.
Quantitatively, GCRL-LTL only succeeds in satisfying the task 9.2% cases, whereas DeepLTL achieves success rate of 79.6% (averaged over 5 seeds and 100 episodes per seed). While LTL2Action does not have a high-level planning component, it considers the entire task includ- ing safety constraints via its GNN encoding, and averages success rate of 50.2%.
G.3 GENERALISATION TO LONGER SEQUENCES
In this section, we investigate the ability of our approach to generalise to longer sequences. Our evaluation so far has already demonstrated that our method can successfully learn general behaviour for satisfying LTL specifications by only training on simple reach-avor sequences. We now extend our analysis by specifically investigating tasks that require a large number of steps to solve.
In particular, we consider the following two task spaces in the LetterWorld environment: sequential reachability objectives of depth 12 (i.e. F (Pı A (F A depth 6 (i.e. -P1 (p2 A... (-P11 U P12))). Note that the longest reach-avoid sequences sampled during training are of length 3. In Table 6, we report the results of our method and the baselines on randomly sampled tasks from the task spaces described above. We observe that our approach generalises well to longer sequences and outperforms the baselines in terms of satisfaction probability and efficiency.
AF F P12)) and reach-avoid specifications of
G.4 ABLATION STUDY: CURRICULUM LEARNING
We conduct ablation study in the LeiterWorld environment investigate the impact of curriculum learning. We train our method without any training curriculum by directly sampling random reach- avoid sequenees of length 3, with potentially multiple propositions reach and avoid at each stage. The evaluation curves on reach/avoid specifications over training (Figure 10) demonstrate that curriculum training improves sample efficiency and reduces variance across seeds.
G.5 ABLATION STUDY: SEQUENCE MODULE
We conduct a further ablation study to investigate the impact of replacing the RNN the sequence module with Transformer (Vaswani et al., 2017) model. Since the reach-avoid sequences arising from common LTL tasks are generally relatively short (2-15 tokens), we expect the simplicity and effectiveness of RNNs to outweigh the benefits of the more complicated Transformer architecture in our setting. For our ablation study, we use a Transformer encoder to learn an embedding of the reach-avoid sequence the final representation of special [CLS) token, and keep the rest of the
25

---

Published as a conference paper at ICLR 2025
Figure 9: Trajectories of DeepLTL (top row) and GCRL-LTL (bottom row) on the adversarial config- uration of the Zny environment. The specification to be completed is -blue U (green V yellow) magenta. GCRL-LTL ignores safety constraints during high-level planning, and hence performs poorly. In contrast, DeepLTL yields trajectories that satisfy the specification.
Discounted return
0.6
0.5
0.4
0.3
0.2
Curriculum
0.1
No curriculum
0.2
Number of steps
1e7
Figure 10: Evaluation curves of training with and without curriculum on the LetterWorld environ- ment. Each datapoint is collected by averaging the discounted return of the policy across 50 episodes with randomly sampled reach/avoid specifications, and shaded areas indicate 90% confidence inter- vals over different random seeds.
Table 7: Comparison of Transformer- and GRU-based sequence modules. We report the success rate (SR) and average number steps to satisfy the task (J)). Results are averaged over seeds and 500 episodes per seed. "4" indicates the standard deviation over seeds.
DeepI.TI.-Traee -ransffrrer
DeepI.TI
SR (1)
j (L)
SR (t)
14 (L)
4P6
0.78 20.8
462.03 +52.03..2.800
0.92
303.38 43
477
0.46
438.244-42.5
0.91
299.95 +00 47
iP8
0.93
357.34451.86
0.9640.01
259.75
0.74
275. 1
0.90+0.03
203,36
P10
0.80
260.58
0.91
187.13
1
P11
0.90
137.46
0.98 0.98
106.21 +07.88
26

---

Published as a conference paper at ICLR 2025
0.12
DeepLTL
0.9
Discounted return
GCRL-ITL
Success aate
0.10
0.6
DeepLTL
0.06
0.5
GCRL-LTL
0.04
6
12
16
20
8
12
16
20
[AP]
[AP]
Figure 11: Impact varying the number atomic propositions on success rate (left) and discounted return (right). Each datapoint is an average over 500 episodes with randomly sampled reach/avoid specifications, and error bars indicate 90% confidence intervals over 5 different random seeds.
model architecture the same. We use an encoder model with an embedding size of 32, attention heads, and 512-dimensional MLP with dropout of 0.1. Despite this being a very small Transformer model, it still has more than 5 times the number of parameters of the GRU.
We report evaluation results for complex specifications in the ZoneEnv environment in Table 7, which strongly support our hypothesis that simpler RNN-based sequence module more effective.
G.6 IMPACT OF THE NUMBER OF ATOMIC PROPOSITIONS
We conduct experiment to evaluate the impact of the number of atomic propositions. For this, we consider modified versions of the FlarWorke World environment with n, {8, 12, 16, 20) regions of different colours (that is, in each version have n, regions and |AP] n,,)) The state space of the FlarWorld environment does not depend on the atomic propositions, therefore we can use the same model architecture throughout the experiment.
The results are shown in Figure 11. We observe that policy performance generally decreases as the number of atomic propositions increases, both for DeepL.TI. and GCRL-LTI. This result is expected, since we increase the number of possible tasks while keeping the number of policy parameters fixed. We also observe that the variance of success becomes larger as the number of atomic propositions increases. This can be explained by the fact that, in the case of large number of atomic propositions, the goal condiiiiond RL process may (for some random seeds) yield policy that cannot consistently satisfy every single proposition. If there exists proposition a E AP that the policy has failed to learn how to satisfy, the policy will consequently not successful in completing any task that requires to be achieved at any stage, resulting in low success rate. Finally, we observe that the performance reduction for DeepLTL generally is less than or similar to the performance reduction for GCRL-LTL.
G.7 IMPACT OF SPECIFICATION COMPLEXITY
In this section, provide additional insights regarding the performance of our approach with respect to the complexity of the given specification. An advantage of our method is the representation of tasks as reach-avoid sequences. This representation explicitly lists the possible ways of satisfying specification, making our approach in principle applicable to arbitrarily complex formulae. As an example, we consider the following specification the LetterWorld environment:
(a Fb (F Fd))) U ((F ((k v b) A (( d -i) U))) A (-hUR))V A ([(b = F(AFF)) U ((IVf) (- Ug)))).
which encompasses 11 unique atomic propositions and complex composition of different LTL operators. The corresponding LDBA consists of a large number of 656 states. However, by explicitly reasoning about the different ways of satisfying the specification, DeepLTL achieves average success rate of 98% (across different random seeds).
At the same time, note that seemingly simple formulae can be difficult to accomplish. In World this is especially true if they involve large number propositions to avoid. such as the specification (aa VbV.v e) U (f Fg), on which DeepL.TI. achieves comparatively low
27

---

Published as a conference paper at ICLR 2025
Table 8: Experimental comparison RAD-embeddings on different finite-horizon tasks in the ZoneEm environment. The numbers in parentheses represent the number of states in the LDBA/DFA. We report the success rate (SR) and average number of steps to satisfy the task (μ)). Results are averaged over 5 seeds and 500 episodes per seed. "+" indicates the standard deviation over seeds.
RAD-embeddings
DeepLTL
SR (1)
j (U)
SR (1)
96 (6)
0.9410.06
469.72.59.00
0.92.1.06
303.38 19.43
P7 (6)
0.88
474.34
0.91 10.03
299.95 1.0.47
PP (8)
0.9610.08
399.38 68.66
0.96.10.44
259.75
109.75
PP (5)
0.92
804.88aas.ck
0.90
14..99
Pio (4)
0.87 #0.11
336.90
0.91 +0.02
187.13
PP1 (4)
0.99 #0.01
149.02=11.77
0,98
106.21
reach/avoid (4/5)
0,91 0,91 +0.04
401.12=33.92
0.93
261.97
parity (5)
0,98+0.01
227227
0.96
112.1
largel (15)
40.32
550.5 206.79
0.92
314.72.-23.25
314.72
233.23
large2 (19)
0.66
490.22-240.23
0.94
322.38a24..0 2:4.02
322.38
success rate of 82% across 5 random seeds. In general, whether a given formula is challenging to satisfy depends primarily the dynamics of the underlying MDP.
Finally, we note that our approach relies on being able to construct an LDBA for a given specification, which is -opbeeexxponentill in the size of the formula in the worst case (Sickert et al., 2016). Inevitably, there thus exist LTL. specifications to which our approach is not applicable, since is infeasible to construct the corresponding LDBA.
G.8 COMPARISON TO RAD-EMBEDDINGS
Table 8 lists experimental results of DeepLTL and RAD-embeddings (Yalcinkaya et al., 2024) on finite-horizon tasks in the ZoneEnv environment. We consider tasks yss -01- from Table reach/avoid tasks (see Section 5.1), as well as parity task, and two tasks with large associated automata. 45 The parity task specifies that the agent has to reach blue while visiting green an even number of times, and yellow while visiting magenta an even number of times. Note that this task is not expressible in LTL., but our method can still be applied to the corresponding LDBA.
For RAD-embedding embeddings, and the policy is also trained on compositional RAD DFAs for 15M environment interaction steps. Throughout the experiments,
frozen GATv2 embeddings pre- treitrained compositional RAD DFAs,
the hyperparameters provided in (Yalcinkaya et al., 2024).
The results shows that RAD-embeddings and DeepLTT. achieve similar success rates, but DeepLTTL generally requires significantly fewer steps until task completion. They also demonstrate that approach indeed generalises to tasks not expressible in LTL, such as parity. Finally, we note that our method achieves substantially higher success rates on tasks with an increased number of states in the corresponding automaton (largel/2). These results further support the advantages of our approach of combining a high-level reasoning step with learned embeddings of reach-avoid sequences.
G.9 TRAJECTORY VISUALISATIONS
We qualitatively confirm that DeepLTL produces the desired behaviour by visualising trajectories in the ZoneEnv and FlarWorld environments for a variety of tasks (Figures 12 and 13).
'large/ corresponds the formula ((green + (-blue U ((magenta Fblue)) (-green U blue)))) (yellow F (magenta A blue))).. 'The formula for large2 is (green (yellow A (F (magenta A AF Fblue)))) U ((blue A A.F magenta) A (-yellow green)).
28

---

Published as a conference paper at ICLR 2025
Figure 12: Example trajectories of DeepLTL in the ZoneEn environment. (Top row) Trajectories for the task F (yellow A (Tgreen U blue)). (Middle row) Trajectories for the task G F yellow A GF blue A green. (Bottom row) Trajectories for the task F blue -magenta.
Figure 13: Example trajectories of DeepLTL in the FlatWorld environment. (Top row) Trajectories for the task (reedAAageetaAAA A (blue/ (geee)) (Bottom row) Trajectories for the task (-red (green/ blue A aqua)) A F (orange (F (red A magenta))).
29


Reviews:
[{"review_id": "rw1mR1XHDE", "reviewer": "Reviewer_aeBd", "summary": "This paper proposes a method that leverages linear temporal logic (LTL) to formulate reinforcement learning (RL) tasks. The authors claim that their method is applicable to infinite-horizon tasks and are non-myopic. The preliminaries and problem setting are presented in a clear and logical flow, and the experimental results are well-reported. However, the authors seem to have completely missed highly relevant literature in this area (see references below).", "questions": "Questions:\n1) In section 4.2 and 4.3, the explanation of the sequence module, which encodes reach-avoid sequence, is unclear. What are the inputs and the outputs of this module?  Could you provide an example to clarify?\n2) Why did you use an RNN? Transformer-based NN architectures outperform RNNs in many problems.\n3) In section 4.5, the statement “the value function is a lower bound of the discounted probability of reaching an accepting state k times via…” does not sound correct. How is the right hand side of the inequality equal to “the discounted probability of reaching an accepting state k times” ? Can you explain your reasoning? \n4) GCRL-LTL also works for infinite-horizon tasks. The experiment results imply that your method outperforms GCRL-LTL. Is there a theoretical explanation for why your method is better than GCRL-LTL? \n5) It is difficult to evaluate the novelty of this paper without a thorough comparison to approaches such as those used in the tool Mungojerrie [4]. Will such a comparison be possible in a short time?\n\n(See further questions in the post-rebuttal review)", "limitations": "", "rating": 8, "confidence": 5, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "1) The paper presents an interesting approach to learn policies to satisfy omega-regular specifications based on visiting accept states in an automaton without discounting states between the visits. \n2) It incorporates policies parameterized as neural networks.\n3) It uses the structure of the automaton specification.", "weaknesses": "The main weakness of this paper is that it ignores significant body of literature that deals with training policies for omega-regular objectives. Without a detailed comparison, it is difficult to evaluate the novelty in this paper. In fact, the technique of discounting seems quite similar to the zeta parameter used in the Hahn et al. paper from TACAS 2019. The authors should clarify how their approach is different.\n\nReferences:\n1. Hahn, E. M., Perez, M., Schewe, S., Somenzi, F., Trivedi, A., & Wojtczak, D. (2019, April). Omega-regular objectives in model-free reinforcement learning. In International conference on tools and algorithms for the construction and analysis of systems (pp. 395-412). \n2. Hahn, E. M., Perez, M., Schewe, S., Somenzi, F., Trivedi, A., & Wojtczak, D. (2020). Faithful and effective reward schemes for model-free reinforcement learning of omega-regular objectives. In Automated Technology for Verification and Analysis: 18th International Symposium, ATVA 2020, Hanoi, Vietnam, October 19–23, 202\n3. Le, Xuan-Bach, Dominik Wagner, Leon Witzman, Alexander Rabinovich, and Luke Ong. \"Reinforcement Learning with LTL and $\\omega $-Regular Objectives via Optimality-Preserving Translation to Average Rewards.\" arXiv preprint arXiv:2410.12175 (2024).\n4. Hahn, E. M., Perez, M., Schewe, S., Somenzi, F., Trivedi, A., & Wojtczak, D. (2021). Mungojerrie: Reinforcement learning of linear-time objectives. arXiv preprint arXiv:2106.09161.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "DmHACDlRTp", "reviewer": "Reviewer_Xrc5", "summary": "The authors propose a multi-task RL approach using goals specified in Linear Temporal Logic. The approach builds on recent work by reasoning about *accepting cycles* in the form of reach-avoid sequences and learns a goal-conditioned policy that can generalize to unseen specifications by finding the highest-valued reach-avoid sequence in the new specification('s automata), where the reach-avoid sequence goals are cast as learned embeddings. The approach is trained in a multi-task setting with a simple curriculum, and experimental results demonstrate that the DeepLTL approach outperforms previous approaches to goal-conditioned LTL-modulo-RL.", "questions": "* Can the authors compare against [1]/[6] in the previous section(s) and reason about why their approach may be preferable? The approaches are different in how they condition and compute embeddings but an argument by the authors advocating their own approach is important given the similarity of the work.\n* The authors include a curriculum-based ablation in the appendix that supports the presence of a curriculum. What other choices of curricula were considered? Do the authors have ideas on how a choice of curriculum would affect learning? \n* Section D.3 in the appendix seems to be missing. Can the authors provide this?\n* At what level of complexity of specification does the deepLTL approach break down? Does a larger alphabet (and therefore a larger class of reach-avoid sequences) make the goal-conditioned RL problem harder by expanding the space of possible embeddings?", "limitations": "", "rating": 8, "confidence": 5, "soundness": 3, "presentation": 3, "contribution": 2, "strengths": "* The paper is overall well-written and nicely constructed. \n* The problem of multi-task RL is, in my opinion, one of the most salient applications of using structured logical specifications. I think the paper does a nice job of trying to extend this.\n* The paper does a god job contextualizing some of the recent theory (e.g. regarding the eventual discounting objective) and discussing the relevance of it in a practical context.\n* The idea of using embeddings, cyclical acceptance, and predicate-conditioned learning builds directly on recent work [1] [2] [3] and I think these principles are helpful in the aim to scale automata-driven RL further to large scale applications.\n\n[1] Compositional Automata Embeddings for Goal-Conditioned Reinforcement Learning. Yalcinkaya et. al 2024.\n\n[2] LTL-Constrained Policy Optimization with Cycle Experience Replay. Shah et. al 2024.\n\n[3] Instructing Goal-Conditioned Reinforcement Learning Agents with Temporal Logic Objectives. Qiu et. al. 2023", "weaknesses": "Although building on very recent work is a good way to step the field forward, it does also beg a bit the question of significance. This work bears strong similarities to [3], with the primary change being to condition over reach-avoid sequences rather than individual atomic propositions or predicates that represent transitions within an automaton. The latter approach, which is what is done in [3], requires a planning-based approach each time a new automaton is seen. The authors do compare against [3] experimentally, and show that on individual challenging tasks their approach is better, which is appreciated. However, I'd like to see a more thorough experimental analysis of the DeepLTL approach itself. Since the DeepLTL approach is quite similar to prior work, this analysis-style work would greatly benefit the field. At what level of complexity of specification does the approach break down? Does a larger alphabet (and therefore a larger class of reach-avoid sequences) make the problem harder by expanding the space of possible embeddings?\n\nRegarding the writing: I don't think including the discussion on eventual discounting [4] (problem 3.1 and theorem 3.1) is totally necessary and the small extension of the theory that the authors provide is more or less orthogonal to their main contribution, which obscures the writing a bit. The authors use a discounted version of LTL as their objective but do not cite recent work that thoroughly explores this problem setting [5]. In section 4.1, the authors discuss reasoning over pre-computed accepting cycles, which bears strong similarities to an identical approach in [2]. Although [2] is cited it would be good for the authors to mention it in section 4.1 given these similarities.\n\nLastly, the approach from [1] is a highly similar approach to automata-goal-conditioned RL that also uses an embedding based approach. Although this work is contemporaneous, a previous version did appear [6] earlier and I think some sort of comparison, if not an explicitly direct one, would be important in strengthening this work.\n\n[1] Compositional Automata Embeddings for Goal-Conditioned Reinforcement Learning. Yalcinkaya et. al 2024.\n\n[2] LTL-Constrained Policy Optimization with Cycle Experience Replay. Shah et. al 2024.\n\n[3] Instructing Goal-Conditioned Reinforcement Learning Agents with Temporal Logic Objectives. Qiu et. al. 2023.\n\n[4] Eventual Discounting Temporal Logic Counterfactual Experience Replay. Voloshin et. al. 2023.\n\n[5] Policy Synthesis and Reinforcement Learning for Discounted LTL. Alur et. al. 2023.\n\n[6] Automata Conditioned Reinforcement Learning with Experience Replay. Yalcinkaya et. al. 2023.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "Shd91oV3Xy", "reviewer": "Reviewer_7njW", "summary": "The paper introduces a novel approach, called DeepLTL, to address the challenge of learning policies that ensure the satisfaction of arbitrary LTL specifications over an MDP. This approach reduces the myopic tendencies found in previous works by representing each specification as a set of reach-avoid sequences of truth assignments. It then leverages a general sequence-conditioned policy to execute arbitrary LTL instructions at test time. Extensive experiments demonstrate the practical effectiveness of this approach.", "questions": "The examples provided by the authors are all based on 2D grid-world environments. To evaluate the approach's performance in higher-dimensional settings, it would be valuable to experiment with environments like the 5-dimensional Carlo environment from [1], as well as other high-dimensional settings, such as the Fetch environment in [2], as utilized in [3]. Additionally, as a minor note, there is a typo on line 066 of the paper; it should read (c) instead of (b).\n\n[1] Cameron Voloshin, Abhinav Verma, and Yisong Yue. Eventual Discounting Temporal Logic Counterfactual Experience Replay. In Proceedings of the 40th International Conference on Machine Learning, pp. 35137–35150. PMLR, July 2023. \n\n[2] M. Plappert et al., “Multi-goal reinforcement learning: Challenging robotics environments and request for research,” 2018, arXiv:1802.09464.\n\n[3] Learning Optimal Strategies for Temporal Tasks in Stochastic Games Alper Kamil Bozkurt , Yu Wang , Michael M. Zavlanos , and Miroslav Pajic", "limitations": "", "rating": 8, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "The proposed approach is tailored to address key challenges of quality, clarity, and significance. Unlike existing techniques, this method is designed to handle infinite-horizon specifications and mitigate the non-myopic tendencies of previous approaches that often lead to sub-optimality. Additionally, it naturally incorporates safety constraints, represented through negative assignments, to guide the policy on propositions to avoid, which is an essential concept for effective planning. In general, the paper is well-written and effectively presented.", "weaknesses": "The approach proposed by the authors is compelling and aims to address an important problem. However, one concern is that the authors appear unaware of works like [1], [2], and [3], which introduced model-free reinforcement learning (RL) methods to tackle the same challenge of maximizing the probability of satisfaction for LTL specifications, expressed as Büchi automata and deterministic parity automata. These methods have even been extended to nondeterministic, adversarial environments (expressed as stochastic games) where nonrandom actions are taken to disrupt task performance, beyond standard MDPs. In such approaches, the LTL specifications are translated into limit-deterministic Büchi automata (LDBAs) to form product MDPs. Rewards are derived from automata using a repeated reachability acceptance condition, allowing controller strategies that maximize cumulative discounted rewards to also maximize satisfaction probabilities; standard RL algorithms are then used to learn these strategies. In my opinion, these results appear to weaken the authors’ claim that ‘Our method is the first approach that is also non-myopic, as it is able to reason about the entire structure of a specification via temporally extended reach-avoid sequences.’ Please discuss how your approach compares to and differs from the methods in [1], [2], and [3], with particular attention to handling non-myopic reasoning and addressing infinite-horizon specifications.\n\nA. K. Bozkurt, Y. Wang, M. M. Zavlanos, and M. Pajic, “Control synthesis from linear temporal logic specifications using model-free reinforcement learning,” in Proc. Int. Conf. Robot. Automat., 2020, pp. 10349–10355\n\nE. M. Hahn, M. Perez, S. Schewe, F. Somenzi, A. Trivedi, and D. Wojtczak, “Omega-regular objectives in model-free reinforcement learning,” in Proc. Int. Conf. Tools Algorithms Construction Anal. Syst., 2019, pp. 395–412.\n\nLearning Optimal Strategies for Temporal Tasks in Stochastic Games Alper Kamil Bozkurt , Yu Wang , Michael M. Zavlanos , and Miroslav Pajic", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "ZscqE0uSUF", "reviewer": "Reviewer_T576", "summary": "This paper presents a reinforcement learning based policy synthesis method for a robot to satisfy a Linear Temporal Logic (LTL) specification. The salient features that distinguish this paper from prior work are the following: (1) the proposed method does not aim to generate a policy for a fixed LTL formula but rather to deal with any arbitrary one, (2) it can deal with specifications that can be satisfied only through infinite length execution,  and (3) it ensures the satisfaction of the safety requirements, and (4) it optimizes the length of the trajectory. The proposed method is based on the observation that the satisfaction of a specification primarily depends on the loops including the final states in the Buchi automaton equivalent to the given specification. For a given LTL formula, the sequence of the sets of actions that lead to the satisfaction and violation of the specification is identified and the policy is trained based on those sequences. On the test time, the policy for the target LTL formula can utilize the policy learnt based on many different LTL specifications and thus the learnt policy can be used in a zero-shot manner. The authors evaluate their method on three benchmark environments and compare it with two baselines. Experimental results establish the proposed method to be superior to the state-of-the-art methods both in terms of the rate of success in satisfying the test specifications and the optimality of the length of the trajectories.", "questions": "In Example 1, why can’t we replace the transition on $\\epsilon_{q_2}$ by a transition on the action $a$ to generate an equivalent Buchi automata?\n\nIn Line 252, in $\\delta(q_i, a) \\ne q_i$, wouldn’t the second $q_i$ be $q_{i+1}$?\n\nIs it not the case that restricting the actions in the set $A_i^+$ will ensure that the actions are not from the sets $A_i^-$?  These two sets appear to be mutually exclusive. Then why do we need to keep track of both?\n\nSome of the terms used in the paper have never been introduced. For example, what is $sup(\\xi)$? How to interpret $\\tau \\sim \\pi | \\varphi$?\n\nOn Line 107, please use $\\equiv$ instead of “=“ to denote formula equivalence.", "limitations": "", "rating": 8, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 4, "strengths": "This paper improves the state-of-the-art for reinforcement learning with LTL specifications in several directions. Unlike the earlier methods, the proposed technique can deal with arbitrary LTL specifications at test time, supports infinite-horizon LTL specifications, ensures the satisfaction of the safety constraints, and attempts to optimize the trajectory length. Thus the technical contribution of the paper is significant.\n\nThe experimental evaluation is quite exhaustive, establishing the efficacy of the proposed method compared to the state-of-the-art.", "weaknesses": "The presentation in some parts of the paper could be improved. Specifically, a running example could help understand several complex ideas. For example, Section 4.2 could be easier to understand had an example been provided. Similarly, the paragraph on representing the reach-avoid sequence on page 6 could also be accompanied by an example. Furthermore, an example of how the negative assignments help could help convince readers about their necessity.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Decision: Accept (Oral)