Venue: NeurIPS 2022 Conference

Reviews:

final_score: rating: 7: Accept: Technically solid paper, with high impact on at least one sub-area, or moderate-to-high impact on more than one areas, with good-to-excellent evaluation, resources, reproducibility, and no unaddressed ethical considerations.
review_content: summary: Policy optimization in RL often involves complex reward engineering that can lead to unexpected results. Linear temporal logic (LTL), however, provides a robust language to encode a cost function where a scalar cost function may be unnatural. This paper provides a novel approach to LTL-constrained reinforcement learning, LTL constrained planning or LCP, under fewer assumptions and providing stronger guarantees than in the existing literature. The authors propose LCP based on a reduction to a reachability problem, and they show that the algorithm "offers strong constraint satisfaction guarantees", as well as prove its sample complexity. The algorithm itself consists of 3 parts: (1) finding an AMEC given the product MDP; (2) finding a cost-optimal recurrent policy within the AMECs; (3) finding a cost-optimal transient policy to reach this AMEC. Finally, the authors provide an empirical evaluation of their method on various environments, showing that their method achieves higher performance with lower sample complexity compared to baselines.
strengths_and_weaknesses: Originality & Quality: To the best of my knowledge, the method LCP appears to be new, and well-situated in / compared to the existing literature. This work is complete, proposing a method and evaluating it against existing baselines. 

Clarity: The submission is clearly written and well-organized. In particular, the inclusion of a section detailing the high-level intuition is very useful to orient the reader, as the work introduces a lot of terminology and is easy to get bogged down in e.g. the proofs in the appendices.  Ideally, I would have liked to see a conclusion that recaps the takeaways from this work and that lays down an avenue for future work, but perhaps this is just a matter of style.

Significance: This work provides a unique theoretical and experimental approach to policy optimization by reframing LTL constrained policy optimization as a reachability problem to recurrent states. 
questions: I believe the paper, which is quite theoretical, could be improved with some discussion for practitioners, i.e. when to use LCP and when LCP would not offer extra benefit (apart from in truly infinite-horizon problems). In particular, the authors only present empirical evaluations in which LCP outperforms existing methods. Were there environments tested where LCP did not outperform existing baselines? LCP tends to give a larger advantage over baselines under which conditions (e.g. when the task is more complex)?
limitations: Limitation are discussed in Section 6, where authors describe how LCP may fall short when used alone in infinite-horizon problems.
review_title: null

final_score: rating: 7: Accept: Technically solid paper, with high impact on at least one sub-area, or moderate-to-high impact on more than one areas, with good-to-excellent evaluation, resources, reproducibility, and no unaddressed ethical considerations.
review_content: summary: This paper presents a novel framework for reinforcement learning under hard LTL constraints. The proposed method, LCP, finds policies that primarily aim to satisfy the constraints over infinite horizons while secondarily minimizing a cost function (representing soft preferences). The method also relaxes many restrictive assumptions from prior works and is rigorously justified through theoretical analysis. Experiments on two RL domains help verify these claims and show the competitive performance of LCP compared to a prior method, LCRL. 
strengths_and_weaknesses: **Originality**: To my understanding, this work borrows ideas from the literature (e.g. the concept of MECs in model checking is widely known) but proposes an elegant and original approach derived from these concepts. This allows the authors to derive strong theoretical guarantees, and some of the key differences with respect to prior work are explained in the text. However, I admit there may be related work that I'm unaware of. 

**Quality**: 
The authors propose a strong model-based approach, LCP, to the LTL-constrained policy optimization problem. This method is backed by rigorous theoretical analysis, though I was unable to verify all of the proofs (which are numerous, and quite dense). However, LCP is conceptually easy to understand and the claims appear reasonable. I have one minor issue with the framework, which I hope the authors can clarify in a question below. 

The superior performance of LCP over a prior work, LCRL, are demonstrated on two domains, though I think the reasons for this need better explanation. The current claim that vanilla LCRL performs worse due to the "extremely sparse" cost function is dubious, as the cost function is uniform everywhere and virtually irrelevant in both domains. Overall, the experiments have a few other weaknesses:

- The performance of LCP appears quite sensitive to specific LTL constraints, and should be evaluated on more than only two.
- The cost function seems to play no role for LCP and vanilla LCRL in the current environments, reducing the problem to "maximize the probability of satisfying the constraint." 

**Clarity**: Overall, the paper is very well-written except for the short experiments section, which delegates many important details to the Appendix. I would also appreciate if the authors could report the LBDAs and the MECs (or a brief description) for these domains so that reviewers can better understand how LCP handles these problems.

