Formal Language Constrained Markov Decision Processes
Authors: Eleanor Quint
Dong Xu
Samuel W Flint
Stephen D Scott
Matthew Dwyer
Venue:  (2021)
Keywords: safe reinforcement learning
formal languages
constrained Markov decision process
safety gym
safety

Abstract: In order to satisfy safety conditions, an agent may be constrained from acting freely. A safe controller can be designed a priori if an environment is well understood, but not when learning is employed. In particular, reinforcement learned (RL) controllers require exploration, which can be hazardous in safety critical situations. We study the benefits of giving structure to the constraints of a constrained Markov decision process by specifying them in formal languages as a step towards using safety methods from software engineering and controller synthesis. We instantiate these constraints as finite automata to efficiently recognise constraint violations. Constraint states are then used to augment the underlying MDP state and to learn a dense cost function, easing the problem of quickly learning joint MDP/constraint dynamics. We empirically evaluate the effect of these methods on training a variety of RL algorithms over several constraints specified in Safety Gym, MuJoCo, and Atari environments.

Under review as a conference paper at ICLR 2021
FORMAL LANGUAGE CONSTRAINED MARKOV DECISION PROCESSES
Anonymous authors Paper under double-blind review
ABSTRACT
In order to satisfy safety conditions, agent may be constrained from acting freely. A safe controller can be designed a priori if an environment is well understood, but not when learning is employed. In partieular, reinforcement learned (RL) controllers require exploration, which can be hazardous in safety critical situations. We study the benefits of giving structure to the constraints of a constrained Markov decision process by specifying them in formal languages as a step towards using safety methods from software engineering and controller synthesis. We instantiate these constraints as finite automata to efficiently recognise constraint violations. Constraint states are then used to augment the underlying MDP state and to learn a dense cost function, easing the problem of quickly learning joint MDP/constraint dynamics. We empirically evaluate the effect of these methods on training a variety of RL algorithms over several constraints specified in Safety Gym, MuloCo, and Atari environments.
INTRODUCTION
The ability impose safety constraints on an agent is key to the deployment of reinforcement learning (RL) systems in real-world environments (Amodei et al. 2016). Controllers that are derived mathematically typically rely on a full a priori analysis of agent behavior remaining within a pre- defined envelope of safety in order to guarantee safe operation (Aréchiga & Krogh 2014). This approach restricts controllers to pre- pre-defined, analytical operational limits, but allows for verification of safety properties (Huth & K Kwiatkowskal 1997) and satisfaction of software contracts (Helm et al.) 1990), which enables their use as a component in larger systems. By contrast, RI controllers are free to learn control trajectories that better suit their tasks and goals; however, understanding and verifying their safety properties is challenging. A particular hazard of learning an RL controller is the requirement of exploration in unknown environment. It is desirable not only obey constraints in the final policy, but also throughout the exploration and learning process (Ray et al. 2019). .
The goal of safe operation decision process (CMDP) (Altman 1999), which adds to a Markov decision process (MDP) a cost signal similar the reward signal, and poses constrained optimization problem in which discounted reward is maximized while the total cost must remain below a pre-specified limit per constraint. We use this framework and propose specifying CMDP constraints in formal languages add useful structure based on expert knowledge, e.g., building sensitivity to proximity into constraints on object collision or converting a non- non-Markovian constraint into a Markovian one (De Giacomo et al. 2020
optimization objective is formalized by the constrained Markov
A significant advantage of specifying constraints with formal languages is that they already form well-developed basis for components of safety-critic systems (Huth & Kwiatkowska 1997 Clarke
et al. 2001 K wwitkkowska et al. 2002 Baier et al. 2003) and safety properties specified in formal languages can be verified priori (Kupterman et al. 2000, Bouajjani et al.) 1997). Moreover, the
recognition problem for many classes of formal languages imposes modest computational require- ments, making them suitable for efficient runtime verification (Chen & Roşu 2007). This allows for low-overhead incorporation of potentially complex constraints into RL training and deployment.
We propose (1) a method for posing formal language constraints defined over MDP trajectories as CMDP cost functions; (2) augmenting MDP state with constraint automaton state to more explicitly encourage learning of joint MDP/constraint dynamics; (3) a method for learning a dense cost function given sparse cost function from joint MDP/constraint dynamics; and (4) method based

---

