Venue: ICLR 2021 Conference

Reviews:

final_score: rating: 6: Marginally above acceptance threshold
review_content: update after rebuttal: I think the paper, with the added discussion, improved. 

Summary and Contribution

This paper concerns safe reinforcement learning. In particular, it takes the perspective of constraining system behavior using formal languages instead of the usual constraint MDP framework where an additional (simple) cost function is used. The constraints are given as finite automata which are basically used as a product with the original MDP state space. The paper provides an empirical evaluation using several state of the art benchmarks.



Reasons for Score

With more details on the correctness, better literature study, and more experiments, the paper would be a clear accept. As of now, I see it as marginally above the acceptance threshold.

Strengths

- A relevant problem is tackled.
- The usage of formal languages is relevant and has been demonstrated to be helpful in a number of results

Weaknesses

- The contribution of the paper is not clear. Several other works have done very similar approaches, and in much more depth.
- The assumptions are not clear.

Questions for Authors

- Please compare your work to the literature listed below. What is novel, how does it relate?
- What is the exact assumption on prior knowledge? Does the MDP need to be known beforehand, or is the exploration of an RL algorithm basically guided by the finite automaton? 
- In the construction of the formal setting, what is different to the standard product construction of MDPs and finite automata? 


Detailed Comments

- related work

At least three papers (one of them is cited) constrain MDP exploration using regular languages (in fact, omega-regular languages). I don't see the novelty, but I'm happy to be convinced otherwise. See:

Mohammadhosein Hasanbeig, Alessandro Abate, Daniel Kroening:
Logically-Correct Reinforcement Learning. CoRR abs/1801.08099 (2018)

Mohammadhosein Hasanbeig, Alessandro Abate, Daniel Kroening:
Cautious Reinforcement Learning with Logical Constraints. AAMAS 2020: 483-491

Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, Dominik Wojtczak:
Omega-Regular Objectives in Model-Free Reinforcement Learning. TACAS (1) 2019: 395-412

- formal construction
In the very short theory part of the paper, the construction seems to me just as the standard construction to a product of an MDP and a finite (omega-regular) automaton. In a nutshell, one has a labelled MDP where the labels correspond to the alphabet of an automaton. Then, a run of the MDP produces a sequence of labels (a trace), which can be checked by the automaton. Now, a product construction of both yields an MDP where a reachability computation for so-called end components gives the probability to satisfy the formal language constraint. See for instance text books such as Baier and Katoen, Principles of Model Checking. As this part is the main body of the technical body of the paper, I would really like to understand, what is the difference. 

review_title: Novelty and technical contribution of the paper is unclear.

final_score: rating: 5: Marginally below acceptance threshold
review_content: #### Summary
The paper proposes a constrained reinforcement learning (RL) formulation relying on constraints written in a formal language. The proposed formulation is based on constrained Markov decision processes where the constraint is represented as a deterministic finite automaton that rejects any trajectory violating the constraint. The proposed solution relies on transforming the automaton's sparse binary cost into an approximate dense cost and augmenting that with the reward objective. The paper presents a series of results from simulations in Safety Gym, MuJoCo, and Atari environments.

#### Strength
1. Constrained RL is certainly an important research area, having a variety of applications such as safety-critical problems.
2. The constraints written in a formal language can represent structured properties, including non-Markovian ones.
3. While a constraint in a formal language requires some domain knowledge, if it is correct, it can accelerate the training phase.

#### Weakness
1. The paper cites some of the related works; however, it is unable to distinguish its contributions compared to the existing methods. In particular, some of the most relevant approaches are using linear temporal logic (LTL) formulas for reward shaping (Camacho et al., 2017a;b), using LTL constraints in RL (Hasanbeig et al., 2018), and shielding mechanisms (Jansen et al., 2018; Alshiekh et al., 2018). The paper cites these references but does not differentiate itself from them.
2. The experimental results of the paper are limited in terms of comparison with the existing methods. In particular, the only comparison is with baselines that do not use this automaton-based side information. However, since there exist many works with the capability of using such side information (some are mentioned in the previous point), these comparisons are essential for correctly evaluating the paper’s contribution and significance.