**Significance**: This paper tackles the important problem of learning constraint-satisfying policies with guarantees. The authors frame this problem in a novel setting and provide an in-depth theoretical analysis which I believe will be useful to others in the field. The claims are backed by experiments, but as of now, their significance is unclear, in part due to missing details. 




questions: - Often in Markov reward processes, only the recurrent cost rate is considered since the transient costs do not affect the long-term average cost. What's the motivation for including transient costs in the optimization objective? 

- (Minor issue with the framework): It's unclear to me that (OPT) is a well-defined optimization problem (with a solution $\pi^*$ that is at least as good as any other solution). This is touched on by the in-text discussion of $\eta$-greedy policies. If this is the case, then Corollary 5.2 is problematic since the result of the argmin wouldn't be defined.

- In the PacMan domain, how would incorporating the food reward into the cost, rather than the LTL constraint, affect the performance of LCP? To my understanding, either objective could specify the same desired behaviour. 
limitations: The limitations were adequately addressed.
review_title: null

final_score: rating: 6: Weak Accept: Technically solid, moderate-to-high impact paper, with no major concerns with respect to evaluation, resources, reproducibility, ethical considerations.
review_content: summary: The authors introduce a formal method for incorporating a probabilistic notion of LTL satisfaction for RL settings. They take the common approach to cross-product the statespace of the LTL's buchi automata for a combined reachable search space, and with the assumption of being able to sample any (s,a) pair on demand, propose a series of algorithms that separately treat the strongly connected components of the reachable states that infinitely achieve the goal condition (a requirement for infinite-trace LTL).

## Revised Score
Raised my evaluation after the authors teased apart the distinction to related work in the rebuttal.
strengths_and_weaknesses: ### Originality
As far as I'm aware, the approach to uniquely treat the SCCs of the merged state space (and the strategy to move between them) is unique. The only major issue I found with the originality is the absence comparison to much of the recent work on reward machines, LTL, etc, and how they can be used to control RL. It's unclear to me if these works come with the same assumptions highlighted in the other RL+LTL works cited in the paper. Some examples include:

- Reward Machines: Exploiting Reward Function Structure in Reinforcement Learning
- LTL2Action: Generalizing LTL Instructions for Multi-Task RL
- LTL and Beyond: Formal Languages for Reward Function Specification in Reinforcement Learning
- Using Reward Machines for High-Level Task Specification and Decomposition in Reinforcement Learning


### Quality
The quality of the work appears to be of high caliber, but assessing it was difficult (more below).

### Clarity
The paper is very dense -- it felt more like an extended abstract to a JMLR paper than a well rounded and self-contained conference submission. At times, entire paragraphs are just paraphrased sentences to results described and elaborated upon in the extensive supplementary work (e.g., paragraph just before section 6). The most difficult sections include:

- Definitions 3.2 and 3.3
- Definition 4.2
- Lines 217 to 234

The general writing is extremely well done and free of grammatical / spelling issues. The only place caught my eye as a potential error is line 145 -- I think it should be $(E, A_E)$ and not $(E, A_{E'})$, and the $E \subseteq E'$ should probably be $E \subset E'$.

### Significance
While the results are strong, the significance is largely impacted by the small size of empirical domains and (ultimately) the sampling requirements for the approach to have any guarantees. It's unclear to me if these techniques can be applied in any reasonably sized RL setting (dozens to hundreds of atoms in a state).
questions: 1. How might this work be modified to handle sample traces rather than arbitrary sampling of state-action pairs?
2. How might any of this work be used in settings where the reachable state-space is unrealistic to enumerate? E.g., if $|AP|>100$
limitations: The limitation of being able to arbitrarily sample from the statespace seems kind of strong. Being able to reset is a fairly strong assumption, but being able to arbitrarily sample any $(s,a)$ pair is a very strong one. I feel similarly about the number of samples required (both theoretically and empirically) across the entire state space.

There is no immediate societal impact from this work, and the authors highlight this adequately.
review_title: null

Meta-review: metareview: We have three reviews with high scores but not high confidence (confidence 2,3,3).  However, the reviews by pGRX and Kr29 seems fairly thorough with strong author responses.  I was particularly satisfied with the author responses as were the these two reviewers.  I have a lingering concern about whether the baselines for the Pacman and Mountain Car are strong enough.  But the conceptual and theoretical contribution seems to warrant publication.
confidence: Less certain
Decision: Accept