Under review as a conference paper at ICLR 2021
MDP
MDP
nn.f
Ω1
Q2
43
Ospae Punk
7
Turcboo Te
Shaping
Furcitin To
start
qo
qu
tokzo
tokinn
Cue
Recogriaan Do
sude
Rocogsizar Do
q4
i
Q5
r
/6
(a)
(b)
Figure I: (a) Illustration of the formal language constraint framework operating through time. State carried forward through time by both the MDP and the recognizer, Dc. (b) No- No-hD-dith
constraint employed in the Atari and MuJoCo domains: (Err) (note, all unrepresented transitions return to (o).
constraint structure to dynamically modify the set of available actions to guarantee the prevention of constraint violations. We validate methods over variety of RL algorithms with standard constraints in Safety Gym and hand-buit buillt constraints in MuloCo and Atari environments.
The remainder of this work is organized follows. Section 2 presents related work in CMDPs, using expert advice in RL and safety, as well as formal languages in similar settings. Section deseribes definition of formal language-based cost function, well as how it's employed in state augmentation, cost shaping. and action shaping. Section details our experimental setup and results and finally, discussion of limitations and future work located in Section
RELATED WORK
Safety and CMDP Framework The CMDP framework doesn't prescribe the exact form of con- straints or how to satisfy the constrained optimization problem. [Chow et al. (2017) propose conditional value-at-risk of accumulated cost and chance constraints as the values to be constrained and use Lagrangian formulation to derive Bellman optimality condition. Dalal et al. (2018) use a different constraint for each MDP state and a safety layer that analytically solves linearized action correction formulation per state. Similarly, Pham et al. 2013 18) introduce a layer that corrects the output of policy to respect constraints on the dynamic of a robotic arm.
Teacher Advice A subset of work in safe exploration reward shaping mechanisms (Ng et al., 1999). Wiewiora et al. (2003) introduce a general method for incorporating arbitrary advice into the reward structure. [Saunders al. (2017) use human in the loop to learn an effective RL agent while minimizing cost accumulated over training. Camacho et al. (2017a use DFAs with static reward shaping attached to states to express non-Markovian rewards. We generalise this work with a learned shaping function in the case of dense soft constraints, and by generalising from reward shaping to other CMDP learning mechanisms. Similar to teacher advice shielding (Jansen et al., 2018 Alshickh et al. 2018), in which agent's 's actions are filtered through shield that blocks actions that would introduce an unsafe state (similar to hard constraints; |section 3). but typically requires MDP states to be enumerable and few enough that shield can be constructed efficiently.
expert advice with potential-basee -based
Formal Languages Formal languages and automata have been used before in RL for task specifi- cation or as task abstractions (options) in hierarchical reinforcement learning (carte et al.] (2018b)
Li al.
2017 Wen et al. 2017 Mousavi et al.) 2014). some cases, these automata were derived
from Linear Temporal Logic (LTL.) formulae, in others LTL or other formal language formulae have
been directly used to specify tasks ([carte et al. 2018ab. Littman et al. (0117) defines a modified
LTL designed for use in reinforcement learning. In robotics, LTL is used for task learning (Li et al.
2017), sometimes in conjunction with teacher demonstrations (Li et al. 2018). Zhu et al. 2019 and Fulton & Platzer (2019) both study the of formal languages for safe RL, though each makes assumptions about prior knowledge of the environment dynamics. Hasanbeig et al. (2018) and Hasanbeig et al. (2020) learn a product MDP with safety constraint specified in formal language,
2

---

Under review as a conference paper at ICLR 2021
but require knowledge of MDP structure and don't scale to large MDPs. Hahn al. (2019) uses an omega-regular language to specify an objective and constructs product MDP to ensure the objective is reached almost surely, but requires large reward shaping which prevents learning when used for constraint rather than objective.
FORMAL LANGUAGE CONSTRAINED MDPS
The constrained Markov decision process (CMDP) Altmnn 1999) extends the Markov decision process (Sutton & Barto 2018) incorporate constraints. The difference is additional set of cost and set of cost limits d, E R. Then, the constrained optimization problem is arg max, (T) s.t. Jc, (TT) S di, I,..., where (TT return-based objective, e.g., finite horizon discounted return defined Jr (T) = Er Eetr 2're] and Jo, is a cost-based constraint function defined similarly, replacing r. with Ci,
functions Q: 5 x x S
We propose formal language constrained MDPs (FLCMDPs) as a subset of CMDPs in which each constraint C C (S A x S)* is defined by set of prohibited trajectories. (Subscript is suppressed from this point without loss of generality). Because C' is defined by a formal language, it can be recognized efficiently by an automaton, which we use to construct the cost function. We define three functions for interacting with the constraint automaton: a translation function Tc: (SxAxS) + Ec that converts MDP transitions into symbol in the recognizer's s input language, a recognizer function Do Qe Ec + Qc that steps the recognizer automaton using its current state and the input symbol and returns its next state, and finally a cost assignment Ge : Qc + I that assigns a real- real-valued cost to each recognizer state. The composition of these three functions forms CMDP cost function defined c= Ge o De o Tc : (S x X 5) x Q. - IR, which requires constraint state Q. to be tracked along with the MDP state, S. The interaction of these functions with the underlying MDP framework is illustrated in Figure 1(a), where the constraint uses the MDP state and action at time t to calculate the cost signal at time and, if action shaping being employed as discussed below, influence the action at time t + 1. We note that this construction does not require knowledge of the MDP transition probabilities and further, its complexity independent of the size of the MDP, which allows it to scale to large, challenging environments.
Translation Function Te The translation function accepts as input the MDP state and action at each time step, and outputs a token in the discrete, finite language of the associated recognizer. This allows the recognizer automaton to be defined in a small, discrete language, rather than over unwieldy and potentially non-discrete MDP transitions. Further, freedom in choice of input language allows for flexible design of the constraint automaton to encode the desired inductive bias, and thus more meaningful structured states.
Recognizer Function De Each constraint is instantiated with a finite automaton recognizer that decides whether a trajectory is in the constraint set. The only necessary assumption about the recognizer is that it defines some meaningful state that may be used for learning the constraint dynamics. Our implementation uses deterministic finite automaton (DFA) the recognizer for each constraint, defined as (Q, Σ, 5, go: F), where Q is the set of the DFA's states, Σ is the alphabet over which the constraint defined, ö Q x Σ + Q is the transition function, qo Q is the start state, and F C Q is the set of accepting states that represent constraint violations. The DFA is set to its initial state at the start of each episode and is advanced at each time step with the token output by the translation layer. Although our experiments use DFAs as a relatively simple recognizer, the framework can be easily modified to work with automata that encode richer formal languages like pushdown automata or hybrid automata.
Constraint State Augmentation In order to more efficiently learn constraint dynamics, the MDP state is augmented with a one-hot representation of the recognizer state q:. To preserve the Markov property of the underlying MDP, state augmentation should contain sufficient information about the recognizer state and, if it is stateful, the translation function. To enhance performance, the one-hot state is embedded to [log, (IQ] dimensions before being input into any network and the embedding is learned with gradients backpropagated through the full network.
3

---

Under review as a conference paper at ICLR 2021
Cost Assignment Function The cost assignment function Ge assigns real-valued cost to each state of the recognizer. This cost can be used in optimization to enforce the constraint with a Lagrangian-derived objective penalty, or via reward shaping, which updates the reward function to Pt Ac, where X is a scaling coeffficient.
Cost assignments are frequently sparse, where Gc is only non-zero at accepting states that recognize a constraint violation. This poses a learning problem for optimization based methods that use reward shaping or an objective penalty to solve the CMDP. A goal of constrained RL is to minimize accumulated constraint violations over training but, to ensure that the frequency of violations is small, the optimization penalty can be large relative to the reward signal. This can lead to a situation in which an unnecessarily conservative policy is adopted early in training, slowing exploration. We next propose method for learning a dense cost function that takes advantage of the structure of the constraint automaton to more quickly learn constraint dynamics and avoid unnecessarily conservative behavior.
Learned Dense Cost The goal of learning a dense cost is not to change the optimality or near- optimality of a policy with respect to the constrained learning problem. Thus, use the form of potential-base based shaping: F()--1, at sr) = > ) - (s{-1),, where & is a potential function (see Ng et al. (1999) for details). This is added as a shaping term the sparse cost to get the dense cost Gc-9t-1, 4t) = Gg())) + ( (q:) - $ (()-1)) where / scales the added dense cost relative to the sparse cost, and @ a function of the recognizer state rather than the MDP state, which requires 8:-2 and dx-2 as additional inputs to calculate -: Generally, if the value of & increases as the automaton state is nearer to a violation, then the added shaping terms add cost for moving nearer to a constraint violation and refund cost for backing away from potential violation.
In our experiments, the potential कTt (4c) is defined using (4)), which is a random variable defined as the number of steps between visiting recognizer state qe and accepting recognizer state. This variable's ' distribution is based on π and the MDP's transition function. Its value is small a violation is expected occur soon after reaching qi and vice-versa. We then define the potential function as TT (q:) (2) (E,, (T. )
which ensures that its value is always in [0, 1] and rises exponentially as the expected time to a violation becomes smaller. If the expected time to next violation much larger than the provided baseline, lbaseline, then the potential value becomes small, as shaping is unnecessary in safe states. The expected value of (q:) over trajectories may be calculated as a Monte Carlo estimate from rollouts by counting the number of steps between each visit to g, and the next constraint violation. Each T,, is tracked with an exponential moving average and is updated between episodes to ensure that it's stationary each rollout. We set phoseline to be the ratio of estimated or exact length of an episode and the constraint limit d;, but find empirically that the the method is resilient to the exact choice.
Hard Constraints and Action Shaping When safety constraints are strict, i.e., when the limit on the number of constraint violations d is zero, the set of available actions is reduced ensure a violation cannot occur. If a constraint isn't 't fully state-dependent (i.e., there is always an action choice that avoids violation), then action shaping can guarantee that a constraint never violated. Otherwise, knowledge of which actions lead to future violating trajectories requires knowledge of the underlying MDP dynamics, which is possible by learning a model that converts state constraints into state-conditional action constraints as in Dalal et al. (2018).
Our implementation of hard constraints initially allows the agent to freely choose its action, but before finalizing that choice, simulates stepping the DFA with the resulting token from the translation function and, if that lookahead step would move it into a violating state, it switches to the next best choice until a non-violating action is found. For the constraints in our experiments, it is always possible to choose a non- non-violating action. A known safe fallback policy can be employed in the case when episode cannot be terminated. Action shaping can be applied during training or deployment, as opposed to reward shaping, which is only applied during training. We experiment with applying action shaping only during training, only during evaluation, or in both training and evaluation.
4

