DeepLTL: Learning to Efficiently Satisfy Complex LTL Specifications for Multi-Task RL

Thank you for taking the time to review our paper! We are pleased to read your positive comments, especially that the "technical contribution of the paper is significant" and that we perform an "exhaustive" experimental evaluation. Please see below for answers and comments regarding the points raised.

Negative assignments $A_i^-$

We think there might be a small misunderstanding regarding the negative assignments. For a path $(q_1, q_2, \ldots)$ in the LDBA, the positive assignments $A_i^+ = \\{ a : \delta(q_i, a) = q_{i+1} \\}$ are the assignments that lead to the next state $q_{i+1}$. The negative assignments are all assignments that do not lead to $q_{i+1}$ and do not form a self-loop. This is why we have the condition $\delta(q_i,a)\neq q_i$ in the definition of the set $A_i^-$.

We appreciate that this might not have been entirely clear in the writing. We have thus made a small change to Section 4.1, explicitly mentioning that $A_i^-$ excludes self-loops, to hopefully make this clearer.

Is 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?

This question relates to our discussion above. $A_i^-$ contains assignments that the policy needs to avoid, i.e. assignments that lead to a different state than the desired one and that do not form a self-loop. For example, consider the formula $\neg a \mathsf{U} b$. In this case, $A_i^-$ contains all assignments where $a$ is true (since this leads to an undesired state in the automaton), $A_i^+$ contains all assignments in which $b$ is true, and all other assignments can safely be ignored by the policy since they keep it in the same LDBA state (e.g. the assignment $\\{ a\mapsto \text{false}, b\mapsto\text{false}, c\mapsto\text{true} \\}$). Intuitively, the policy's goal is to materialise an assignment in $A_i^+$, but this may require many steps, during which it must avoid assignments in $A_i^-$ but is allowed to materialise other assignments.

Comments and questions

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.

Many thanks for this suggestion. Since we already provide high-level examples in Figure 3 and Figure 4, do you have any suggestions how we can improve them to make the relevant sections easier to understand?

In Example 1, why can’t we replace the transition on $\varepsilon_{q_2}$ by a transition on the action $a$ to generate an equivalent Buchi automata?

You are right that we could in principle replace the $\varepsilon$-transition with an $a$-transition to obtain a Büchi automaton accepting the same language. However, the resulting automaton would not be an LDBA. In particular, note that the transition $\neg b$ (the self-loop on state $q_0$) already contains the assignment in which $a$ is true. As such, the transition function would be non-deterministic for the input $a$ in state $q_0$.

The advantage of LDBAs is that they contain all non-determinism in the $\varepsilon$-transitions, which can be folded into the action space of the policy, and thus learned (see Definition 1 and the discussion thereafter). If we used a non-deterministic Büchi automaton, we would not know how to progress the product MDP in the case of a non-deterministic transition.

Some of the terms used in the paper have never been introduced. For example, what is $supp(\xi)$? How to interpret $\tau\sim\pi|\varphi$?

$supp(\xi)$ denotes the support of probability distribution $\xi$, i.e. all formulae with nonzero probability. We have clarified this in the revised version of the paper. We introduce the notation $\tau\sim\pi$ in line 96 and the notation $\pi|\varphi$ for a specification-conditioned policy in line 147.

On Line 107, please use $\equiv$ instead of “=“ to denote formula equivalence.

Many thanks, we have revised the paper accordingly.

Thank you again for your comments and feedback! We hope our response and edits have clarified some of the points. Please let us know if you have any other questions or remarks!

We thank you for the detailed feedback and are pleased that you found our approach "compelling" and our paper "well-written and effectively presented". Nevertheless, we would like to point out some possible misunderstandings that might have negatively impacted the assessment.

Comparison to [1], [2], and [3]

We appreciate these references and agree that they are generally relevant in the context of our work. However, please note that these approaches tackle a different/simpler problem than the one we consider and are not applicable to our setting. In particular, our approach is realised in a multi-task RL setting and we train a single policy that can zero-shot execute arbitrary unseen LTL specifications at test time. In contrast, the methods in [1], [2], and [3] only learn a policy for a single, fixed task. This is a crucial difference: our approach trains a single policy once, which can then satisfy arbitrary tasks such as the ones in our evaluation (see Tables 2 and 3). The given references would have to train a separate new policy for every specification, and cannot generalise to new tasks at test time.

We have submitted an updated version of the paper to hopefully make this distinction clearer. The updated version includes a changed title that explicitly mentions multi-task RL, and minor corresponding edits to the abstract and introduction. We have also updated the related work section (Section 6) to more explicitly point out the differences to methods that only handle a single task, and include an extended discussion of related work in the appendix (see Appendix C in the updated paper), which includes the provided references.

In my opinion, these results appear to weaken the authors’ claim that ‘Our method is the first approach that is also non-myopic [...]'