#### Recommended Decision
Given the paper's unclear contribution and lack of necessary comparison with the existing literature, I recommend rejecting the paper in its current form.

#### Supporting Arguments
1. The paper motivates the automaton-based constraints mostly for safety-critical applications. Nonetheless, the soft version of the constraints still lead to constraint violations and provide no safety guarantees.
2. In addition to citing the related work, the paper needs to clearly state the differences with the existing methods.
3. The writing requires somewhat considerable polishing. There are many typos, grammatical errors, and awkward phrases. Some notations are undefined, e.g., state space $S$ and action space $A$, $\tau$, operators in regular expressions, alphabets $n$ and $f$ in Figure 1(b), and the evaluation metric called accumulated cost regret. While the reader can probably infer some of them, the paper should be self-contained in this regard.
4. Figure 2 is not mentioned nor discussed in the paper. Some figures and tables are inserted far from where they are initially mentioned.
5. To properly answer the second question posed in Section 4.3 regarding the choice of hyperparameters, a criterion, strategy, or heuristic is required. Reporting the better hyperparameters for some instances, on its own, is not sufficient as an answer.

#### Questions
1. How is $t_v(q_t)$ estimated using rollouts, given that the framework and the simulations seem to be for the model-free setting?
2. Could you please explain the reasoning for the choice of $t_v^{baseline}$?

#### Additional Feedback for Improving the Paper
1. The following references are also highly related to this paper:
    - Zhu, He, et al. "An inductive synthesis framework for verifiable reinforcement learning." Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. 2019.
    - Fulton, Nathan, and André Platzer. "Verifiably safe off-model reinforcement learning." International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, Cham, 2019.
2. Compound adjectives require hyphens, e.g., “formal language constrained MDP” $\to$ “formal-language-constrained MDP”.
3. The clarity of the paragraphs on “Hard Constraints and Action Shaping” can be improved.
4. Please further motivate and explain why the constraints introduced in the simulation setting (except “proximity”) are required.
5. Please make the bibliography consistent in terms of details provided for each reference and the formatting. Also, the year of some references is repeated.

---
#### UPDATE
I thank the authors for their response. I am still concerned about the paper's novelty and contribution compared to the existing work as the differences seem minor. Also, the comparison with the approach by Camacho et al. (2017a;b) is not sufficient since different values of hyperparameter $\lambda$ may perform better. Given the authors' revisions and the added results, I have increased my score. However, I am still inclined toward rejecting the paper.

review_title: Unclear contribution and lack of contrast and comparison with relevant literature

final_score: rating: 6: Marginally above acceptance threshold
review_content: #### Summary
The authors propose to use formal languages, specifically DFAs, as a mechanism to specify constraints in a constrained MDP setting. This has the benefit of being able to rely on a large body of existing work on identification, safety verification, etc. The strategy relies on decomposing the constraint into a translation, recogniser & cost assignment function that connect the MDP to the DFA. The mentioned cost can then be combined with existing solution for solving cMDPs, such as reward shaping and Lagrangian methods. The key observation is that adding the recogniser state to the observations of the policy can result in significant gains in both performance and constraint satisfaction. A range of results are presented across different environment suites and hyper parameters.

#### Pros
- A novel design strategy for specifying constraints in constrained MDPs, which have become very popular again as means of learning safe controllers in e.g. robotics.
- Extensive evaluation on both discrete and continuous domains with various constraints, optimised hypers and multiple seeds.
- Results are largely in favour of the proposed method, esp. the benefit of adding the constraint state as an observation.
- Very clear and concise presentation (except minor comments, see below).

#### Cons
- The significance of this work is perhaps lower. While using the framework of formal languages to define constraints is a novel design strategy, the methods employed in this paper to resolve the resulting cMDP are not novel beyond adding the constraint state to the policy's observations. Any of the mentioned benefits of using formal languages, such as verification, are not actually investigated. I also would have liked to see more exploration of the benefit / shape of the dense cost function, as this now gets lost as a binary hyper parameter in the tables.
- The chosen constraints are not very interesting as they pertain largely to sequences of actions only (except for Safety Gym). Even for what would intuitively be state-dependent constraints such as paddle ball distance, the authors specify the translation function in such a way that it becomes an action-only constraint. This makes action shaping significantly easier.