---

Under review as a conference paper at ICLR 2021
4 EXPERIMENTAL EVALUATION
4.1 CONSTRAINTS
We evaluated FLCMDPs on four families of constraints, which we define with regular expressions. The cost function defined by each constraint is binary, unless we use dense cost shaping.
No-dithering: A no-dithering constraint prohibits movements in small, tight patterns that cover very small areas. In one dimension, we define dithering as actions are taken to move left, right, left, and right in order or the opposite, i.e., : (rr) E)e. The automaton encoding this constraint is depicted in Figure lb). In environments with two-dimensional action spaces, such as Atari Seaquest, we generalize this to vertical and diagonal moves and constrains actions that take the agent back to where it started in at most four step In MuJoCo, constraints are applied per joint and the translation function maps negative and positive- positive-valued actions to 'E" and 'r', respectively.
No-overactuating: A no-overactuating constraint prohibits repeated movements in the same direction over long period of time. In Atari environments, this forbids moving in the same direction four times in a row, i.e.. (E* "Ur r²). In two dimensions, this is extended to include moving vertically: : "IAA U R U U D*). Each of the left (L), right (R), up (U) and down (D) tokens is produced by the translation function from the primary direction it's named after or diagonal moves that contain the primary direction, e.g., L = f t+u U &+d, where "C+u" is the atomic left-up diagonal action. In MuJoCo environments, overactuation is modelled as occurring when the sum of the magnitudes of joint actuations exceeds a threshold. This requires the translation function discretize the magnitude in order for DFA to calculate an approximate sum. The MDP state-based version is "dynamic actuation", which sets the threshold dynamically based on a discretized distance from the goal.
The proximity constraint, used in Safety Gym, encodes the distance to a collision with any of the variety of hazards found in its environments. The translation function uses the max value over all the hazard lidars, which have higher value as a hazard comes closer, and discretizes it into one of ten values. The constraint is defined as being violated if the agent contacts the hazard, which is identical to the constraint defined in the Safety Gym environments and described in Ray et al. (2019).
Proximity:
Domain-specific: In addition to the previously described simple constraints, we define hand-built constraints for the Breakout and Space Invaders Atari environments. These constraints are designed to mimic specific human strategies in each environment for avoiding taking actions that end the episode. In Atari Breakout, we define the "paddle-ball" constraint, which limits the allowed horizontal distance between the ball and the center of the paddle. In Atari Space Invaders, we define the "danger zone" constraint, which puts floor on the the allowed distance between the player's ship and the bullets fired by enemies. We provide more details of each constraint in Appendix B
4.2 ENVIRONMENTS
In Safety Gym, the Spinning Up implementation of PPO with Lagrangian optimization penalization was employed, with hyperparameters as chosen identically to Ray et al. (209)). We modified each network concatenate the constraint state augmentation with the input and used d = 25 for the expected cost limit. All safety requirements are accounted for in a single constraint and we report the constraint violations accounted for in the Safety Gym environments rather than as reported by the finite automaton (though these are identical when not using cost shaping). Each environment, which randomly re-arranged each episode, is made up of a pairing of a robot and a task. The robots are Point, which turns and moves, and Car, which is wheeled with differential drive control. The tasks are Goal, which requires moving into a goal area, Button, which requires pressing a series of buttons, and Push, which requires moving box into a goal area. More details can be found in Ray et al. 2019))
In Atari environments (Bellemare et al. 2013), we modified the DQN implemented in OpenAl Baselines (Dhariwal et al. 2017) by appending the state augmentation to the output of its final convolutional layer. Reward shaping was used for soft constraint enforcement with the penalty fixed at one of {0, 0.0001 0.0025. -0.05,- -0.01}, and each agent trained for 10M steps before collecting data from an evaluation phase of 100K steps for 15 or more train/eval seed pairs for each hyperparameter combination. For MuJoCo environments (Brockman al. 2016), we trained the
'The regex describing this constraint is included in Appendix D
5