We appreciate that previous methods that learn a policy for a single LTL specification are generally non-myopic and can handle infinite-horizon specifications. However, we are not aware of any non-myopic method that is able to satisfy infinite-horizon specifications in the multi-task RL setting. If you are aware of such a method, we would greatly appreciate a reference.

2D grid-world environments

Please note that our experiments include the high-dimensional ZoneEnv environment with continuous state and action spaces, which is a standard environment in previous research on multi-task RL with LTL tasks (Vaezipoor et al. 2021, Qiu et al. 2023). This is a Mujoco environment consisting of a robot navigating a planar world with continuous acceleration and steering actions while observing sensory information, including lidar observations about various coloured zones. The state-space of this environment is 80-dimensional (compared to the 25-dimensional Fetch environment and the 5-dimensional Carlo environment). For a description of the environment see Section 5.1 and Appendix E.

We also consider the FlatWorld environment, which similarly features a continuous state space (albeit of lower dimensionality 2).

We therefore believe our experiments already demonstrate the performance of our approach in high-dimensional and continuous environments.

Additionally, as a minor note, there is a typo on line 066 of the paper; it should read (c) instead of (b).

Many thanks, we fixed the typo in the updated version of the paper.

We appreciate your comments and hope that our response with the corresponding edits in the revised version of the paper has made our contribution clearer; in particular the difference to related work that handles only a single LTL specification, and our evaluation in high-dimensional environments. Please let us know if this mitigates your concerns!

Thank you for taking the time to review our paper! We provide answers to your questions below. In particular, we would like to point out some possible misunderstandings that might have negatively impacted the assessment.

Existing literature on $\omega$-regular objectives

We appreciate the given references and agree that they are relevant in the context of our work. However, please note that these approaches tackle a different/simpler problem than the one we consider and are not applicable to our setting. In particular, our approach is realised in a multi-task RL setting and we train a single policy that can zero-shot execute arbitrary unseen LTL specifications at test time. In contrast, the methods in [1-4] only learn a policy for a single, fixed task. This is a crucial difference: our approach trains a single policy once, which can then satisfy arbitrary tasks such as the ones in our evaluation (see Tables 2 and 3). The given references would have to train a separate new policy for every specification, and cannot generalise to new tasks at test time.

We have submitted an updated version of the paper to hopefully make this distinction clearer. The updated version includes a changed title that explicitly mentions multi-task RL, and minor corresponding edits to the abstract and introduction. We have also updated the related work section (Section 6) to more explicitly point out the differences to methods that only handle a single task, and include an extended discussion of related work in the appendix (see Appendix C in the updated paper), which includes the provided references.

In the context of multi-task RL with LTL specifications, which is the problem we consider in our paper, we are only aware of a single work that can handle $\omega$-regular specifications (Qiu et al. 2023). As we discuss in the paper (Section 4.6 and lines 518-525) our approach has various theoretical advantages (also see below), and we demonstrate that it performs better in practice (see Table 1, Figure 6, Table 5, Figure 9).

Answers to questions

Q1

As illustrated in Figure 4, the sequence module takes as input a reach-avoid sequence $\sigma$ and outputs a corresponding embedding $e_\sigma$ that is used to condition the policy. For example, if the current task is F (a & F b), the corresponding reach-avoid sequence is (({a}, {}), ({b}, {})) (where all avoid sets are empty). The sequence module maps this sequence to some embedding $e\in\mathbb R^n$ which conditions the trained policy to first reach proposition a and subsequently reach proposition b.

Q2

We mainly opted for RNNs for the sake of simplicity: while Transformers excel at long-distance tasks, the sequences arising from the LTL formulae we consider are generally relatively short (2-15 tokens). Furthermore Transformers are known to be difficult to train and require large amounts of training data (Liu et al. 2020). We also note that our choice is consistent with previous works, which mainly use GRUs for sequence modelling (Kuo et al. 2020, Vaezipoor et al. 2021, Xu and Fekri 2024).

[1] Liu et al (2020). ‘Understanding the Difficulty of Training Transformers’. In EMNLP'20.

Q3

Let $\sigma$ be a truncated reach-avoid sequence that visits an accepting state $k$ times, and denote the length of $\sigma$ as $n$. As per our training procedure (Section 4.4) we have that $i = n + 1$ iff the agent has satisfied all assignments in $\sigma$, i.e. successfully finished "executing" the sequence. This means the agent has visited an accepting state $k$ times. The expected value

$$\mathbb E_{\tau\sim\pi|\sigma}\left[ \sum_{t=0}^\infty \mathbb 1[i = n+ 1]\right]$$

is thus exactly the probability of the policy reaching an accepting state $k$ times by following $\sigma$.

Q4

