Safer Reinforcement Learning with Counterexample-guided Offline Training
Authors: Xiaotong Ji
Antonio Filieri
Venue: Submitted to ICLR 2023 (2023)

Abstract: Safe reinforcement learning (RL) aims at addressing the limitation of reinforcement learning in safety-critical scenarios, where failures during learning may incur high costs. Several methods exist to incorporate external knowledge or to use proximal sensor data to limit the exploration of unsafe states. However, dealing with (partially) unknown environments and dynamics, where an agent must discover safety threats during exploration, remains challenging. In this paper, we propose a method to abstract hybrid continuous-discrete systems into compact surrogate models representing the safety-relevant knowledge acquired by the agent at any time during exploration. We exploit probabilistic counterexamples generation to synthesise minimal, partial simulation environments from the surrogate model where the agent can train offline to produce heuristic strategies to minimise the risk of visiting unsafe states during subsequent online exploration. We demonstrate our method's effectiveness in increasing the agent's exploration safety on a selection of OpenAI Gym benchmarks. 

Under review as a conference paper at ICLR 2023
SAFER REINFORCEMENT LEARNING WITH COUNTEREXAMPLE-GUUI OFFLINE TRAINING
Anonymous authors
Paper under double-blind review
ABSTRACT
Safe reinforcement learning (RL) aims at addressing the limitation of reinforce- ment learning in safety-critical scenarios, where failures during learning may in- cur high costs. Several methods exist to incorporate external knowledge or use proximal sensor data to limit the exploration of unsafe states. However, deal- ing with (partially) unknown environments and dynamies, where an agent must discover safety threats during exploration, remains challenging. In this paper, we propose a method to abstract hybrid aadiinuou--issceed systems into compact sur- rogate models representing the safety-relcvan knowledge acquired by the agent at any time during exploration. We exploit probabilistic counterexamples generation synthesise minimal, partial simulation environments from the surrogate model where the agent can train offline to produce heuristic strategies to minimise the risk of visiting unsafe states during subsequent online exploration. We demon- strate our method's effectiveness in increasing the agent's s exploration safety on a selection of problems from literature and the OpenAl Gym.
Introduction
A critical limitation of applying Reinforcement Learning (RL) in real-world control systems is its lack of guarantee avoid unsafe behaviours. At its core, RL is trial-and-error process, where the learning agent explores the decision space and receives rewards for the outcome of its decisions. However, in safety-critical scenarios, failing trials may result in high costs or unsafe situations and should be avoided as much as possible. Nevertheless, several learning methods try to incorporate the advantages of model-driven and data-driven methods to encourage safety during learning (Kim)
itt al. 2020 Garcia & Fernández] 2015).
One natural approach for encouraging safer learning is to analyse the kinematic model of the learning system with specific safety requirements and to design safe exploration (Garcia & Fernández] 2012 Alshickh et al.] 22018] Pham et al. 2018) or safe optimisation (Achiam et al. 2017: Tessler et al, 2018 Stooke al. (2220) strategies that avoid unsafe states or minimise the expected occurrence of unsafe events during training. However, this approach is not applicable for most control systems with partially- knowwl unknown dynamics, where not enough information is available to characterise unsafe states or events a priori.
To increase the safety of learning in environments with (partially) unknown dynamics, we propose an online-ofie -ofinee learning scheme where online execution traces are used to construct an abstract representation of the visited state-space and the outcome of the agent's actions. The abstraction is iteratively refined with evidence collected online and constitutes compact stochastic model of relevatre aspects of the environment. A probabilistic model checker is then used to produce from the abstract representation minimal counterexample sub-model, i.c., subset of the abstract state space and of the related action space within which the agent can reach unsafe states with a probability larger than tolerable. Simulation-basee learning is then used to train the agent offline within diverse counterexample sub-models to refine its strategy towards avoiding unsafe states. This way, we migrate most trial-and-error risks the simulation environment, while discouraging the exploration of risky behaviours during online learning.
Our main contribution in this paper is a safer RL method for control systems with no prior knowledge of the environment relying probabilistic counterexample guidance. In particular, we 1) propose a conservative geometric abstraction model representing safety-relevan experience collected by the agent any time during online exploration, with theoretical convergence and accuracy guarantees, 2) use minimal label set probabilistic counterexample generation to synthesise small-scale simula- tion environments for the offline training of the agent aimed at reducing the likelihood of reaching

---

Under review as a conference paper at ICLR 2023
unsafe states during online exploration, 3) preliminary evaluation of our method to enhance Q- Learning agent on problems from literature and the OpenAl Gym demonstrating how achieves comparable cumulative rewards while increasing the exploration safety rate by up to 40% compared with previous related work (Hasanbeig et al. 2018 2022).
2 Background
Markov Decision Process. We represent the abstract model of control system and its environ- ment, with hybrid discrete-continuous state space, as a (discrete) MDP (Bellman) 1957): a tuple < S, s0; A, P, R, L 2, where S is finite state space, 8p is the initial state, A is finite set of dis- crete actions, P: S x A S + [0, 1] is the probability of transitioning from a state s E S to s' E S with action a E A, : S function that assigns atomic propositions (AP) to each state.
IR is an immediate reward function, L : S + 24h is labelling
policy π - A selects in every state & the action a to be taken by the agent. Given a discount factor 7 (0, 1], such that rewards received after n transitions are discounted by the factor y", a deterministic policy selects in state 8 E the action arg max, Q (8, a) that maximises the Q- value (Watkins & Dayan 1992) defined as:
(" as) + B ( s4t)) 10 (SL+1, ac+1)l
(I)
Probabilistic Model Checking. Probabilistic model checking is an automated verification method that, given stochastic model the MDP in our case and a property expressed in a suitable prob- abilistic temporal logic, can verify whether the model complies with the property not (Baier & Katoen 2008). In this work, we use Probabilistic Computational Temporal Logic (PCTL) (Hansson & Jonsson| 1994) to specify the probabilistic safety requirement for the agent. The syntax of PCTL formulae is recursively defined as:
+ = true a
+ A +
-6
Poap
(2)
8 = X ΦU
A PCTL property is defined by a state formulae t. whose satisfaction can be determined in each state of the model. true is satisfied in every state, a E AP is satisfied in any state whose label includes E Lss), and A and - are the Boolean conjunction and negation operators. The modal operator Poap'p holds in a state s if the cumulative probability of all the paths originating in s and satisfying the path formula tp does not exceed p E [0, 1] under any possible policy. The Next operator X is satisfied by any path originating in s such that the next state satisfies 4. The Until operator UU is satisfied by any path originating in such that state s' satisfying $2 eventually encountered along the path, and all the states between 8 and 8' (if any) satisfy 4 The formula true U + is commonly abbreviated as F& and satisfied by any path that eventually reaches a state satisfying 4. A model M satisfies PCTL property & if d holds in the initial state so.
PCTL allows specifying variety of safety requirements. In this work, we focus on safety require- ments specified as upper-bounds on the probability of eventually reaching a state labelled unsafe:
Definition 2.1 Safety Specification: Given a threshold X E (0,1], the safery requirement for a learning agent is formalised by the PCTL property Pęx [F unsafel, i.e., the maximum probability of reaching a state labelled as unsa fe must be lower than or equal to X.
Counterexamples in Probabilistic Model Checking. When a model M does not satisfy a PCTL property, a counterexample can be computed as evidence of the violation. In this work, we adapt the minimal critical label set counterexample generation method of (Wimmer et al. 2013), which computes the minimal submodel a subset of the model state space and of the actions possible in such subset- - within which there is a policy that already violates the property:
Definition 2.2 Counterexample of Safety Specification: The solution of the following optimi- sation problem (adapted from (Wimmer et al. 2013)) is a minimal counterexample of the safety specification P Psx [F unsaaaa fe):
minimise 2 -WoP=o +
Σ w())xe, such that
LeL.
2