---

Under review as a conference paper at ICLR 2021
Table 1: Metrics averaged over the last 25 episodes of training in Safety Gym environments with PPO- Lagrangian methods, normalized relative to unconstrained PPO metrics. Cost rate is the accumulated cost regret over the entirety of training.
FLCMDP State Augmented
Baseline
Environment
Return
Violation
Cost Rate
Return
Violation
Cost Rate
Point-Goall
0.750
0.427
0.281
0.918
0.925
0.503
Point-Goal2
0.195
0.083
0.078
0.021
0.062
0.155
Point-Buttoni
0.252
0.129
0.128
0.343
0.296
0.218
0.251
0.130
0.141
0.166
0.255
0.118
Point-Pushl 0.549
0.042
0.061
0.692
0.496
0.543
Point-Push2 0.938
0.173
0.148
0.670
0.295
0.258
Car-Goal
0.825
0.295
0.284
0.803
0.475
0.445
Goal2
0,005
0.011
0.079
0.021
0.046
0.108
C
0.022
0.083
0.071
0.018
0.039
0.118
Car-Button2
0.031
0.147
0.076
0.009
0.009
0.078
Car-Pushl
0.737
0.032
0.069
0.882
0.387
0.420
Car-Push2
0.256
0.086
0.124
0.025
0.115
0.202
conatiial and sprrecct
sonalbo
comminer: cort
conteer taat
Figure 2: Performaanc/conformmacc curves in selected Safety Gym environments with Pareto frontiers plotted per reward shaping method. We observe that using state augmentation (green) consistently outperforms the baseline (blue) at all levels of reward shaping, which are anti-correlated with episodic cost and episodic return. The use of cost shaping (purple) produces gains in return at given amount of cost only at small reward shaping values correlating to high return and cost. Consequently, the combination of state augmentation and cost shaping inherits this behavior of being more effectiveness when cost/return are higher. The full set of plots is included in Appendix C
Baselines PPO agent (Schulman et al. 2017 with dense constraints and the state augmentation concatenated to the input MDP observation. Reward shaping similar to Atari was employed for constraint enforcement. Atari and MuJoCo environments do not have constraints built in, so we report the number of constraint violations per episode from the custom constraints and minimize them without a specific goal value.
4.3 RESULTS
We experiment with our methods to evaluate the usefulness of formal language constraints in optimizing three objectives. In the final policy output by the training process, it is desirable to simultancously maximize return per episode and minimize constraint violations per episode, or keep them below the specified limit. The third objective is minimize accumulated cost regret

---

Under review as a conference paper at ICLR 2021
Table 2: Atari reward shaping with state augmentation, choosing hyperparameters that minimize constraint violations per episode. "Dense" refers to whether the dense cost term was used and "reward shaping" refers to the fixed reward shaping coefficient X.
FLCMDP State Angmenttd
Bastine
Reward Shaping
Mean Episode Reward
Mean
Mian
Mran Episode
Mean
Mron
Environment
Construint
Dense
Step Rewurd
Viols100 steps
Reward
Step Reward
Viebs/100 steps
octuation
Faise
- 11001
297.12 = 8.07
0,15 1. 0.0039
0.45 = 0.00067
272.19 2: 43.12
0.14 0.01
13.59 a: 0.025
Breakout
dithering
Filse
- 0.001
263.57 11.14
I.15 + 0.0068
0.INE 8.4c-166
272.19
43,12
0.14 0.01
0.12 + 0.001
puddle ball
True
0.0022
314.79
15.09
1.37 + 0.0056
6.15 = 0,0831
272.19
43.12
0.14 0.01
13.40 0.022
Sesguest
actutiin
dichering
False
False
0.011
1858.55
1608.65
478.56
41:25
0.75 1 0.013
0.76 + 0.18
0.081 0.001
2.71 0,0066
2250,13
2250.13+
647.92
647.92
0.96 0.21
0.96 0.21
9.74 0.017
1.61 0.007
actuation daugerzone
False
598.78
98
0.63 0.033
5.39 L 0.017
604.86
44.86
0.62 0.04
10.58 0.011
Spucelaaades
0.65 0.017
0.00
604
44.86
0.04
0,00 0U00
dithoring
20.25
0.63 0.021
604,86
44.86
0.53
Table 3: Atari reward shaping with state augmentation, choosing hyperparameters that maximize cumulative reward per episode. "Dense" refers to whether the dense cost term was used and "reward shaping" refers to the fixed reward shaping coefficient X.
FLCMDP State Augmented
Buseline
Mean Step Reward
Meun
Knvironment
Constraint
Dense
Shaping
Episode Reward
Step Reward
Viots100 Steps
Epiiode
Reward
Viote/000 Steps
actustion
False
0.001
297.12
0.45 1,000667
272. 19
0.025
Breakoot
dibering
True
0.005
302-24
43.81
0.14 0.02
0.11 0.001
272.00 19
43.12
0.14 0.01
0.12 0.001
paddle ball
Tree
0.1025
314.79
15.09
0.17 0.0056
6.15 0,0031
272.19 1: 43.12
0.14 2: 0.01
13:40 0.022
Sengues
actunioon dithering
True
False
0.IK225
0.001
2539.54
1997 91 539.75 75
442.02
0:93 = 0.11
0.86 0.23
4.43 =: 0.016
1.58 + 0.011
2250.1 + 647.92
2250.13 + 647.92
0.96 = 0.21
0.96 + 0.21
9.74 =: 0.017
1.61 + 0.007
actustion
False
0.005
646.99
50.55
0.64 0.04
20 +: 0.0053
604 86 + 44.86
0.62 + 0.04
10.88 :: 0.011
Spucelavadors
Gangerzone
False
0.0001
687.37
16.75
0.63 0.01
0.00 1: 0.00
604.36
1: 44.86
0.62 1: 0.04
0,00 1: 0.00
dithering
False
0.001
640.35
25.94
0.67 0,09
0.17 + 11,00227
684 + 44.86
0.62 + 0.04
0,53 0.0004
over the course of training. To examine the proposed methods, we investigate two questions. First, what effect do the proposed methods have on accumulated regret? In Section 4.3.1 we compare the proposed methods against baseline when combined with PPO using Lagrangian approach in Safety Gym (Ray et al.) 2019). Second, how should hyperparameters be chosen to minimize or maximize each objective respectively? In Section 2.3.2 examine which hyperparameter choices worked well in various Atari and MuJoCo environments using reward shaping. Finally, in Section 13. we see what effect enforcing zero constraint violations with action shaping has on Atari environments.
4.3.1 LAGRANGIAN RESULTS AND ACCUMULATED COST
Table compares PPO with Lagrangian constraint enforcement with and without constraint state augmentation. The clearest trend is in the reduction of the cost rate, which measures accumulated cost regret, often by between almost one half and order of magnitude. This results from the inclusion of the helpful inductive bias provided by the constraint structure. This result not surprising, but does quantify the magnitude of the benefit that low-overhead method like formal language constraints can have. Qualitatively, we noted that the earliest steps of training had decreased performance generally as the embedding of the constraint state was being learned, but quickly surpassed bascline performance once the updates of the embedded representation became small.
Ray et al. 2019) says that algorithm A dominates Ag when they are evaluated under the same conditions, the cost and return of A₁ are at least as good as that of A2, and at least one of cost and return is strictly better for A₁. By this definition, the state augmented approach strictly dominates the baseline in 6 of 12 environments, while coming close in most of the rest. Specifically, we also note that state augmentation allowed significant step to be taken in closing the gap between unconstrained PPO return and PPO-Lagrangee in the Point-Goal2 and Car-Push2 environments, with increases of roughly an order of magnitude in each.
4.3.2 REWARD SHAPING RESULTS AND SENSITIVITY TO REWARD SHAPING
The most basic function of the proposed framework is to reduce constraint violations. Figure 2 shows performaace//ooorrmance curves in Safety Gym where reward shaping was varied in (0.20. -0.005, -0.1, -0.1, The curves show a meaningful trade-off between the objectives episodic return and cost, which is improved by the use of proposed methods. Table presentts the mean and standard deviation of violations per 100 evaluation steps, episode length. and episode reward for reward shaping-enforeed constraints with the choice of hyperparameters that produced
7