Yes, in comparison to GCRL-LTL our method is non-myopic and considers safety constraints during planning (cf. Section 4.6 and lines 520-523). These theoretical advantages explain why our approach outperforms GCRL-LTL in terms of efficiency and satisfaction probability. In Appendix F.2 we also provide a further comparison to GCRL-LTL on tasks with safety constraints, which highlights the differences in the planning approaches.

Q5

As discussed above, our paper proposes a novel method for zero-shot execution of arbitrary LTL specifications in a multi-task RL setting. This is fundamentally different from the approaches implemented in [4], which train a policy for a single, fixed specification and cannot generalise to different tasks. Do you still think such a comparison is useful and required, given the fundamentally different problem statements?

We appreciate your comments and hope that our response along with the corresponding edits in the revised version of the paper has made our contribution clearer. If anything else is unclear, we would be more than happy to engage in further discussion. Please let us know if this mitigates your concerns!

Thank you for your response. We are pleased that the updates to the paper have clarified our contribution. Below we respond to the suggestions and criticisms raised (in two parts).

RNNs vs Transformers

Thank you for your suggestion! As discussed in our original response, we opted for RNNs over Transformers since the reach-avoid sequences arising from common LTL tasks are generally relatively short (2-15 tokens). In this scenario, we believe that the simplicity of training RNNs outweighs the empirical performance gains observed in Transformers on long-distance tasks with vast amounts of data.

We confirm this hypothesis by experimentally evaluating DeepLTL with a Transformer model instead of an RNN in the ZoneEnv environment. For this, we broadly follow the BERT architecture: we use a Transformer encoder to learn an embedding of the sequence $\sigma$ as the final representation of a special [CLS] token. We use a small model with an embedding size of 32, 4 attention heads, and a 512-dimensional MLP with dropout of 0.1. Note that even though we use such a small Transformer model, it still has more than 5x the number of parameters of the RNN.

We report the achieved success rates in the table below:

The results confirm our intuition that RNNs perform better than Transformers in our short-sequence and relatively low-data setting (compared to e.g. foundation models). We are happy to include these experimental results as an ablation study in the final version of the paper.

Comparison to Mungojerrie

Our approach differs in several key respects from the tool Mungojerrie. First and foremost, we address the problem of learning a policy that can zero-shot execute arbitrary LTL specifications, whereas Mungojerrie only learns a policy for a single, fixed LTL specification. As such, our techniques are fundamentally different: we first train a general sequence-conditioned policy on a variety of reach-avoid sequences with a focus on generalisation to arbitrary sequences. At test time, we are given an unseen LTL formula, construct the corresponding LDBA, extract possible reach-avoid sequences, select the best sequence according to the learned value function, and finally leverage the trained sequence-conditioned policy to satisfy the formula (see Figure 3).

In contrast, Mungojerrie only has to deal with a single LTL specification. It constructs the LDBA for this, and directly trains a policy in the product MDP of the original MDP and the LDBA. Mungojerrie introduces a variety of different reward schemes for the reinforcement learning objective that ensure the resulting policy is probability-optimal. In contrast, we trade off optimality and efficiency of the resulting policy (see the discussion in Section 3 and Appendix B).

Empirical comparison

We agree that there is value in comparing to methods that only work for a single specification. However, please note that the primary purpose of our method is to learn a policy that is able to generalise to arbitrary formulae at test time, and this is what we test in our experimental evaluation: we train a single policy and test it on a range of complex tasks. We thus compare to methods that tackle the same problem in our experiments, as it is not clear how to fairly compare to methods that can only handle a single specification. We also note that Mungojerrie cannot be easily applied to the experiments that we consider, since it can only handle models with finite state and action spaces specified in PRISM, whereas we consider arbitrary MDPs with potentially continuous state and action-spaces (e.g. ZoneEnv, FlatWorld).

Technical details

We hope our discussion above clarifies the technical differences between our method and Mungojerrie. The $\zeta$ parameter in Mungojerrie is used to ensure that the reward-optimal policy is also probability-optimal. This is comparable to eventual discounting (Problem 1) (Voloshin et al. 2023), which ensures probability-optimality by only discounting visits to accepting states, without introducing an additional hyperparameter such as $\zeta$. Note that we first extend eventual discounting to the multi-task setting (Problem 1 and Theorem 1), but then consider a modified version which trades of probability-optimality with efficiency for the rest of the paper (Problem 2).

We continue our response below.

Writing

I don't think including the discussion on eventual discounting [4] (problem 3.1 and theorem 3.1) is totally necessary [...] obscures the writing a bit.

We include the discussion on eventual discounting since we believe it is important to formally develop the problem statement and motivate the approximate objective in Problem 2. This is especially important since one of the advantages of our method is that it is non-myopic, which is not a concern under the eventual discounting setting. Do you have any suggestions how we could make this discussion clearer?