#### Comments
- I couldn't find the definition of the cost assignment functions for the environments. Are they just binary?
- When a constraint gets violated, the DFA gets into an accepting state but it seems the episode does not get terminated. Does the DFA get reset in the next step?
- Using "reward shaping", "cost shaping" and "dense reward" can be confusing as they're often used interchangeably in other works.
- Figure 2 is not discussed in the text at all. Do the data points represent different values for $\lambda$?
- In Table 3 seaquest actuation and Table breakout dithering the wrong result is marked in bold (indicating best performance).

#### Conclusion
Overall, even though the significance is perhaps limited, I vote to borderline accept this paper due to the clarity and thorough evaluation.
review_title: Novel design strategy for constrained RL

final_score: rating: 6: Marginally above acceptance threshold
review_content: The paper builds on the constrained MDP framework (Altman, 1999), by considering the special-case where the cost functions are defined in terms of states from a parser of a formal language. In the experiments the work uses deterministic finite automata (DFA) but in principle other more expressive classes could be used. Using a formal language to specify constraints may simplify model checking (although this is left to future work). 

Pros:
  - Novel idea: not aware of any other work using formal languages for MDP constrained. Although as the paper notes, formal languages (especially those derived from LTL formulae) have been used elsewhere in RL.
  - Some encouraging empirical results: outperforms baseline in safety Gym, and is able to get higher episode return (!) as well as lower violations in some MuJoCo and Atari environments. (The effect of higher returns likely disappears with longer training or more powerful RL algorithms -- but the constraints being a useful inductive bias is nice.)
 
Cons:
  - While the paper shows that useful constraints *can* be expressed in formal languages, it does not demonstrate that formal languages are a useful way of expressing the constraints. All the constraints in section 4.1 could have been specified quite easily by other means -- e.g. directly writing a cost function in Python. There is vague discussion in section 1 & 5 about how formal languages could enable model checking or connect more generally with safety engineering, but I'm unconvinced.

   In particular, while formal languages might make for a specification that is amenable to verification, the neural network policy that is learned will still be difficult to verify -- especially when the properties depend on the (unknown) transition dynamics as they often do. Moreover, there is no reason why the constraints used in training need to be the same as those used for checking. Why not use a more expressive set of constraints in training, and then check the subset we can easily specify in a formal language?
  - The method requires hand-designing appropriate constraints. In the experiments these were different for each class of environments (safety Gym, MuJoCo, Atari) and in some cases were specific to the environment (e.g. "paddle-ball" and "danger-zone"). I'm sympathetic to this -- safe exploration must need some extra source of information besides just task reward -- but given this there needs to be some discussion or ideally evaluation of the usability of this procedure. It certainly seems intractable for a normal end-user (unlike methods based on e.g. learning from demonstrations or preference comparisons).

  Moreover, it seems quite challenging even for experienced RL practitioners to scale into complex environments. For example, the Atari constraints require having access to some high-level representation of the environment (paddle position, ball position). In real-world robotics, an analogue of this would require training a real-time object localization system.
  - The clarity of the submission could be improved in places. In particular, a clear up-front definition of the problem setting would be useful. Are the transition dynamics known? Unknown? Not known analytically but with oracle query access? Are the cost functions Markovian or not?
  - Hard action space seems to require a resettable environment or known transition dynamics, which weakens the results. RL usually assumes unknown transition dynamics: you should compare to baselines that also make use of this information for fairness, or at least make explicit this difference.

I find the paper borderline -- the idea is interesting and the results encouraging -- but the serious open questions re: whether formal languages are useful and, if they are, whether the approach is scalable make me vote against acceptance.