---

Under review as a conference paper at ICLR 2021
Table 4: Mean per-episode MuloCo rewards and violations with soft dense constraints and constraint state augmentation. Top row displays the reward shaping coefficient X.
8:0 0000
010 68
13 60 200
Table 5: Atari results with hard constraints, choosing hyperparameters which maximize reward when applying action shaping in training and evaluation, only in training, or only in evaluation.
Training and Evaluation
Training Only
Evalantion Only
Mean Episode Reward
Mean Viols/100 Steps
Mean
Mean
Mean
Mean
Environment
Constraint
Episode Reward
Viols100 Steps
Episode Reward
Viols/100 Steps
actuation
302. 302.00- +: 20.75
0.0 + 0.0
320.31 1: 6.09
0.092 + 0,00026
311.91 1: 13.80
0.0 1: 0.0
Breakout
ditbering
295.31 4: 29.07
0.0 4: 0.0
276.72 15.50
0.0073 +: 3.1e-05
275.25 + 12:67
0.0 0.0
paddle
218.14
281.77 11.03
0.00029
229.00
0.0
Seaquest
actuation
dithering
1926.97 + 430.24
2284.78
15.45
0.0 + +.00
0.0 + 0.0
1899. 7X 502 27
2256.06 + 30.53
0.01 # 2.8e-05
8.30 0.043
1895.77 + 366,79
2267.53 23 .4
0.0 + 0.0
0.0 + 0.0
actuation
586.66
582,79 51.47
0.012
Spacelmaderss
dangerzone
613.6] +: 24.05
733.52 16.95
+: D.O
613.82 +: 27.52
+:
ditbering
627.40 1. 31.43
0.0 0.0
624.33 4: 25.27
0.008 +: 3c-05
626.59 1: 31.04
0.0 2: 0.0
the minimum violations for each environment//consraaint pair evaluation. We note that the highest value of reward shaping available is generally the best choice for minimizing constraint violations, which were often reduced by an order of magnitude or more from the bascline. Minimizing constraint violations has small deleterious effect mean episode reward, but because mean reward per step didn't decrease, episodes were shorter as a result of constraint enforcement.
In addition minimizing constraint violations, we found that the application of soft constraints can also increase reward per episode. Table 3 presents results for soft constraints with the choice of hyperparameters that produced the maximum reward in each environment/constraiitt pair. In this case, lower reward shaping values perform best. The hyperparameter values that minimized constraint violations with the Breakout actuation and paddle ball constraints also maximized reward, implying that the objectives were correlated under those constraints. Table A presents results for soft constraints with constraint state augmentation in three MuJoCo environments. We find, similar to Atari, that there is one value of reward shaping that is most effective in each environment/constraiit pair and that reward degrades smoothly as is shifted from the optimal value.
4.3.3 HARD ACTION SHAPING RESULTS
Table presents results for hard constraints with the hyperparameters that produced the maximum return for each environment//onstrraln pair. Results for cases where hard action shaping was only applied during training or only applied during evaluation are presented well. There is a slight trend indicating that using action shaping at train time in addition to evaluation increases performance. For those constraints that are qualitatively observed to constrain adaptive behavior, performance rises when using hard shaping only in training, at the cost of allowing constraint violations.
5 DISCUSSION
The ability to specify MDP constraints in formal languages opens the possibility for using model checking (Kupferman et al. 2000 Bouajjani al. 1997), agnostic to the choice of learning algorithm, to verify properties of a safety constraint. Formal language constraints might be learned from exploration, given pre-specified safety objective, and, because of their explicitness, used without complication for downstream applications or verification. This makes formal language constraints particularly useful in multi-component, contract-based software systems (Meyer 1992), where one or more components is learned using the MDP formalism.
Experiments with more complex constraints are necessary to explore yet unaddressed challenges, the primary challenge being that the constraints used with action shaping in this work ensured the allowed set of actions was never empty. If this is not the case, lookahead might be required to guarantee zero constraint violations. Further, the tested hard constraints were only used with DQN, which provides ranked choice over discrete actions. Future work might investigate how to choose optimal actions which are not the first choice in the absence of ranked choice.
8