---

Under review as a conference paper at ICLR 2023
Pso > X
(4)
Vs E T. ps =1
(5)
SS.....
Σ
(6)
aEP(.)
Ts.a
(7)
aEP(s)
E S S Ya E A, vl Lo(s, Da S xt
(8)
E T, Va E A, Ps,.s' ((ss,,,'') PPP Po
(9)
E E A. P. S (1aTaa) +
Σ
Psa.
(10)
&:P(s,a,))
Le(s, a,5 = P(s,a,8))2
(11)
ss E S,aE a. E [0, 1] A Ps.a. E [0, 1] Fe,a E {0,1}
(12)
vl E L,(s,,,8), xe E 10,1]
(13)
where S is the state space of the model, T is the set of states labelled as unsafe, Ps represents the probability of reaching reaching any state in from state 8, ns.a E {0, 1} indicates that action is selected in state Ps.a.s' represents the probability contribution of the transitions from to s' via action a, where this transition selected to be part of the counterexanple. E Le(s, a, s') is the label identifying a transition from s' via (not to be confused with the function L labeling states of the model) such that xι = 1 iff the transition is included in the counterexample, Iι = 0 otherwise.
Intuitively, the optimisation problem aims to find policy æ that will make the agent violate the safety specification within the smallest counterexample sub-model, i.e., the sub-model composed of all the transitions (s, a, s') from the original model whose corresponding 2ı is 1.
To this goal, equation requires the probability of reaching unsafe state be (violation of the safety specification); equation 5 fixes P. = 1 for all the unsafe states; equation 6 jipose the agent to select at most one action for each state s; no action is chosen in a state s, equation ensures that p. = O. equation Anuuationnenaa ensures that the contribution of the transition (s. a, s') is 0 if such transition not included in the counterexample, otherwise, equation 9 Ps.a,s' bounded by the probability of the corresponding transitions in the model (P(s, s')) times the probability of reaching the target from s' (p equation 10 ensures that action is selected in state s, the probability of reaching T from is bounded by the sum of the probabilities of reaching T from its successors given Finally, two additional constraints are defined in (Wimmer et al.) 2013) to prevent the agent from getting stuck in infinite loop that would prevent it from reaching T. We omit them in this section for simplicity and refer the reader to (Wimmer et al., 2013) (they are implemented for our experiments).
In the objective function, the weights (f) assign to the selector variable the opposite normalised Q-value corresponding to the state-action pair in E, while we > ma)(w(()) VE e Le A w(E) > encourage the selection with preference for labels with larger Q-
0}. With this weighting, Value, to discover violating behaviours in the most commonly-selccten state-action pairs, while also minimising the size of the sub-model.
Multiple Counterexamples. The minimal solution the MILP problem in Def. 2.2 may not be unique, and different minimal solutions may lead different violating behaviours (Ceška et al., 2019). Because counterexamples will be used to generate simulation environments for offline learn- ing, we aim to keep their size small for faster training. On the other hand, representing diverse violating behaviours may lead to more robust safety training. To foster the diversity of violating behaviour information used for guiding safer exploration, we further generate a set of "mutations" of counterexample by adding blocking clauses to labels selected in existing counterexamples i.e., adding constraints to the optimisation problem that force arbitrary labels selected in the initial coun- terexample to be deselected by forcing the corresponding Σ₁ 0. The goal is to produce multiple diverse counterexamples that jointly provide a more comprehensive representation of the violations scenarios so far explored by the agent.
3

---

Under review as a conference paper at ICLR 2023
3 Simulation-based Learning with Counterexample Exploration Guidance
We present our learning framework for simulation-based learning with counterexample exploration guidance in this section. The key idea of our method is mitigate the risk of visiting discovered unsafe states by alternating online and offline training phases. The online phases aim at explor- ing the environment and learning the outcome of different actions to build and continuously refine an abstract, compact representation of the control problem. The offline phases use counterexam- ples from the abstract representation to synthesise smaller simulation environments that allow the agent to refine its policies towards minimising the risk of visiting discovered unsafe states. We first describe our abstraction procedure and the synthesis of simulation models in See. [3.]] Then, learning algorithm, combining offline learning with online exploration, and discuss the main challenges of offline learning.
in Sec. [.2 we introduce the simulation-
3.1 SIMULATION MODEL CONSTRUCTION
We present the process of the simulation model construction in three parts: 1) partition different safety behaviours of a continuous state space using a geometric abstraction method based on the sampled dataset of explored paths, and 2) organise the partition results in an MDP surrogate model, and 3) construct the simulation environments for offline learning based on the surrogate model.
Geometric Abstraction. We assume the state to be represented by a vector of real numbers. Sam- pled states not recognised and labelled unsafe by the agent assumed safe to explore, and we also assume the label set of a state to expand monotonically: in particular, a state labelled as unsafe will be considered unsafe for the rest of the exploration. We aim at abstracting the ex- plored concrete state space as a finite set of disjoint polyhedra, each defined as the intersection of a finite set of hyperplanes. This process can be seen as a classification task, where regions of the con- tinuous concrete state space are covered by the union of polyhedra, with the goal of separating safe and unsafe concrete regions. While such separation can achieve arbitrary accuracy by increasing the number of polyhedra, in general, not all shapes of the concrete regions can be exactly covered, and very high accuracy may require a prohibitive computational cost. To control the impact of the limited abstraction accuracy on the safety of the agent, we require the abstraction to conservatively satisfy the following safety invariant at any time.
Definition 3.1 Safety Invariant. All explored unsafe concrete states should be mapped to unsafe abstract states.
Inspired by the idea of casting the learning of geometric concepts as set cover problem in (Bshouty et al., 1998, Sharma et al. 2013), we frame the separation task as a minimal red-blue set cover problem maintaining the safety invariant. Let X = {æoo :..,... Fn } be the set of all explored concrete states and U = {uo. ui..... 3 } be the set of explored states assigned the "unsafe" label. Find the minimum number of sets C, with false classification rate for safe concrete states (X \ U) bounded by a constant f. such that C' = [Ui=1C;}, where each element u E U is covered by one set C,, An element æ is covered by (polyhedra) predicate C2 E C' x Ci, where
C {x we + b S 0}
(14)
We fix w = 1 in this work, i.e., restrict to hyper-boxes rather than arbitrary polyhedra, to simplify the implementation of a branch and bound abstraction procedure. The solution set guarantees that all the unsafe concrete states are covered by Boolean combination of C, while safe concrete states may also be covered by some predicate C, with a given maximum tolerable rate f. Therefore the abstraction may over-approximate the boundaries of an unsafe concrete region thus including also safe concrete states but will not misclassify unsafe regions. The abstraction is refined after each online learning phase to more accurately represent the unsafe regions.
Abstract Model Construction and Minimisation. After mapping each point in the concrete state space to abstract state C, finite surrogate MDP model M. can be constructed from the paths explored during online learning phases by estimating for each abstract state the applicable actions and the resulting transition probabilities to other abstract states. As result of the safety invariant of the state abstraction process, Md may conservatively overestimate the probability of reaching an unsafe state, since some safe concrete states may be abstracted into unsafe abstract states.
In general, the surrogate state space may become intractably large, particularly for the purpose of counterexample generation. To mitigate this issue, we merge adjacent states, i.c.. states connected by at least one transition/one edge, with similar safety behaviours to a single abstract state. The intuition behind this restriction is akin spatial locality, in that states closer to an unsafe state
4

---

Under review as a conference paper at ICLR 2023
more likely to lead to unsafe outcomes in future online phases. To define such merging strategy, we define e-simulation for adjacent states - i.c., abstract states sharing at least one hyperplane adapting the general notion of eee--mmlattoon (c.g., (Desharnais al. (008)):
Definition 3.2 Adjacent e-simulation: Let Sp be the partition of S induced by the equivalence
relation ~ s' iff L(s) L(s'). Then, for a given E [0, 11. two adjacent states s and s' are e-similar (n()) = SD(s') and E Sn \ (S(()). IP(s, a, 8D) - P(s', a, [p)] S e.
The e-simulation in Def. 3 allows the definition of hierarchical merging scheme. Let level lo contain the imitial abstract states. e-similar adjacent states from level 4 are merged into a single state level 1,+1, until further merge is possible. Intuitively, since only adjacent abstract states can be merged, for a given e, the final minimised abstraction is likely to be finer in the neighbourhood of states labelled as unsafe (or as goal), where a small number of steps and corresponding traversal of adjacent states is sufficient to discriminate the outcome of the trajectory being explored; coarser when more steps are required to decide on the outcome.
Simulation. For safety requirement Pęx [F unsafe], we generate counterexamples of the safety specification based on the abstract, minimised model MA using the MIIP introduced in Def. 2.2 All state-action pairs that may directly incur violating behaviours would be included in at least one of the multiple counterexamples generated from the abstract model, provided enough diverse counterexamples
Counterexample-GGide
generated.
Each generated counterexample submodel Meer =< Secr, 80: Accr, Peezy Rear: >> is used as an abstract simulation environment aimed at penalising the selection of actions that are likely to lead to reaching an unsafe state, To this goal, the agent performs offline Q-Learning within Meez with senalty-rewaid function Reez assigning a negative reward -1 upon reaching an unsafe state and 0 when reaching other states notice that, being Meer a sub-model of the abstraction MA. some states may not have outgoing transitions since such transitions would not contribute to the violation of the safety requirement, as discussed in Sec. 2
3.2 SIMULATION-BASED LEARNING WITH COUNTEREXAMPLE GUIDANCE
Algorithm[ summarises the main steps of our simulation-basee learning with counterexample guid- ance. We initially assume no knowledge about the environment is given to the agent; both the abstract model M and the set of explored paths D are empty [ine[]]. If prior knowledge is avail- able, either in the form of an initial abstraction or of previously explored paths, MA and D can be initialised accordingly.
The on 1
procedure (line lets the agent operate in the concrete environment sim- ilar to a standard Q-Learning process for I epochs, but with the following variation. At every step, MA contains an abstraction for the current concrete state, with probability 3 E (0, 1) the agent selects the next action among those available from the corresponding abstract state, proportionally to their respective Q-value, while with probability - / it selects a random action among all those available in the concrete space. Initially, the abstract model is empty, thus the agent will necessarily explore actions not represented in the abstract model. As the learning process progresses, the proba- bility of exploring unknown actions will be bounded by 1 3. This allows potentially exploring new regions of the concrete space and refining the abstraction, while limiting within each online phase the intrinsic risk of exploring unknown regions. The online learning process can terminate earlier the number of visits to unsafe states exceeds [X epochs]
The sequence of explored conerete paths, including the labelled concrete states visited, the action selected, and the collected rewards, is returned in Dontine and added to the experience dataset D that will be used to refine the current abstraction MA. The number of times unsafe concrete states are visited (i unsafe) is also returned and used to decide whether to trigger an offline learning phase to reduce the risk of reaching such discovered unsafe states in the future (line(6).
The offline learning phase starts with refining the abstraction MA (line 77 which is then used to generate a set of counterexamples, each used to train the agent offfine until no significant changes to the Q-values are detected. It is in general possible to generate all diverse counterexamples from MA as described in Sec. 2 However, for large models, generating all of them may be prohibitively expensive and a finite number of counterexamples may be preferable.
Offline learning work on minimal submodels of the approximate, abstract environment each gener- ated from a counterexample, therefore enclosing sufficient trajectories with enough probability mass to violate the safety requirements. Whenever the agent reaches an unsafe state during simulation, negative reward gets backpropagated, ultimately penalizing the actions more likely to eventually
5

---

Under review as a conference paper at ICLR 2023
lead to safety violation. No positive reward is given for reaching goal during offline learning, positive rewards are instead collected during the online phase. In counterexample generation, there trade-off between covering the simulations most relevant to the current policy of the agent and producing a variety of diverse simulation environments. We pursue the first goal by weighting the objective function of the optimization problem in Def with the current Q-values, thus preferring counterexamples closer to the current policy of the agent. We pursue the second goal (multiple counterexamples) by imposing random blocking clause that excludes previously explored coun- terexamples during the same offline learning campaign in Sec.
After each offline learning phase, the agent resumes online learning until convergence is achieved or a new offline phase is triggered by the occurrence enough unsafe events. Different offline phases optimise the generation of counterexamples based the Q-values updated from both online exploration and previous offline learning, thus increasing the likelihood of generating a different set of counterexamples that reduce the exploration risk for the more likely action to be selected that time.
Algorithm 1: Simulation-bused Learning with Counterexample Guidance
MA, D 0:
while not done do
Dontine: funsafe t wateeeeoiiiieeeeeeeeeeaaaaeeeen
// online learning // update the dataset estimate safety rate
D t D U D :
Punsats t tunsafe//epochsss
if Punaate 2 À then
//simulation-based offline learning
MA + A D);
// update the abstract model
for t' t, do
Mcex + Mce A); // generate new counterexample simulation 8 8..
done <- Flsalse;
12
while not done do
// sample action from the action space 8,,, v,r, done + (s) // generate the destination state and reward with the simulation model
Acex
14
Q(s a) + (1 a) ((s, a) + a(r + max(Q(s'));
15
8 5 8
end
18
end
19 end
20 end
Theoretical discussion. The switch between online and offline training reduces a possible shift between the Q-value computed on the abstract states and the Q-value that would result learning directly in the concrete space thanks to the iterative refinement of the abstraction. As already dis- cussed, the set cover solution preserves the safery invariant of Def. 3.1 thus discovered concrete unsafe states will always map to abstract unsafe states. We further analyse the convergence of the abstraction to an arbitrarily accurate representation of the concrete space throughout the learning process by showing that the following claims hold:
1. The probability of exploring any safe unexplored concrete states is always non-zero 2. Eventually, all concrete unsafe states will be abstracted into an abstract unsafe state
3. The misclassification error for unexplored concrete state regions mapped into abstract states, while preserving the safety invariant, can be bounded with a Probably Approxi- mately Correct (PAC) assumption (Valiant 2013)
Since we always allow with a controllable probability 3 the selection of any action available in a concrete state, only reduce the likelihood of selecting potentially risky action, but we do not strictly prevent their selection as in, e.g., shielding methods (Alshickh et al. 2018). In turn, every reachable concrete state will eventually be explored with probability (claim

---

Under review as a conference paper at ICLR 2023
When a previously unknown concrete unsafe state is explored (claim 2), the next refinement of the abstraction will preserve the safety invariant by mapping it to an unsafe abstract state (cf. See. 3.1)
Concerning claim 3. the abstraction error of the cover solution in unexplored space can be bounded with u E (0. with a probability of at least - 8 with PAC assumption (Blumer et al.) Seenik-ChervoennissVVV
[989). If the finite, then L has abstraction eπror at most u with a probability at least 1 - 8 if L is consistent with sample size max( 2 log 3. &VC log 12). According to the proof in (Blumer et al. 1989). VC di- mension of a set cover solution C' in the form of C' C==(6 [U C₁ 0 < i S {} is less than 2d. log(3s), where s the number of set in C. Therefore, the required sample size to bound the abstraction error for a set cover classification is max( á log 2. 16ds (ods)))(33) log 12) Because the probability of ex- ploring any concrete state remains strictly positive, the abstraction will eventually converge any prescribed (u, 5) accuracy with probability 1.
dimension and the dimension of learning concept is
8:
4 Evaluation
We empirically evaluate the performance of our method from the perspective of 1) the improvement in the exploration safety rate and 2) the impact on the cumulative reward achieved by the agent.
Environments. We consider three environments: slippery FrozenLake8x8 from OpenAl Gym (Brockman et al. 2016), DiscreteGrid environment from the implementation of (Hasanbeig et al.) 2022]. and HybridGrd environment, where we change the state space of DiscreteGrid from dis- crete to continuous with the same layout. In all the environments, the agent decides direction of move between up, down, left, and right. We define the objective of the agent as finding policy with maximum Q-value while avoiding unsafe behaviours with intolerably high probability during exploration. In the FrozenLake828 specifically, the agent aims to find a walkable path in an 8x8 grid environment with slippery actions while avoiding entering states labelled with H. With the slippery setting, the agent will move in the intended direction with a probability of only 1/3 else will move in either perpendicular directions with equal probabilities of 1/3 respectively. In the DiscreteGrid environment (Hasanbeig et al., 2022) and HybridGrid environments, the agent aims to reach the states labelled with "goall" and then states labelled with "goal2" in a fixed order while avoiding entering any states labelled with "unsafe" along the path, with 15% uncertainty of moving to ran- dom directions. In HybridGrid, the distance covered in move is also randomly sampled from a Gaussian (2, 0.5) thus moving in the same direction from a state may reach different states.
Surrogate Model and Safety Specification. We parameterise the abstraction process with max- imum false classification rate = 0.05 for the set cover problem setting, 0.01 for adjacent e- simulation, and a discount factor 7 = 0.9 for the Q-value updates. The minimisation of the abstract models reduces the state space by around 99 times (from 1600 to 15 abstract states) in DiscreteGrid. A similar reduction is observed for HybridGrid, where the abstraction can closely represent the grid layout of the continuous space. The resulting counterexamples are comparably small, thus introduc- ing low overhead for both the MILP solution of the offfine learning phases. Although the state space Frozenlake8x8 is originally small, the minimisation process simplifies the number of state space by 21.9% (from 64 to 50 abstract states).
We set the safety specification parameter À 0.2 in DiscreteGrid and HybridGrid, and A 0.35 in Frozenl.ake8x8. 8.e8x8.. These values are chosen to account for the intrinsic uncertainty in the respective environments, where the direction of movement chosen by the agent materialises with a probabil- ity 1/3 in FrozenLake, and 85% in DiscreteGrid and HybridGrid. In HybridGrid, also the length covered by each move is sampled from (22,, 0.5), thus introducing further uncertainty.
Baselines. We compare the learning performance of method to the standard Q-Learning as the baseline without any guidance and compare our method with (Hasanbeig et al.) 2018 2022) (QL- LCRL in the figures), using the same set of tyree-parameters from their implementation. QL-LCRL is included in the evaluation for the intuition of combining model checking with model-free RL to encourage safety during learning, albeit they use model checking to shield them from unsafe actions rather than using counterexamples and offline learning.
Experimental Results Fig A.I shows the accumulated rewards and safety rates in the three envi- ronments. The cumulative rewards of QL, QL-LCRL and QL-CEX (our method) all converge to similar values, showing that the performance under guidance (QL-LCRL and QL-CEX) remains level comparable to the baseline QL method. We observe that QL-CEX has a better average safety rate in all these three environments, and converges to higher safety rates faster than the other meth- ods. In DiscreteGrid and HybridGrid, the safety rate of online learning in our method exceeds the
7

---

Under review as a conference paper at ICLR 2023
INDRDOND
Mms
QU4GAL
OL-CEX
Figure 1: Average reward and safety rate with several experiments in QL, QL-LCRL (Haaanbii al. 2022 and QL-CEX (our method) in FrozenLake8x8,, DiscreteGrid, and HybridGrid
threshold after the first iteration of offline learning. This due to the rapid convergence of the ab- straction thanks to the grid layout that can be accurately and efficiently represented and minimised. In FrozenLake8x8,, more online data required to form an accurate abstraction before the safety specification is satisfied. Although counterexample generation takes extra time in solving the MILP (averaged solve time for single counterexample is less than 0.3 seconds for DiscreteGrid and Hy- bridGrid and less than 2 seconds for Frozenl ake8x8 Macbook Air with M1 CPU and 8Gb of memory, using Gurobi (Gurobi Optimization, LLC]2202) as MILP solver), the offline training takes place within the counterexample-gune space compared to the concrete model.
simulation model, which has significantly smaller state
10
10
15
15
20
20
25
25
30
30
35
35
15
20
15
20
25
30
35
(a) Synthesised policy of QL-LCRL.
(b) Synthesised policy QL-CEX
Figure Synthesised policies of QL-LCRL and QL-CEX in discrete DiscreteGrid
In the DiscreteGrid environment, the reduced abstract state space in QL-CEX significantly speeds up the learning process. We particularly show the synthesised policy of QL-LCRI and QL-CEX with the objective of finishing the two-steps task reach goal I (cyan) and then goal 2 (yellow), avoiding the unsafe regions (red) - in order to compare the influence of the guidance methods. The QL-CEX policy leads to smoother path towards the goal while steering further away from the unsafe regions. This expected since shielding methods prevent the selection of actions deemed unsafe, while providing limited guidance for which alternative to select, while the offline training of QL-CEX leads the agent to adjust the Q-values of all explored actions to reduce the risk of eventually reaching unsafe state.
8

---

Under review as a conference paper at ICLR 2023
Finally, for HybridGrid, the continuous concrete state space prevents the use of QL-LCRL (Hasan- beig et al. 2022). thus we compare only with QL as a baseline. Despite the uncertainty from both the 15% probability of moving in random direction and the distance covered in such direction sampled from (2, 0.5). thus potentially reaching a large set of different states after each action, QL-CCX rapidly converges a safety rate around 70%. We remark that without accurate prior knowledge, it is not possible to entirely avoid visiting unsafe states during online exploration, since their location not known before they are visited the first time. Our method aims increasing the safety rate during online exploration, while it cannot totally prevent unsafe events from happening.
5 Related Work
Safe Exploration. (Garcia & Fernández 2015 Kim et al. 2020 Brunke et al. 2022) provide sur- veys and taxonomies of recent safe reinforcement learning methods with different emphases. Most existing safe exploration methods assume prior knowledge about the environment or the agent's s dy- namics (Moldovan & Abbeel [2012] Fulton & Platzer 2018), known safety constraints (Alshickh)
et al., 2018:Jansen Jansen et al. [018 Hasanbeig et al., 2018: Pham et al. 2018), or utilise expert guid- ance (Garcia & Fernández, [212 Zhou & Lij 2018 Huang al. 2018) to provide guarantee for safety constraints satisfaction during exploration. A different class methods (Sui et al., 2015] Wachi et al., 2018 Liu al.
2020) utilises surrogate Gaussian process models to characterise the unknown dynamics and optimise the unknown function with a prior model structure. There are only a few methods (Dalal al., 2018, Bharadhwaj et al., 2020) to tackle the unknown model structure by training a safety layer/critic used for filtering out probabilistic unsafe actions based on an offline dataset. While motivated by the same idea of safer exploration without prior knowledge, our method can be initialised with none or only small amount of previously explored paths, mhile, show comparable or superior performance to other guidance- based algorithms (Hasanbeig et al.] 2018) that rely prior knowledge of the safety constraints.
Offiine RI. Offline RL can be seen as a data-driven formulation of RI, where the agent collects transitions using the behaviour policy instead of interacting with the environment (Levine et al. 2020). The biggest challenge in offline RL is the bootstrapping error: the Q-value is evaluated with little or no prior knowledge and propagated through Bellman equation (Kumar et al. 2019). (Wu et al. 2019, Siegel et al. 2020) regularise the behaviour policy while optimising to address this issue. (Buckman et al., 2020; Kumar al. 2020) alternatively update the Q values in more conservative ways to learn a lower bound of the Q function using uncertainty estimated with the sampled information. From the safe RL perspective, (Urpí et al. (02T) optimises risk-averse criterion using data previously collected by safe policy offline, and (Bharadhwaj et al. 2020) learn a conservative safety critic offline to tackle the problem of safe exploration with unknown MDPs. Our work instead introduces a pessimistic simulation model, maintaining conservative safety behaviours over the offline dataset and switching between online and offline learning to reduce the shift effect between simulation and concrete control systems.
Conclusion
We presented our investigation of safer offline model-free reinforcement learning method using counterexample-guiee guided simulation. We proposed an abstraction strategy to represent the knowledge acquired during online exploration in succinet, finite MDP model that can consistently and accu- rately describe safery-relevant dynamics of the explored environment. Counterexample generation methods from probabilistic model checking are then adapted to synthesise small-scale simulation environment capturing scenarios in which the decisions of the agent may lead to the violation of safety requirements the probability of reaching an unsafe state is higher than a tolerable threshold. The agent can then train offline within this simulated environment, using a reward scheme aimed at reducing the likelihood of selecting actions that may eventually lead to visiting again already dis- covered unsafe states. The knowledge refined during the offline training phases is then exploited to reduce the risk during subsequent online exploration, while newly explored paths feedback informa- tion to the next offline learning phase.
The alternation of online exploration and offline knowledge refinement and counterexample--uidee learning can ultimately lead to higher safety rates during exploration, without significant reduction in the achieved cumulative reward, as demonstrated in our preliminary evaluation on problems from previous literature and the OpenAl Gym. While this work focused on improving Q-Leaning, the basic framework is not specific to Q-Learning, and we plan to explore its impact on other learning algorithms in future work.

---

Under review as a conference paper at ICLR 2023
References
Joshua Achiam, David Held, Aviv Tamar, and Pieter Abbeel. Constrained policy optimization. In International Conference Machine Learning, pp. 22-31. PMLR, 2017.
Mohammed Alshickh, Roderick Bloem, Rüdiger Ehlers, Bettina Könighofer, Scott Nickum, and Ufuk Topcu. Safe reinforcement learning via shielding. In Thirty-Second AAAI Conference Artificial Intelligence, 2018.
Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT press, 2008.
Richard Bellman. markovian decision process. Journal of mathematics and mechanics, pp. 679- 684, 1957.
Homanga Bharadhwaj. Aviral Kumar, Nicholas Rhinchart, Sergey Levine, Florian Shkurti, and Ani- mesh Garg. Conservative safety critics for exploration. arXiv preprint (xXix:20100144977 2020.
Anselm Blumer, Andrzej Ehrenfeucht, David Haussler, and Manfred K Warmuth. Learnability and the vapnik-chervonenkis dimension. Journal of the ACM (JACM), 36(4):929-963 1989.
Greg Brockman, Vicki Cheung, Ludwig Pettersson, Jonas Schneider, John Schulman, Jie Tang, and Wojciech Zaremba. Openai gym. arXiv preprint arXiv:1606.01550. 2016.
Lukas Brunke, Melissa Greeff, Adam W Hall, Zhaocong Yuan, Siqi Zhou, Jacopo Panerati, and Angela P Schoellig. Safe learning in robotics: From learning-based control to safe reinforcement learning. Anmual Review of Control, Robotics, and Autonomous Systems, 5:41 1 5:411-444, 2022.
Nader H Bshouty, Sally A Goldman, H David Mathias, Subhash Suri, and Hisao Tamaki. Noise- tolerant distribution learning general geometric concepts. Journal of the ACM (JACM), 45 (5):863-88) 890, 1998.
Jacob Buckman, Carles Gelada, and Marc Bellemare. The importance of pessimism fixed- dataset policy optimization. arXiv preprint arXin:2009.06799, 2020.
Milan Češka, Christian Hensel, Sebastian Junges, and Joost-Pieter Katoen. Counterexample-ddiven synthesis for probabilistic program sketches. International Symposium on Formal Methods, pp. 101-120. Springer, 2019.
Gal Dalal, Krishnamurthy Dvijotham, Matej Vecerik, Todd Hester, Cosmin Paduraru, and Yuval Tassa. Safe exploration in continuous action spaces. arXiv preprint 1003:::180100775550 2018.
Josée Desharnais, François Laviolette, and Mathieu Tracol. Approximate analysis of probabilistic processes: Logic. simulation and games. In 2008 Fifth International Conference Quantitative Evaluation of Systems, pp. 264-273. IEEE, 2008
Nathan Fulton and Andre Platzer. Safe reinforcement learning via formal methods: Toward safe control through proof and learning. Proceedings of the AAAI Conference on Artificial Intelligence, 32(1), Apr 2018.
Javier Garcia and Fernando Fernández. Safe exploration of state and action spaces in reinforcement learning. Journal of Artificial Intelligence Research, 45:515-564, 2012.
Javier Garcia and Fernando Fernández. A comprehensive survey on safe reinforcement learning. Journal of Machine Learning Research, 16(1):1437-1480, 2015. 2015.
Gurobi Optimization, LLC. Gurobi Optimizer Reference Manual, 2022. URL https: gurobi com
Hans Hansson and Bengt Jonsson. A logic for reasoning about time and reliability. Formal aspects of computing, 6(5):512-535, 1994.
Mohammadhosein Hasanbeig. Alessandro Abate, and Daniel Kroening. Logicclly-constrainee re- inforcement learning. arXiv preprint arXiv: 11880000099, 2018.
10

---

Under review as a conference paper at ICLR 2023
Mohammadhosein Hasanbeig, Daniel Kroening, and Alessandro Abate. LCRL: certified policy synthesis via logically-constraiie reinforcement learning. In Frika Ábrahám and Marco Paolieri (eds.), Quantitative Evaluation of Systems 19th International Conference, QEST 2022, War- saw, Poland, September 12-16, 2022, Proceedings, volume 13479 of Lecture Notes in Com- puter Science, pp. 217-231. Springer, 2022. doi: 10. 000007797888-31--63333 https: /ttps://doi..om wrw.:..orgg....
URL
Jessie Huang, Fa Wu, Doina Precup, and Yang Cai. Learning safe policies with expert guidance. Advances in Neural Information Processing Systems, 31, 2018.
Nils Jansen, Bettina Könighofer, Sebastian Junges, and Roderick Bloem. Shielded decision-making in mdps. arXiv preprini arXiv:/807 177666/807.060996 2018.
Youngmin Kim, Richard Allmendinger, and Manuel López-lbáñezz Safe learning and optimization techniques: Towards survey of the state of the art. In International Workshop on the Foundations of Trustworthy Al Integrating Learning, Optimization and Reasoning, pp. 123-139. Springer, 2020.
Aviral Kumar, Justin Fu, Matthew Soh, George Tucker, and Sergey Levine. Stabilizing off- policy q- learning via bootstrapping error reduction. Advances in Neural Information Processing Systems, 32, 2019.
Aviral Kumar, Aurick Zhou, George Tucker, and Sergey Levine. Conservative q-learning for offline reinforcement learning. Advances in Neural Information Processing Systems, 33:1179-111 1191, 2020.
Sergey Levine, Aviral Kumar, George Tucker, and Justin Fu. Offline reinforcement learning: Tuto- rial, review, and perspectives on open problems. arXiv preprint urXiv:2005.01643 2020.
Anqi Liu, Guanya Shi, Joon-Jo Chung, Anima Anandkumar, and Yisong Yue. Robust regression for safe exploration in control. In Learning for Dynamics and Control, pp. 608-619 PMLR, 2020.
Teodor Mihai Moldovan and Pieter Abbeel. Safe exploration in markov decision processes. arXiv preprint Xrviv:2055. /201.480.......... 2012.
Tu-Hoa Pham, Giovanni De Magistris, and Ryuki Tachibana. Optlayer-practica constrained opti- mization for deep reinforcement learning in the real world. In 20/8 IEEE International Confer- ence on Robotics and Automation (ICRA), pp. 6236 6236-6243 IEEE, 2018.
Rahul Sharma, Saurabh Gupta, Bharath Hariharan, Alex Aiken, and Aditya V Nori. Verification as learning geometric concepts. In International Static Analysis Symposium, pp. 388-411. Springer, 2013.
Noah Y Siegel, Jost Tobias Springenberg, Felix Berkenkamp. Abbas Abdolmaleki, Michael Ne- unert, Thomas Lampe, Roland Hafner, Nicolas Heess, and Martin Riedmiller. Keep doing what worked: Behavioral modelling priors for offline reinforcement learning, arXiv preprint arXiv:2002.08336, 2020.
Adam Stooke, Joshua Achiam, and Pieter Abbeel. Responsive safety in reinforcement learning by pid lagrangian methods. In International Conference on Machine Learning, pp. 9133-9143. PMLR, 2020.
Yanan Sui, Alkis Gotovos, Joel Burdick, and Andreas Krause. Safe exploration for optimization with gaussian processes. In International conference machine learning, pp. 997-1005. PMLR, 2015.
Chen Tessler, Daniel J Mankowitz, and Shie Mannor. Reward constrained policy optimization. arXiv preprint 1105: 2018.
Núria Armengol Urpí, Sebastian Curi, and Andreas Krause. Risk-averse offline reinforcement learn ing. arXiv preprint drXtvv22102.0537,, 2021.
Leslie Valiant. Probably approximately correct: natureōs algorithms for learning and prospering in complex world. Basic Books (A7)), 2013.

---

Under review as a conference paper at ICLR 2023
Akifumi Wachi, Yanan Sui, Yisong Yue, and Masahiro Ono. Safe exploration and optimization of constrained mdps using gaussian processes. Proceedings of the AAAI Conference on Artificial Intelligence, volume 32, 2018.
Christopher JCH Watkins and Peter Dayan. Q-learning. Machine learning, 8(3):279-292, 1992.
Ralf Wimmer, Nils Jansen, Andreas Vorpahl, Erika Abrahám, Joost-Pieter Katoen, and Bernd Becker. High-level counterexamples for probabilistic automata. In International Conference on Quantitative Evaluation of Systems, pp. 39-54. Springer, 2013.
Yifan Wu, George Tucker, and Ofir Nachum. Behavior regularized offline reinforcement learning. arXiv preprint arXiv: 191,111 2019.
Weichao Zhou and Wenchao Li. Safety-aware apprenticeship learning. In International Conference Computer Aided Verification, pp. 662-680 Springer, 2018.
12

---

Under review as a conference paper at ICLR 2023
A Appendix
A.I
ADDITIONAL EVALUATION NOTES
FROZON JACCEA
DSCRETOORO
GL
QI-CCL
QI-CEX
Figure 3: Average reward and safety rate with several experiments QL, QL-LCRL (Hasanbeig al. 2022) and QL-CEX (our method) in FrozenLake8x8 and DiscreteGrid with 100k online learn- ing episodes
We compared the learning performances of our method and the other two baseline methods with three different environments in Sec. 4 with 5,000, 2,000, and 2,000 training episodes respectively. However, due to the high uncertainty the FrozenLake8x8 environment, none of the evaluated meth- ods achieves the 65% safety rate threshold within 5,000 episodes while only QL-CEX (our method) achieves the required safety rate threshold (80%) in DiscreteGrid within 2,000 episodes. Fig. shows the evaluation on FrozenLake8x8 and DiscreteGrid when 100,000/50,000 online learning episodes are allowed. It can be observed that both baseline methods and QL-CEX eventually con- verge a policy that satisfy the safety requirement, However, QL-CEX has generally faster safety rate improvement trend and already after few thousand episodes, which reduces the number of unsafe events also throughout the subsequent online exploration phases. Notably, the offline learn- ing phases are triggered if the preceding online phase violated the safety requirement. Hence, they should occur less frequently as exploration and abstraction consolidate.
A.2 IMPLEMENTATION
used with QL, QL.-ICRII, and QL-CEX are the same. For QL- LCRL-specific additional typer-parameten we use the same values as (Hasanbeig al. 2022). The discount factor is 7 = 0.9, confidence level of the cover solution a = 0.95 (confidence) and e 0.01 for adjacent c-simulation used with same values for all environments. In the environment of slippery Frozenlake8x8, we set the learning rate a 0.1 and the initial value of a decaying probability of random exploration equal 0.2, due the high uncertainty in environment. In DiscreteGrid and HybridGrid, we set the learning rate a = 0.9 and the initial value of a decaying probability of random exploration equal to 0.3.
All common
To ease reproducibility and future comparisons, as well as reduce threats to the internal validity of experiments due bugs in our implementation, the code implementing QL-CEX is available at: https: //nn:mou/s 4open. eeciienner////e CEX 70BD
13


Reviews:
[{"review_id": "pvnZfdmnKvl", "reviewer": "Reviewer_4QqX", "summary": "", "questions": "", "limitations": "", "rating": 3, "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": "This paper proposes a method that extends Q-learning to train offline on counterexamples of unsafe states, generated through a safety specification combined with set covering algorithm. ", "summary_of_the_review": "I think this paper presents a nice method for safe RL in simple environments, however my main issue with this paper is that the writing is not clear enough, so I recommend a reject.", "strength_and_weaknesses": "## Strengths\n\n**************Method:**************\n\n- The set cover formulation is very interesting and seems like a nice way to abstract states into sets of unsafe and safe states.\n- The tie-in to VC dim/PAC learning analysis is nice, I wonder if the authors can show these bounds holding empirically?\n\n************************Experiments:************************\n\n- Experiments are solid, showing a higher safety rate and similar or sometimes higher rewards to sensible baselines.\n\n## Weaknesses\n\n**Clarity:** \n\n- The background section could be written better.\n    - “atomic propositions” are stated without definition in the first paragraph.\n    - First sentence mentions a hybrid discrete-continuous state space, but then talks about $S$ being a finite state space. This is a bit confusing; the hybrid discrete-continuous state space can be introduced and then detailed later. I think it makes sense to talk about this only in Section 3.\n    - The Probabilistic Model Checking section is confusing for someone (like me) who has not seen PCTL before. Rather than just listing everything and defining everything, after Eqs 2/3, it may make more sense to write an intuitive explanation of how PCTL is used for safety checking, define only the necessary terms, and then leave extra details to an appendix. Perhaps the authors could keep the definitions there, but explain how things are used. For example, they define the modal operator but do not mention how its connection to the RL safety problem. This applies for all operator definitions and makes this section very hard to read.\n    - Again, in Definition 2.2, the main paper doesn’t need a huge, multi-line equation with a bunch of definitions. This should be left to the appendix, and it makes the paper harder to read. I’m not saying these equations are unnecessary, it’s just that the authors have presented them in a way that detracts from the clarity, and therefore quality, of this paper. Similarly, the explanation below details most of the equations and simply writes out what they are in words. This is unnecessary—-a higher-level intuitive explanation is better.\n- Assumptions should be better stated beforehand: e.g. that the transition dynamics are assumed to be known.\n- The word “simulation” may imply some kind of sim2real situation to certain groups of RL researchers. Perhaps instead of “simulation,” the authors can replace this with “offline learning phase.”\n- Safety rate seems to be only defined in L5 of Alg 1, but talked about extensively in the experiments. The authors should properly define it in-text in the experiments section again.\n\n**Experiments:** \n\n- I know that this is not the point of the paper, but it would be nice to extend this algorithm to a continuous control task, the only difference being the underlying Q-learning algorithm would have to change to something like an actor-critic alg.\n- Is there a possibility that the advantages over QL and QL-LCRL comes from the number of updates performed? DiscreteGrid8x8’s results make me a little suspicious that the results could be more similar if the other two baselines were matched in the ratio of Q-learning updates performed to environment steps.\n\n****************************Minor details:****************************\n\n- Typos:\n    - “hybrid discrete-continues state space”\n    - “Probabilistic model checking” background section: extra parenthesis after $\\alpha$\n- Questions:\n    - A max false classification rate of 0.95 seems very high. Can the authors explain this choice?\n- Some missing safety papers taking different approaches the authors could cite and compare: [https://arxiv.org/pdf/1702.01182.pdf](https://arxiv.org/pdf/1702.01182.pdf), [https://arxiv.org/abs/2008.06622](https://arxiv.org/abs/2008.06622),  [https://www.aaai.org/AAAI22Papers/AAAI-5810.MaY.pdf](https://www.aaai.org/AAAI22Papers/AAAI-5810.MaY.pdf)", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "4: All of the claims and statements are well-supported and correct.", "technical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work.", "empirical_novelty_and_significance": "2: The contributions are only marginally significant or novel."}, "extra_text": {}}, {"review_id": "p7KsUbJKYg", "reviewer": "Reviewer_QNmG", "summary": "", "questions": "", "limitations": "", "rating": 3, "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": "This paper studies the problem of safe reinforcement learning. It proposes a model-based reinforcement learning algorithm to address the problem, by abstracting the states and constructing a minimal environment to improve the local safety of the learned policy. The small environment is constructed by finding \"counterexamples\" using probabilistic model checking. Experiments on three toy environments from related literation and OpenAI Gym are conducted to show the efficacy of the proposed algorithm. ", "summary_of_the_review": "As stated above, I'm concerned about the complexity of the proposed method,  the insufficiency of the experiments and the lack of rigid theoretical analysis. I don't recommend acceptance in its current form. ", "strength_and_weaknesses": "My major concern with the paper is that it proposes an overcomplicated method, conducts experiments on toy examples and lacks rigid theoretical analysis. \n\n- Method:\n  - I'd say the QL-CEX is very sophisticated: It involves state abstraction, building and minimizing a dynamics model and finding counterexamples (i.e., sub-dynamics where the current policy visits unsafe states with probability greater than $\\lambda$). \n  - The algorithm invokes the `onlineQLearning` procedure, but the standard Q Learning only works for discrete state/action space. How does it work for the HybridGrid environment? Furthermore, is the $Q$ in Algorithm 1, L.15 the same $Q$ used in L.3? Note that the real environment has a different reward function than $R_{cex}$ and even the state space is different. \n  - I didn't understand why PCTL is used for probabilistic model checking. As far as I can see, the proposed method discretizes state space (in the sense that every state is mapped to a discrete abstract state) and also learns a model. So I think it might be possible to reuse the existing work on safety RL in a tabular case. \n\n- Experiments: \n  - The experiments are simple and can only serve as proof of concept. I don't see an obvious way to scale up QL-CEX. As far as I can see, QL-CEX converts a continuous state space to a discrete state space, which means that it essentially can't deal with a continuous state space. \n  - The paper uses QL-LCRL as a baseline, the experiments show that it's only slightly better than the standard Q Learning algorithm in DiscreteGrid and even worse than it. Any other good baselines? \n  - In FrozenLake8x8, all of the three algorithms don't satisfy the safety constraint: the one that performs best only achieves ~25% safety rate, which is far from the goal (65% if I understand it correctly). \n  - This paper lacks ablation studies. For example, how well do geometric abstraction and model construction work? \n- Theory:\n  - I don't expect a theoretical analysis of state abstraction, which is not the central topic of this paper. I expect a theoretical analysis of other properties of QL-CEX, e.g., convergence, safety guarantee, and sample efficiency. ", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "2: Several of the paper’s claims are incorrect or not well-supported.", "technical_novelty_and_significance": "2: The contributions are only marginally significant or novel.", "empirical_novelty_and_significance": "1: The contributions are neither significant nor novel."}, "extra_text": {}}, {"review_id": "XW-jZQjHOyY", "reviewer": "Reviewer_xUpK", "summary": "", "questions": "", "limitations": "", "rating": 3, "confidence": 4, "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": "This paper addresses safe reinforcement learning (RL) problems for safety-critical applications where failures during learning may incur high costs. The authors aims to deal with (partially) unknown environments and dynamics, where an agent must discover unsafe state-action pairs during exploration. In this paper, the authors propose an abstraction strategy to represent the knowledge\nacquired during online exploration in a succinct, finite MDP model that can consistently and accurately describe safety-relevant dynamics of the explored environment. The authors exploit probabilistic counterexamples generation to synthesize minimal, partial simulation environments from the surrogate model where the agent can train offline to produce heuristic strategies to minimize the risk of visiting unsafe states during subsequent online exploration. The effectiveness of their proposed method is demonstrated in several benchmark tasks.", "summary_of_the_review": "Though the problem setting is interesting and the proposed approach is interesting, I have several concerns especially on theoretical and empirical results. I strongly recommend the authors to rewrite this paper by 1) improving the theory part (i.e., clearly state theorems and provide formal proofs) and 2) improving experiment part (i.e., add experiments on continuous control with strong baselines and provide source code or sufficient information for reproducibility).", "strength_and_weaknesses": "### Strength\n**Important problem to be solved**. I think this paper addresses an important problem for (safe) RL community.\n\n**Interesting approach**. I think the proposed ideas are interesting and technically-sound. It is particularly nice to propose a method which does not require a prior knowledge and small amount of offline data.\n\n### Weakness\n**Theory**. There are theoretical discussions in page 6, but this part is quite unfriendly to the readers. The descriptions are informal, and there is no proof. I feel that most of the readers cannot catch up with the theoretical analyses in this paper. I guess this is due to the page limit, and I recommend the authors to\n+ Clearly state each theorem with necessary assumptions. Also, provide proofs for theorems.\n+ The authors can write proofs in the appendix if there is no space in the main paper. \n\n**Experiment**. The benchmark problem is rather easy, so I think that the authors should have tested their method in continuous control problems as well as grid world. In this case, the baseline methods should be PPO-Lagrangian or CPO. The current experiments are conducted in limited problem settings; hence, I don't think that the authors' claims have been sufficiently supported empirically.\n\n**Minor comments**\n+ [Section 2]  A policy $\\pi: s \\rightarrow a$ $\\Longrightarrow$ A policy $\\pi: S \\rightarrow A$\n+ [Section 4] Ray & Amodei (2019) is the paper on Safety-Gym, so it is not appropriate to cite this for Slippery FrozenLake8x8\n+ [Section 5] apriori --> a priori\n \n", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "2: Several of the paper’s claims are incorrect or not well-supported.", "technical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work.", "empirical_novelty_and_significance": "2: The contributions are only marginally significant or novel."}, "extra_text": {}}, {"review_id": "Vg3107id_p", "reviewer": "Reviewer_noqT", "summary": "", "questions": "", "limitations": "", "rating": 3, "confidence": 2, "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": "The authors propose a safe reinforcement learning algorithm for the setting where the environment dynamics are unknown or partially known. A hybrid offline-online learning method is proposed where some online exploration is done to construct a notion of safety in that environment. The authors use a probabilistic model checker to produce counterfactual sub-models, which are potentially unsafe states. Finally, simulation-based learning is used to train the agent offline to avoid reaching unsafe states.  \n\n", "summary_of_the_review": "- Authors propose a model-based safe RL method, with an online exploration component to construct a counterfactual sub-model to learn about unsafe actions and states via probabilistic model checking. \n- Experiments results on model-based safe RL baseline demonstrate the efficacy of the proposed method.  \n\n--- Review update ---\n\nThank you authors for all the efforts. I have read the reviews by other reviewers, and I agree with the following broad limitations of the paper:\n\n- Complex method, without satisfactory experimental results. \n- Lack of rigid theoretical analysis.\n- As pointed out by Reviewer xUpK, the theory introduced in the paper is very hard for the readers to follow, so the writing needs a lot of improvements. \n\nBased on the lack of strong experimental results, and writing, I am changing my scores of the paper. I recommend authors change the writing and experimental section based on the reviews. ", "strength_and_weaknesses": "Strengths of the paper:\n\n- The paper is well-written and succinctly introduces the notion of model-based safety. \n- The counterfactual construction of safety specification seems elegant, though I have to admit I am not very well-versed in the literature on formal verification and model-based safe RL. \n- Empirical results look promising. \n\nSome questions to the authors: \n\n- Why did authors restrict the baselines to Hasanbeig et. al 2018; 2022? Why aren't baselines from offline RL, for ex: RISK-AVERSE OFFLINE REINFORCEMENT LEARNING, ICLR'21 used? ", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "3: Some of the paper’s claims have minor issues. A few statements are not well-supported, or require small changes to be made correct.", "technical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work.", "empirical_novelty_and_significance": "2: The contributions are only marginally significant or novel."}, "extra_text": {}}]

Author rebuttal:

Decision: Reject