Some particular things I would suggest addressing in revisions:
  1. Greater justification of why formal languages. This is the most important point here and I'd consider increasing my vote if the usefulness of this approach was clarified. For example, can you cite any papers that use formal languages as specification to validate black-box systems (like RL policy + unknown MDP)?
  2. Discussion of how this method can scale, ideally with empirical validation. For example, could you actually learn a formal language specification (probably hard but impressive), or at least have a case-study where you apply this approach to something that doesn't have a nice low-dimensional state representation? Alternatively, if this method is limited to low-dimensional environments -- why use your method here and not a more classical control method?

Some clarifying questions I'd also appreciate if the authors could address during the discussion:
  1. How is $t_v$ computed? It seems underdefined -- it is a function of $q_t$ but the natural language definition given seems like it is in terms of constraint violations from rollouts of the current MDP state. As I understand it, many different states $s_t$ could lead to the same $q_t$ -- nor is making it a function of $s_t$ sufficient since the same $s_t$ could lead to different $q_t$ depending on previous states!

    Even if this issue is resolved (e.g. making it a function of both $s_t$ and $q_t$), computing it seems like it would require rollouts from $s_t$. This seems very expensive -- is my understanding correct? If so, could you report wall-clock times, or possibly train different algorithms for a fixed wall-clock time? Otherwise comparing algorithms for the same number of training timesteps seems unfair if the shaping effectively involves extra hidden environment interactions.
  2. Perhaps related to this confusion, you state in the hard action shaping section, that "before finalizing that choice, simulates stepping the DFA with the resulting token from the translation function". I am confused how one does this -- isn't the point we don't know the transition dynamics, so do not know the next MDP state we will end up in? If we do have a transition model, why don't we do planning instead to never take a sequence of actions that violate constraints?
  3. Any ideas why hard action shaping in both Training and Evaluation sometimes does worse than just during Training or just during Evaluation?

Some more detailed suggestions for improvements (no need to respond to these, they did not affect my decision in any significant way):
  - Page 2, “teacher advice”. “RL safety” is not a synonym for “safe exploration”, since there are other forms of safety related to RL (e.g. satisfying constraints in the final policy; optimizing a desirable objective, like user happiness, rather than a misaligned one, like short-term user engagement). 
  - Page 3, \delta: what is $A$? It is not defined anywhere that I can see – should this be $\Sigma$?
  - Page 3, $D_C$ is not a function since it takes only a single token but outputs the next state, which is dependent on the current state (not supplied). This also makes the constraints non-Markovian which seems like it should be emphasized more (although this is somewhat implicit in the “Constraint State Augmentation” section).
  - Page 3, Constraint State Augmentation: I think the dimensions should be integer ceiling not integer floor.
  - Page 3, Learned Dense Cost: perhaps make $t_{v}$ upper case since it's a random variable. This method also seems a bit ad-hoc – is there a theoretical justification for it? If not, how do other choices (e.g. a different exponent base to 1/2) change things?
  - Page 7-8: tables of numbers were a bit hard to digest. Consider turning some of them into figures, e.g. bar charts?
  - Table 5: a bold entry for “Training Only” in Breakout seems incorrect (for dithering, “Training and Evaluation” does better).
  - Discussion: “was never be empty”->”was never empty”. (“Best effort” also seems an odd phrase for this property.)

### Update: the author's revision have clarified many of the points of confusion above, and have largely addressed my concern re: the value of formal languages in this setting. I continue to be concerned about the scalability of this class of methods, but since it is a problem common to other work in this field, I do not want to hold this too much against the current submission. Given this I have increased my score to a 6. ###
review_title: Novel idea with encouraging results, concerns re: scalability and some clarity issues

Meta-review: The paper proposes formulating safety constraints as formal language constrains, as a step toward bridging the gap between ML and software engineering, and enabling safe exploration in RL.  The authors responded and improved the paper significantly during the rebuttal period. Despite that, the reviewers raise the question, and I agree, that the significance of the paper, especially the novelty of the method, do not meet ICLR standard. The future version of the paper should be developed more in terms of the novelty, evaluations, and related works. 

Decision: Reject