---

Under review as a conference paper at ICLR 2021
REFERENCES
Mohammed Alshickh, Roderick Bloem, Rüdiger Ehlers, Bettina Könighofer, Scott Nickum, and Ufuk Topeu. Safe reinforcement learning via shielding. In Proceedings of AAAI 18, pp. 2669-2678, 2018.
Eitan Altman. Constrained Markov decision processes, volume 7. CRC Press, 1999.
Dario Amodei, Chris Olah, Jacob Steinhardt, Paul Christiano, John Schulman, and Dan Mané. Concrete problems in AI safety. arXiv preprint arXiv:1606.06500 2016.
N. Aréchiga and B. Krogh. Using verified control envelopes for safe controller design. 2014 American Control Conference, pp. 2918 29233,,,, June 2014.
Christel Baier, Boudewijn Haverkort, Holger Hermanns, and Joost-Pietes Pieter Katoen. Model-checking algorithmss for continuous-tima Markov chains. IEEE Transactions on software engineering, (6): 524-541, 2003.
M. G. Bellemare, Y. Naddaf, J. Veness, and M. Bowling. The arcade learning environment: An evaluation platform for general agents. Journal of Artificial Intelligence Research, 47:253-279, jun 2013.
Ahmed Bouajjani, Javier Esparza, and Oded Maler. Reachability analysis of pushdown automata: Application to model-checking. In International Conference on Concurrency Theory, pp. 135-150. Springer, 1997.
Greg Brockman, Vicki Cheung, Ludwig Pettersson, Jonas Schneider, John Schulman, Jie Tang, and Wojeiech Zaremba. OpenAl gym. arXiv preprint arXiv:1606.0115500 005400000011,.... 2016.
Alberto Camacho, Oscar Chen, Scott Sanner, and Sheila Mcllraith. Non-markoving rewards expressed in LTL: guiding search via reward shaping. In Proceedings of the Tenth International Symposium on Combinatorial Search, SOCS 20/7, 16-17 June 2017, Pittsburgh, Pennsylvania, USA., pp. 169-160, 2017a.
Alberto Camacho, Oscar Chen, Scott Sanner, and Sheila Mcllraith. Decision makinn with non non- markovakovinn rewards: From LTL to automata- based reward shaping. In Proceedings of the Milti-disciplinary Conference on Reinforcement Learning and Decision Making (RLDM), pp- 279-283, 2017b.
Feng Chen and Grigore Roşu. Mop: An efficient and generic runtime verification framework. In Proceedings of the 22Nd Annual ACM SIGPLAN Conference on Object-oriented Programming Systems and Applications, OOPSLA '07, 2007.
Yinlam Chow, Mohammad Ghavamzadeh, Lucas Janson, and Marco Pavone. Risk-constrained reinforcement learning with percentile risk criteria. The Journal of Machine Learning Research, 18(1):6070-6120, 2017.
Edmund M. Clarke, Oma Grumberg, and Doron A. Peled. Model checking. MIT Press, 2001. ISBN 978-0-262-03270-44
Gal Dalal, Krishnamurthy Dvijotham, Matej Vecerik, Todd Hester, Cosmin Paduraru, and Yuval Tassa. Safe exploration in continuous action spaces. arXiv preprint wrXiv:1801.08555 2018.
Giuseppe De Giacomo, Marco Favorito, Luca locchi, Fabio Patrizi, and Alessandro Ronca. Temporal logic monitoring rewards via transducers. 2020.
Prafulla Dhariwal, Christopher Hesse, Oleg Klimov, Alex Nichol, Matthias Plappert, Alec Radford,
John Schulman, Szymon Sidor, Yuhuai Wu, and Peter Zhokhov. OpenAl baselines. https 2017.
//qithub.. wwtpc/ppeaa//aseee..i..co
Nathan Fulton and André Platzer. Verifiably safe off- model reinforcement learning. In International Conference on Tools and Algorithmss for the Construction and Analysis of Systems, pp. 413-430. Springer, 2019.

---