The authors use a discounted version of LTL as their objective but do not cite recent work that thoroughly explores this problem setting [5].

Many thanks for the reference! We now cite [5] in Section 3 and added a discussion of discounted LTL to the appendix (Appendix C).

In section 4.1, the authors discuss reasoning over pre-computed accepting cycles, which bears strong similarities to an identical approach in [2].

We appreciate that there are similarities between our approach and [2], and followed your suggestion of mentioning these explicitly in Section 4.1 in the updated paper. However, we also note that there are significant differences between our approach and [2] : [2] makes use of accepting cycles in the setting of a single, fixed task for the purpose of reward shaping. In contrast, we use the set of paths to accepting cycles from the current LDBA state as a representation to condition a goal-conditioned policy in a multi-task setting, and show that we can use them for learning useful goal embeddings. We are not aware of any prior work that uses accepting cycles in a similar way.

Questions

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?

The curricula are designed to gradually expose the policy to more challenging tasks. As such, the curricula we consider generally start with short reach-avoid sequences and move on to longer and more complex sequences as the policy improves. Intuitively, it does not make sense to train on a sequence $(a,b)$ if the policy cannot yet satisfy $(a)$ alone. This explains why we observe in our ablation study that using a curriculum speeds up learning; we believe that other curricula with similar properties should yield comparable results. In particular, we would be excited to explore techniques such as automated curriculum design in future work.

Section D.3 in the appendix seems to be missing. Can the authors provide this?

Many thanks for catching this, we include the hyperparameters in the updated Appendix F.3.

Thank you again for the detailed feedback! We hope that the updates to the paper, additional experimental results, and our comments are helpful. Please let us know if these have addressed your concerns. We are more than happy to engage in further discussion!

Thank you for taking the time to review our paper! We are pleased to read your positive comments, and very much appreciate the detailed feedback. We agree with the proposed changes and have thus updated the paper to address the feedback, including further experimental results and a discussion and experimental comparison to [1]. Below we provide a detailed response to the points and questions raised (in two parts).

Further experimental analysis of DeepLTL

Does a larger alphabet (and therefore a larger class of reach-avoid sequences) make the problem harder by expanding the space of possible embeddings?

We investigate this question in the updated Appendix G.5. We conduct experiments in a modified version of the FlatWorld environment with a varying number of atomic propositions. We chose FlatWorld as it can be readily augmented with the number of propositions as a parameter, and since its state space does not depend on the number of propositions. This allows us to use the same model architecture in each case, and control for differences arising solely from different state spaces.

The results confirm our expectation that policy performance generally decreases as the number of propositions increases, since additional propositions significantly increase the task space, making the goal-conditioned RL problem more difficult. However, we note that the performance decrease of DeepLTL is generally similar or less than the performance reduction of the baseline GCRL-LTL. Integrating more advanced goal-conditioned RL algorithms, such as counterfactual experience [4], would likely further improve performance in environments with a large number of propositions; however, this is not the main focus of our paper and we thus leave it for future work.

At what level of complexity of specification does the approach break down?

We provide a discussion and experimental analysis in the updated Appendix G.6. An advantage of our task representation based on reach-avoid sequences is that it makes the ways of satisfying a given specification explicit, allowing our method in principle to scale to large and complex formulae. We illustrate this with a concrete example formula that results in an LDBA with 656 states, with DeepLTL still achieving a success rate of 98%.

However, generally the complexity of satisfying a given specification primarily depends on the underlying MDP. For example, if proposition p is difficult to achieve in the MDP, then even the simple formula F p is challenging. Finally, we note that we assume that we can construct the LDBA, which is doubly-exponential in the worst case (Sickert et al. 2016). While many other methods also rely on this assumption, clearly there are cases in which it is infeasible to construct the LDBA.

Comparison to [1]

Many thanks for providing this reference. We now mention it in the updated related work section and give a more detailed comparison in the extended related work (Appendix D). Furthermore, we conduct an experimental comparison of our approach and [1] in Appendix G.7.

In contrast to our approach, [1] is based on DFAs, which are limited to finite-horizon tasks and thus strictly less expressive than LDBAs. Their approach to computing embeddings is also different: [1] computes an embedding for the entire automaton, whereas we compute embeddings of reach-avoid sequences extracted from the LDBA. This separates high-level reasoning (how to satisfy the specification) from low-level reasoning (how to act in the MDP) and allows the goal-conditioned policy to focus on achieving one particular sequence of propositions.

Our experimental results demonstrate that [1] and our method achieve similar success rates on finite-horizon tasks, but our method generally requires significantly fewer steps until completion. We also note that DeepLTL achieves much higher success rates on tasks with a large associated automaton, since our policy is conditioned on only a single satisfying sequence rather than the whole automaton structure. These results highlight the advantages of our embeddings based on reach-avoid sequences.

We continue our response below.