Under review as a conference paper at ICLR 2021
Emst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, and Dominik Wojtczak. Omega-regular objectives in model-free reinforcement learning. International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 395-3995522 Springer, 2019.
Mohammadhosein Hasanbeig. A. Abate, and D. Kroening. Logically-correct reinforcement learning. ArXiv, 0ttps/880.,0099 2018.
Mohammadhosein Hasanbeig, Alessandro Abate, and Daniel Kroening. Cautious reinforcement learning with logical constraints. arXiv preprint arXiv:2002. 12/56, 2020.
Richard Helm, Ian M Holland, and Dipayan Gangopadhyay. Contracts: specifying behavioral compositions in object- systems. ACM Sigplan Notices, 25(10):169-180, 1990.
Michael Huth and Marta Z. Kwiatkowska. Quantitative analysis and model checking. In Proceedings, 12th Annual IEFE Symposium Logic in Computer Science, Warsaw, Poland, June 29 July 2, 1997, pp. 111-122, 1997.
Rodrigo Toro Icarte, Toryn Q. Klassen, Richard Anthony Valenzano, and Sheila A. Mcllraith. Teaching multiple tasks an RL agent using LTL. In Proceedings of the 17th International Conference on Autonomous Agents and MultiAgent Systems, AAMAS 2018, Stockholm, Sweden, July 10-15, 2018, pp. 452 461, 20.
Rodrigo Toro Icarte, Toryn Q Klassen, Richard Anthony Valenzano, and Sheila A. Mcllraith. Using reward machines for high-level task specification and decomposition in reinforcement learning. Proceedings of the 35th International Conference on Machine Learning, ICML 2018, Stockholmsmüsssan, Stockholm, Sweden, July 10-15, 2018, pp. 2112-2121, 20.
Nils Jansen, Bettina Könighofer, Sebastian Junges, and Roderick Bloem. Shielded decision-making in mdps arXiv preprini arXiv: 00000000000666 2018.
Oma Kupferman, Moshe Y Vardi, and Pierre Wolper. An automataa-hherretic approach to branching- time model checking. Journal of the ACM (JACM), 47(2):312-36 -60, 2000.
Marta Kwiatkowska, Gethin Norman, and David Parker. Prism: Probabilistic symbolic model checker. In International Conference on Modelling Techniques and Tools for Computer Performance Evaluation, pp. 200-204. Springer, 2002.
Xiao Li, Cristian loan Vasile, and Calin Belta. Reinforcement learning with temporal logic rewards. In 2017 IEEE/RSJ International Conference on Intelligent Robots and Systems, IROS 2017, Vancouver, BC, Canada, September 24-28, 2017, pp. 3834-3839, 2017.
Xiao Li, Yao Ma, and Calin Belta. Automata guided reinforcement learning with demonstrations. CoRR, abs/1809.00 bbss/889900605, 2018
Michael L. Littman, Ufuk Topcu, Jie Fu, Charles Lee Isbell Jr., Min Wen, and James MacGlashan. 2017.
Enviroomenn-indeeeeddenn task specifications via GLTTL CoRR,
Bertrand Meyer. Applying 'design by contract'. Computer, 25(10):40 51, 1992.
Seyed Sajad Mousavi, Behzad Ghazanfari, Nasser Mozayani, and Mohammad Reza Jahed-Motlagh. Automatic abstraction controller in reinforcement learning agent via automata. Appl. Soft Comput., 25:1 18-118 2014.
Andrew Y. Ng. Daishi Harada, and Stuart J. Russell. Policy invariance under reward transformations: Theory and application to reward shaping. In Proceedings of the Sixteenth International Conference on Machine Learning (ICML 1999), Bled, Slovenia, June 27 30, 1999, pp. 278-287, 1999.
Tu-Hoa Pham, Giovanni De Magistris, and Ryuki Tachibana. Optlayer-practical constrained opti- mization for deep reinforcement learning in the real world. In 2018 IEEE International Conference on Robotics and Automation (ICRA), pp. 6236-6243. IEEE, 2018
Alex Ray, Joshua Achiam, and Dario Amodei. Benchmarking safe exploration in deep reinforcement learning. arXiv preprint 1910v01900.0/1 2019.
10

---

Under review as a conference paper at ICLR 2021
William Saunders, Girish Sastry, Andreas Stuhlmueller, and Owain Evans. Trial without enror: Towards safe reinforcement learning via human intervention. arXiv preprint arXiv.170..0517. 2017.
John Schulman, Filip Wolski, Prafulla Dhariwal, Alec Radford, and Oleg Klimov. Proximal policy optimization algorithms. arXiv preprint arXiv:1707.06347 2017.
Richard S Sutton and Andrew G Barto. Reinforcement learning: An introduction. MIT press, 2018.
Stéfan van der Walt, Johannes L. Schönberger, Juan Nunez-Iglesias, François Boulogne, Joshua D. Warner, Neil Yager, Emmanuelle Gouillart, Tony Yu, and the scikit-image contributors. scikit- image: image processing in Python. PeerJ, 2:e453, 6 2014. ISSN 2167-8359. doi: 10.7717/peerj. 453. URL http::tt/t/oooorreeee. www.:/.....1111000......... 7717 www.:/07111/pp...... p.ppppeeer.....
Min Wen, Ivan Papusha, and Ufuk Topcu. Learning from demonstrations with high-level side information. In Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017, Melbourne, Australia, August 19-25, 2017, pp. 3055-3061, 2017.
Eric Wiewiora, Garrison W Cottrell, and Charles Elkan. Principled methods for advising reinforce- ment learning agents. In Proceedings of the 20th International Conference on Machine Learning (ICML-03), pp. 792-799, 2003.
He Zhu, Zikang Xiong, Stephen Magill, and Suresh Jagannathan. An inductive synthesis framework for verifiable reinforcement learning. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 686-701, 2019.


Reviews:
[{"review_id": "oSiG5pIO594", "reviewer": "AnonReviewer2", "summary": "", "questions": "", "limitations": "", "rating": 6, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "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": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "#### Summary\nThe 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.\n\n#### Pros\n- 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.\n- Extensive evaluation on both discrete and continuous domains with various constraints, optimised hypers and multiple seeds.\n- Results are largely in favour of the proposed method, esp. the benefit of adding the constraint state as an observation.\n- Very clear and concise presentation (except minor comments, see below).\n\n#### Cons\n- 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.\n- 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.\n\n#### Comments\n- I couldn't find the definition of the cost assignment functions for the environments. Are they just binary?\n- 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?\n- Using \"reward shaping\", \"cost shaping\" and \"dense reward\" can be confusing as they're often used interchangeably in other works.\n- Figure 2 is not discussed in the text at all. Do the data points represent different values for $\\lambda$?\n- In Table 3 seaquest actuation and Table breakout dithering the wrong result is marked in bold (indicating best performance).\n\n#### Conclusion\nOverall, even though the significance is perhaps limited, I vote to borderline accept this paper due to the clarity and thorough evaluation.", "extra_scores": {}, "extra_text": {}}, {"review_id": "LacrlxL88Hi", "reviewer": "AnonReviewer3", "summary": "", "questions": "", "limitations": "", "rating": 5, "confidence": 5, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "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": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "#### Summary\nThe 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.\n\n#### Strength\n1. Constrained RL is certainly an important research area, having a variety of applications such as safety-critical problems.\n2. The constraints written in a formal language can represent structured properties, including non-Markovian ones.\n3. While a constraint in a formal language requires some domain knowledge, if it is correct, it can accelerate the training phase.\n\n#### Weakness\n1. 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.\n2. 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.\n\n#### Recommended Decision\nGiven the paper's unclear contribution and lack of necessary comparison with the existing literature, I recommend rejecting the paper in its current form.\n\n#### Supporting Arguments\n1. 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.\n2. In addition to citing the related work, the paper needs to clearly state the differences with the existing methods.\n3. 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.\n4. Figure 2 is not mentioned nor discussed in the paper. Some figures and tables are inserted far from where they are initially mentioned.\n5. 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.\n\n#### Questions\n1. How is $t_v(q_t)$ estimated using rollouts, given that the framework and the simulations seem to be for the model-free setting?\n2. Could you please explain the reasoning for the choice of $t_v^{baseline}$?\n\n#### Additional Feedback for Improving the Paper\n1. The following references are also highly related to this paper:\n    - 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.\n    - 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.\n2. Compound adjectives require hyphens, e.g., “formal language constrained MDP” $\\to$ “formal-language-constrained MDP”.\n3. The clarity of the paragraphs on “Hard Constraints and Action Shaping” can be improved.\n4. Please further motivate and explain why the constraints introduced in the simulation setting (except “proximity”) are required.\n5. Please make the bibliography consistent in terms of details provided for each reference and the formatting. Also, the year of some references is repeated.\n\n---\n#### UPDATE\nI 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.\n", "extra_scores": {}, "extra_text": {}}, {"review_id": "DUXFRioCrG4", "reviewer": "AnonReviewer1", "summary": "", "questions": "", "limitations": "", "rating": 6, "confidence": 5, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "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": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "update after rebuttal: I think the paper, with the added discussion, improved. \n\nSummary and Contribution\n\nThis 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.\n\n\n\nReasons for Score\n\nWith 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.\n\nStrengths\n\n- A relevant problem is tackled.\n- The usage of formal languages is relevant and has been demonstrated to be helpful in a number of results\n\nWeaknesses\n\n- The contribution of the paper is not clear. Several other works have done very similar approaches, and in much more depth.\n- The assumptions are not clear.\n\nQuestions for Authors\n\n- Please compare your work to the literature listed below. What is novel, how does it relate?\n- 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? \n- In the construction of the formal setting, what is different to the standard product construction of MDPs and finite automata? \n\n\nDetailed Comments\n\n- related work\n\nAt 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:\n\nMohammadhosein Hasanbeig, Alessandro Abate, Daniel Kroening:\nLogically-Correct Reinforcement Learning. CoRR abs/1801.08099 (2018)\n\nMohammadhosein Hasanbeig, Alessandro Abate, Daniel Kroening:\nCautious Reinforcement Learning with Logical Constraints. AAMAS 2020: 483-491\n\nErnst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, Dominik Wojtczak:\nOmega-Regular Objectives in Model-Free Reinforcement Learning. TACAS (1) 2019: 395-412\n\n- formal construction\nIn 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. \n", "extra_scores": {}, "extra_text": {}}, {"review_id": "8omNL6e1Jhf", "reviewer": "AnonReviewer4", "summary": "", "questions": "", "limitations": "", "rating": 6, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "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": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "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). \n\nPros:\n  - 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.\n  - 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.)\n \nCons:\n  - 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.\n\n   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?\n  - 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).\n\n  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.\n  - 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?\n  - 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.\n\nI 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.\n\nSome particular things I would suggest addressing in revisions:\n  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)?\n  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?\n\nSome clarifying questions I'd also appreciate if the authors could address during the discussion:\n  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!\n\n    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.\n  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?\n  3. Any ideas why hard action shaping in both Training and Evaluation sometimes does worse than just during Training or just during Evaluation?\n\nSome more detailed suggestions for improvements (no need to respond to these, they did not affect my decision in any significant way):\n  - 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). \n  - Page 3, \\delta: what is $A$? It is not defined anywhere that I can see – should this be $\\Sigma$?\n  - 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).\n  - Page 3, Constraint State Augmentation: I think the dimensions should be integer ceiling not integer floor.\n  - 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?\n  - Page 7-8: tables of numbers were a bit hard to digest. Consider turning some of them into figures, e.g. bar charts?\n  - Table 5: a bold entry for “Training Only” in Breakout seems incorrect (for dithering, “Training and Evaluation” does better).\n  - Discussion: “was never be empty”->”was never empty”. (“Best effort” also seems an odd phrase for this property.)\n\n### 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. ###", "extra_scores": {}, "extra_text": {}}]

Author rebuttal:

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