Test Where Decisions Matter: Importance-driven Testing for Deep Reinforcement Learning
Authors: Stefan Pranger
Hana Chockler
Martin Tappler
Bettina Könighofer
Venue: NeurIPS 2024 poster (2024)
Keywords: Policy Verification
Probabilistic Model Checking
Deep Reinforcement Learning
Primary area: interpretability_and_explainability

Abstract: In many Deep Reinforcement Learning (RL) problems, decisions in a trained policy vary in significance for the expected safety and performance of the policy. Since RL policies are very complex, testing efforts should concentrate on states in which the agent's decisions have the highest impact on the expected outcome. In this paper, we propose a novel model-based method to rigorously compute a ranking of state importance across the entire state space. We then focus our testing efforts on the highest-ranked states. In this paper, we focus on testing for safety. However, the proposed methods can be easily adapted to test for performance. In each iteration, our testing framework computes optimistic and pessimistic safety estimates. These estimates provide lower and upper bounds on the expected outcomes of the policy execution across all modeled states in the state space. Our approach divides the state space into safe and unsafe regions upon convergence, providing clear insights into the policy's weaknesses. Two important properties characterize our approach. (1) Optimal Test-Case Selection: At any time in the testing process, our approach evaluates the policy in the states that are most critical for safety. (2) Guaranteed Safety: Our approach can provide formal verification guarantees over the entire state space by sampling only a fraction of the policy. Any safety properties assured by the pessimistic estimate are formally proven to hold for the policy. We provide a detailed evaluation of our framework on several examples, showing that our method discovers unsafe policy behavior with low testing effort.

Test Where Decisions Matter: Importance-driven Testing for Deep Reinforcement Learning
Stefan Pranger,' Hana Chockler, Martin Tappler, 3 Bettina Könighofer
Institute of Information Security,
Graz University of Technology
Kings College London
Institute of Computer Engineering, TU Wien
hont hana www.ahhccccckckccccoookk ac.uk martin. hartäan.tapplerrttw.e..cccc
Abstract
In many Deep Reinforcement Learning (RL) problems, decisions in a trained policy vary in significance for the expected safety and performance of the policy. Since RL policies very complex, testing efforts should concentrate states in which the agent's decisions have the highest impact on the expected outcome. this paper, propose novel model-based method to rigorously compute ranking of state importance across the entire state space. We then focus our testing efforts on the highest-ranked states. In this paper, focus testing for safety. However, the proposed methods can be easily adapted to test for performance. In each iteration, testing framework computes optimistic and pessimistic safety estimates. These estimates provide lower and upper bounds on the expected outcomes of the policy execution across all modeled states in the state space. Our approach divides the state space into safe and unsafe regions upon convergence, providing clear insights into the policy's weaknesses. Two important properties characterize our approach. (1) Optimal Test-Case Selection: At any time in the testing process, our approach evaluates the policy in the states that are most critical for safety. (2) Guaranteed Safety: Our approach can provide formal verification guarantees over the entire state space by sampling only a fraction of the policy. Any safety properties assured by the pessimistic estimate are formally proven to hold for the policy. We provide detailed evaluation of our framework on several examples, showing that our method discovers unsafe policy behavior with low testing effort.
1 Introduction
Deep reinforcement learning (RL) [1] is powerful method for training policies that complete tasks in complex environments. Due to the high potential RL in safety-critical domains, such as autonomous driving [2], ensuring the reliability of its safety-critical properties is becoming increasingly vital. Formal verification provides provable correctness guarantees [3]. However, the most significant challenge in the formal verification of RL policies is scalability, which limits its current applicability [4]. As for conventional software, a complete safety evaluation by exhaustively testing policy's is decisions is infcasible. Hence, it is necessary establish much confidence as possible in a policy with a limited testing budget.
38th Conference on Neural Information Processing Systems (NcurIPS 2024).

---

Environment
MDP of environment
Restriczed
sample policy
Specification
RL policy
Optimistic estimate
Pessimistic estimate
Clustering
Stop?
Importance
ranking
Final results
Figure High-level view of algorithm for importance-driven testing for RL.
We propose a novel model-based testing framework for RL policies, which tests policies in the states where their decisions matter most. We follow the insights from Chockler et [5] that not all decisions hold equal significance on the expected safety and performance of a policy. Decisions in certain states may have a significant impact on the overall expected outcome the policy, while in other states, the impact may not be as severe or critical. The core of our algorithm is ranking of the importance of states of the environment. This ranking is based on the difference that the decision in a particular state makes the expected overall performance (e.g.. accumulated reward) or safety of the policy. For lack of space, we focus on safety from here on. The proposed method can easily be adapted to evaluate the agent's performance, which we discuss in Appendix D.
Figure outlines our algorithm. The inputs to our algorithm are model of the environment in the form of a Markov decision process [6], a formal safety specification y,, and an RL agent in the form of a deterministic policy. In each iteration, our algorithm computes optimistic and pessimistic estimates, which provide lower and upper bounds for the expected probability of satisfying the safety specification over all possible policies. The algorithm terminates the maximal difference between the estimates gets below some threshold
maximal number of executed test cases is reached. As long as the stopping criterion is not met, the algorithm computes an importance ranking of the states. The higher the rank of a state, the more influence the decision in that state has for satisfying violating the safety specification. Next, the most important decisions the policy are sampled and used fix the decisions, thus restricting the MDP. The algorithm continues with the restricted MDP to iteratively refine the estimates. Our testing framework can be modified through an optional step by clustering the highly ranked states. A fraction of test cases is then uniformly selected from the individual clusters. The intuition behind clustering is that the agent is likely to behave similarly in comparable situations. Following this intuition, we mark all states in cluster as safe if all tested states of this cluster are verified to be safe. Otherwise, the entire cluster is marked as unsafe. This increases the scalability of testing approach since only fraction of each cluster needs be tested for deriving test verdicts for all states in the cluster. However, since not all decisions in cluster are sampled, unsafe policy behavior can be missed.
Our algorithm provides the following benefits:
Optimal Test-Case Selection: At any time in the testing process, approach evaluates the policy in the states that are most critical for safety.
Guaranteed Safety: A pessimistic estimate provides a formal verification guarantee: under the given model it is guaranteed that if the pessimistic estimate for given state satisfies the testing criteria, then the agent's policy formally verified from that state.
Highlighting the most important decisions is central technique in explainable Al [7, 8). We provide a rigorous method to compute an importance ranking. Simpler policies that only use the top-ranked decisions can help understand the policy's 's prrision-making [5].
The iterative nature of our approach can be used in debugging process to construct safety frontier: if a sampled decision in a certain state is evaluated to unsafe, the next ranking iteration assigns higher importance to the predecessor states to be tested next. Thus, the unsafe region around safety hazard grows until it reveals all states where the policy behaves unsafely.
Upon convergence, our approach partitions the state space into safe and unsafe regions. The identified unsafe regions offer interpretable insights into the policy's current weaknesses.

---

1.1 Related Work
Evaluation of RL policies. Off-policy evaluation (OPE) [9, 10, 11] aims to estimate the expected performance of newly trained policy by using executions of a previously trained policy. In contrast, our approach estimates the performance of the policy under test by computing the best-possible (optimistic) estimate and the worst-pose porst-possible (pessimistic) estimate in the current MDP. In contrast to OPE, our framework provides formal verification guarantees over the entire state space: any safety property assured by the pessimistic estimate is formally proven to hold. Several recent works proposed evaluation strategies to analyze RL policies [12], by adapting software testing techniques to RL. Various approaches apply fuzz search-based testing in the black-box environment [13, 14, 15, 16). in which to test the policy. Most efforts of the testing community focused on selecting test cases that falsify safety with high probability [15, 17]. These methods effectively reveal unsafe behavior, but they do not provide safety assurance from non-failing tests, they lack proper notions of coverage. In contrast, our testing approach is model-based. Model-based testing of probabilistic systems was proposed in [18]. To the best of our knowledge, there is no model-based testing approach for RL policies with formalized criteria of completeness. That is, we are the first to propose safety estimates with formal interpretations which form the basis of our test-case generation.
basis to find safety-critical situations
Model-based formal methods for model-free RL. Several recent works have proposed approaches for developing RL controllers by combining model-based formal methods and model-free RL. The appeal of this combination lies in the strengths of each approach: model-based methods offer formal safety and correctness guarantees, while model-free RI demonstrates superior scalability and yields high-performance controllers by learning from the full-order system dynamics [19, 20). Most of the existing work in this area addresses the problem of safe exploration in RI. [21, 22]. To the best of our knowledge, our work is the first to employ similar techniques for analyzing a trained policy.
Importance ranking. Ranking policy decisions has been proposed for explaining and simplifying RL policies. In [5], the ranking is based on statistical fault localization computed on a set of executions of the original policy and its small perturbations. A continuation of this work [23] uses an average treatment effect to rank policy decisions. In contrast, we provide a rigorous method to compute the importance ranking. Our estimates consider any possible behavior of the policy over the entire state space. Thus, the estimates provide strong verification guarantees. Similarly to ranking policy decisions, [24] rank the importance of individual neurons in network to assess coverage of a given test set.
2 Background
Markoy Decision Process. A Markov decision process (MDP) [25] M = (S,A, p) is a tuple
with a finite state set S. finite set A = {ai...,a,, ] of actions, probabilistic transition function
P S x A x S - [0, 1]. and probability distribution of initial states S + [0. 1]. An execution (or path) is finite or infinite sequence p = su, ag, $1, 01 with ((s;, ae, $1+1) > 0 and p(so) > 0. A (memoryless deterministic) policy π : S + A is function mapping states to actions. II denotes the set of all memoryless deterministic policies. Applying to an MDP M induces a Markov chain (MC) .M" An execution in . is a sequence p 80, 81, .., with P(s;, n (8:), 8:+1) >> 0. Pr denotes the unique probability measure of M over infinite executions starting in 8.
Probabilistic Model Checking. Probabilistic model checking [3] computes the probabilities of satisfying a temporal-logic formula yp over a finite or infinite horizon. We define the properties below with bound n. For the unbounded horizon, n = co. For a given MDP M, a policy ग, and a property o Computation Tree Logic (CTL) [3], model checking computes the following probabilities:
P : S x N + J0, 1] is the expected probability to satisfy yp state S within n steps in M pmax
MM () = maxten P (o n) is the maximal expected probability over all policies II from state within n steps.
pinin
n) = min P. P.M (s, n) is the minimal expected probability over all policies in II from state within n steps.
(,, (s,
For the remainder of this paper, let yp be a formula in the safety fragment of CTL. Using & and a user-defined safety threshold 6p, we define safety objectives as follows:
3

---

Algorithm Importance-driven model-based testing (IMT)
Input: MDP M, policy æ, safety objective (42, 6p))
Parameters: # samples safety threshold 6,, minimal difference Egp
Output: failure states Sj S S, safe states S S S, estimates Copt S and epes - R
1: M S, + S; S 0; S2 + 0: 2
2: loop
3:
Copts Epes computeestimates((""
4: S. + S. fs E Su
epes (8) 2 {pp
5:
Sj Sj U E Su koptl (8) 04)
6: S. < Su (8 E Su (xp)(() < 04 epes
(8) 2 à
7: if (eop
epes (8))
Ep. then
8:
stop end if
9:
10:
Srank =coopputRaanking(MMM mm]
{(51. 01) ... (Sm: }m)) < samplePolicy(#= Srank)
M(HT) +- restrictMDP(MM)). ((s,)) 01). (sm: am)))
13:
it
end loop
15: return Sy, Copt, Epes
Definition 2.1 (Safety objective). Given an MDP M = (S,A,P, n)), safety property y, and threshold 6g [0, 1]. A safety objective tuple (9p, 62). policy ιT satisfies (p,, 6,)) from a given state 8 E S within steps if P
2 8p-
Reinforcement Learning. An RL [1] agent learns task via interactions with unknown envi- ronment modeled by an MDP M with an associated reward function R S + R. In each state A. the environment then moves to state s' with probability
E S, the agent chooses action P(s, a, s'), The return retp of an execution p is the discounted cumulative reward defined by ret, o RR(R)) using the discount factor y E [0, 1j. The objective of the agent is learn deterministic memoryless optimal policy xt that maximizes the expectation of the return.
3 Importance-driven Testing for RL
In this section, will describe framework for importance-driven model-based testing, which abbreviate with IMT. An overview of our algorithm is depicted in Fig. 1. Its central elements are the computation of the estimates and the importance ranking that guides the selection of the test cases. In Sec. 3.1 we discuss IMT in detail, and in Sec.3.2 we discuss its extension with clustering.
3.1 Importance-driven Model-Based Testing
Alg. gives the pseudo-code of our approach for importance-driven safety testing. Our algorithm evaluates policy with respect to safety objective (yp, 6,)) over horizon of steps (for the unbounded horizon, = oo). The algorithm takes as input an MDP M = AS, A, P, jt), policy under test S A, and safety objective (p,6,p) It returns result classification states into safe and failure states (S, and Sy, respectively). and the optimistic and pessimistic estimates for all states in the state space (Copt S + [0, 1] and epes S [0, 1]. respectively), which derived as the expected maximal and minimal probability of satisfying the safety objective 8p))
Safety estimates. In Line 3, IMT computes the safety estimates for the current (restricted) MDP M The optimistic estimate copt n) is the maximal expected probability of satisfying & for an execution in M from given state within a steps quantified over all policies. Similarly, the pessimistic estimate (s, n) is the minimal expected probability of satisfying y. This yields the following definition:
Definition 3.1 (Safety estimates). For a given MDP M A,P. a given safety property y, and given number of steps, the optimistic and pessimistic safety estimate copt Cpes: SxN [0,

---

are defined as follows:
Vs S: Cope n) PM, M, ns, and vs E S: epes n) P (s n).
For state action pair (s, a) and a bound n, the maximal expected probability of satisfying ip from state s after executing a is
ss E S. E A eopo
(P(s,,, E s'ES
eopt(s', n- 1)).
Based on the estimates, the algorithm classifies undetermined states from S. as verified safe and adds them to S, or classifies them as unsafe and adds to the set of failure states Sy (Lines 4 and 5). A state 8 E S satisfies the safety objective (4, 5,p) if epes (8, 12) 2 6Ø. Note that the pessimistic safety estimate is achieved in execution that chooses the most unsafe actions in each non-restricted state. Thus, if for a given state (pee(s 2 6. then P. PM= n) 2 be holds. This highlights the strength of our algorithm: by assuming the worst policy behavior in unrestricted states, we provide verification results without sampling the policy in every state. A state E S is unsafe if Copt (s, n) S. dg. The optimistic safety probability is achieved in an execution that chooses the safest action in each non-restricted state. Thus, if copt n)) S و,,, the policy π cannot pick actions that would yield higher probabilities of satisfying yp from s.
Stopping criteria. In Line 7, the stopping criterion is defined via a user-defined threshold Eg for the minimal difference between the estimates. IMT stops if the difference between the optimistic and the pessimistic safety estimate is below the threshold ε. for all states, i.e., max, [aap (8, 1t)= (8, r2) < e.p- For small values of epss. further restricting the MDP would only marginally change the testing results. Otherwise, IMT continues with sampling the policy and restricting the MDP, as the optimistic and pessimistic estimates are sufficiently different. As an alternative stopping criterion, user could also define a total testing budget.
Importance ranking. In each iteration, IMT computes importance ranking over all states in the current MDP ( (Line 10). In the following steps, the most important decisions of the policy are sampled and used to restrict M1(), which results in refined estimates. The rank of a state reflects the maximal difference that a decision can have on satisfying the safety objective.
Definition 3.2. (Importance ranking for safety.) Given an MDP M = A, P,H). a safety property sp, and bound n, the importance ranking rank: S N R is given as the maximal difference between the optimistic estimates with respect to the available actions:
Vs S: rank(s, n) a,a' E.A
max (Cops a, eape (s n)).
For the importance ranking, we consider the impact of decisions on the optimistic estimates. That is, state s is important if, for some actions a and a', it holds that the expected maximal safety probability that can still be achieved after executing from is considerably larger than the probability that can be obtained after executing a' from s. The importance ranking returns the set of states Syank of the m highest ranked states of M
Sampling the policy. In Line 11, IMT samples the decisions of the policy in the highest ranked states E Srank of M This results in the set r = ((11,1)). ........ (Sm; pm)) with a; = π (s:)).
Restricting the MDP. In Line 12, our algorithm restricts ( according to the sampled policy's decisions, i.c., actions not chosen by æ in the sampled states are removed from M Given the current MDP (+) = (S, A, p((), pp))),)) 14) and the sampled state-action pairs T, the restricted MDP M (S, A, p(++1) 1), pu) has the following probabilistic transition function:
(P (s. $ Srank or (s,a) r else.
Ys, s' E Va E A: p(++)) (s,
0
In every iteration of the algorithm, more actions in the MDP model become fixed to the actions chosen by æ, leading to more accurate safety estimates for n, i.e., (s, monotonically increases and Copt (s. n) monotonically decreases, for all s E S.
Theorem 1. The algorithm IMT as described in Alg. 1 terminates.
Proof Sketch. For fully restricted MDP, for any E S, for any n. it holds that Cope n) (8 (5,11, v)). This holds because a fully restricted MDP is Markov chain that describes the policy completely. Hence the estimates are the same.
5

---

Algorithm 2 IMT with Clustering
Input: M, π. 0p)
Parameters: importance threshold 6;, testing fraction K, testing horizon n, 8p. Epp Output: S C S, S S S, Copt : R. Epes : + R
1: // Line 1 - are as Alg. 1
9: Srank -=IcomputeRankinngAAAA.
10: C *=-celusterStatesSS
6:)
11: (1), ... (9g), } f- executeTests(rr C,
12: M +- restrictMDP(MM (((1,))) (9c), 1(21))
Line 12 14 are in Alg.
3.2 Importance-driven Model-Based Testing with Clustering
In this section, we extend IMT by introducing clustering in Alg. 1. Fig. shows the high-level view of IMT including clustering. For problems with very large state spaces, sampling the agents in all highly-ranked states becomes too expensive. To tackle this scalability issue, we propose to cluster similar states and test only fixed fraction of the states in each cluster. By doing so, we balance the trade-off between accuracy and scalability: The fewer states from a cluster are tested, the higher the scalability of our testing approach. However, the likelihood that some unsafe behavior of the agent remains undetected increases. Clustering offers the additional advantage that similar states are grouped. Under the assumption that the agent implements policy that selects the same action in similar situations, IMT most likely detects unsafe behavior by sampling large enough fraction of each cluster. Alg. states the changes in the pseudo-code for IMT with clustering.
Clustering. In Line 10, after computing the importance ranking, IMT performs clustering on all states with an importance ranking value greater than some bound = rank(s.n.) States are clustered according to their state information and their importance value, i.e., we compute clustering assignment el S (o., 1] N. This gives partitioning of Srank into sets of states sharing the same cluster label. Note that any off-the-shelf clustering algorithm can be used to compute the clusters of states."
Executing tests. In Line 11, the behavior of the policy in the clustered states is evaluated. From each cluster, fixed percentage of states is randomly selected to be tested. To test state 8, the agent is executed from 8 for a certain number of steps. If the safety objective is violated during the execution, is marked unsafe and added Sy- Based on the testing results of the individual states assign verdicts to the clusters proposing a conservative evaluation of safety. Each cluster cj with a tested state s E Sy is assigned failing verdict U, FAIL. Consequently, all states s E oj are marked unsafe and added to Sy. Conversely, if a cluster ej does not contain a single tested state from Sy, it is assigned a safe verdict 1/y SAFE, and its states are added S,.
Restricting the MDP. In Line 12, IMT restricts M in all states that belong to a cluster cj by turning the states into sink states. Additionally, a cluster has the verdict vj = FAIL, all states considered safety violation.
The effects of clustering. Since IMT with clustering only tests a fraction x of each individual cluster, the size and quality of the computed clusters affect the testing process. Clusters that are too large can lead to unnecessary testing efforts, as safe behavior might be deemed unsafe due to conservative evaluation. Additionally, if cluster contains states that are not sufficiently similar, IMT with clustering may fail to detect unsafe behavior in the policy.
Complexity Analysis. We discuss the computational complexity of single iteration of IMT. The safety estimates are computed via value iteration in Opoly(( (size(M)) n)) with n being the bound for the objective [3]. The computation of the ranking only requires sorting of the computed estimates and thus requires O(S) log (S]) time. The subsequent restriction of M is linear the number of actions present in M, i.e. ([S)) [Al). Lastly, the complexity of sampling the policy is dependent on the network architecture and the costs for clustering the state space depend on the chosen algorithm.
For vision-base state spaces, deep clustering approaches could be used [26].

---

(a) GridWorld.
(b) Results for TT
(c) Results for m2-
Figure 2: Slippery Gridworld example: setting (left), visualization of evaluating (middle), and (right).
IMT Sy
MT Syl
IMT
MT
150
Est. Probability
# Failed Tests
150
# States
100
100
0.5
50
50
0
50
100
150
0
50
100 150
500
1,000
Policy Queries
Policy Queries
Policy Queries
(a) Verified States.
(b) Average safety estimates.
(c) Results for random testing.
Figure Slippery Gridworld example: Evaluation results of m2.
4 Experimental Evaluation
All details of the experimental setup can be found in Appendix A. We provide the implementation and tested policies as supplementary material. We compare IMT with our model-based approach without importance ranking (MT) and model-free random testing (RT) as baseline. Thus, in MT, our algorithm restricts the MDP by the sampled agent's decisions and computes Copt and Epes to provide evaluation results on the entire state space but samples the policy randomly. For RT, the policy is executed from random states for a certain number of steps. Any violation of the evaluation objective reported. We report the runtimes averaged over 10 runs for each experiment in seconds, unless indicated otherwise, as total time( STDev) / total time for computing the estimates(+: STDev) total time for querying the policy (+ STDev).
4.1 Slippery Gridworld
We performed our first experiment in the Farama Minigrid environment [27]. description of the environment and the RL training parameters are given in Appendix B. The Gridworld is depicted in Fig. 2a. The agent has to reach the green goal without touching the lava. The lava is surrounded by slippery tiles, stepping
which carries predefined probability of slipping into lava. The size of the state space |S] x 7 x 196, with 49 cells multiplied by for the different orientations of the agent. The safety objective requires the agent to not enter the lava with a probability 5, 2 1.0.
RL training parameters. We trained policies тi and Te by utilizing a DQN. We used sparse reward function with a reward of 1 for reaching the green goal and -1 for falling into the lava. We trained कi using fixed initial state and π2 using initial states uniformly sampled from S.
IMT/MT parameters. We used a horizon of n = oc, a minimal difference of E = 0.05, a number of samples per iteration of m 10. For IMT. states with a ranking value close to 0 were sampled.
Visualizing IMT. Fig. visualizes the iterations of our IMT algorithm when evaluating क.. Per iteration, the picture on the top visualizes the highest-ranked states, with the intensity of the color capturing the ranking. Note that a state represents the (æ., y) coorrdinntss of the grid and the orientation of the agent and is thus visualized as a triangle. Per iteration, IMT samples gı in the highest-ranked
7

---

15y1-
[8.
[S.
[5.)
State
Paicy Eioo
20k
Failing States
6k
# States
10k
4k
2k
Ok
Ok
Ok
10k
20k
0.1 0.25 0.5 0.75 1.0
Policy Queries
(a) UAV Reach-Avoid setting.
(b) Results for noise = 0.1
(c) Number of safety violations.
Figure 4: UAV Task: setting (4a). verified states (4b), and number of identified safety violations (4c).
states (blue triangles) and computes the estimates. The pictures the bottom show the updated sets of verified states after computing the estimates: Sg is visualized in green, Sy in red, and S, in иi were sampled. IMT terminates
blue. Brighter colors represent states in which the decisions after 5 iterations when evaluating IT Note that the evaluation iteratively reveals the area in which TT violates safety. Fig. 2c visualizes the evaluation of the policy πº. IMT terminates after a single iteration and positively verifies in all states in which the safety objective can be fulfilled.
Evaluation results. Fig. 3a plots the number of verified states when evaluating Ti. Solid lines represent IMT results, dashed lines represent MT, where green lines represent [S,]. red lines represent [Sy], and blue lines [. We repeated the analysis via MT 10 times: the shaded area represents the minimal and maximal values, and the dashed lines the average number of states. After sampling Ti only 33 times, IMT terminates with [S,] 145, |Syl = 51, and |S 0. Thus, IMT provides complete verification results of π over the entire state space with only 33 policy samples. In contrast, on average, MT verifies the entire state space after sampling the agent's decisions almost on the entire state space. Fig. 3b plots the values for the optimistic (green) and pessimistic (red) safety estimates for IMT (solid lines) and MT (dashed lines), averaged over all states, which show that the averaged estimates of IMT tighten faster than for MТ. Finally, we report the findings of RT in Fig. 3c when executing a test case for 10 steps. The results show the clear advantage of exploiting our testing approach. By utilizing testing with model checking, space contrast RT which only able to report a small number of states from which şp is violated.
obtain verification results on the entire state
Runtimes. The costs for computing the estimates per iteration are in the range of milliseconds. The total runtime to verify πi was 12.29(=0.7) 1.11(#0.10) 0.11(#0.01), with IMT and 25.62 (1.)22++18)//2 3.21 /0.41 with MT.
4.2 UAV Reach-Avoid Task
For the second set of experiments, test policies computed for drone navigation by Badings et al. [28]. We refer to this work for details regarding the policy and environment, which illustrated in. Fig. 4a. The task of the drone is navigate the goal location (green box). The safety objective y states that the drone must not collide with a building (grey boxes) and must stay within the boundaries with probability 6,3 2 0.95. The state space [S] comprises 25.517 states. The wind in the simulation affects the drone, which is modeled stochastically and controlled through the parameter 7..
IMT parameters. We used
500 samples per iteration, and Exp: above.
Evaluation results. Our testing approach IMT/MT was able to verify control policies computed under five difference noise settings of E {0.1, 0.25, 0.5, 0.75, 1.0} over the entire state space. Fig. 4c gives the number verified unsafe states per policy. All policies with 17 < 0.75 are verified safe in all states from which it is possible to behave safely (light red bars indicate states from which safety violations cannot be avoided). Even though the policies have been specially designed to be safe, IMT was able to find safety violations for policies with r 2 0.75. The policies showed unsafe behavior in 15 or 775 additional states, respectively, for which safe behavior would have been possible (dark bars). Fig. 4b shows the verification results for IMT and MT for v) 0.1. The test results for the policies with 7) 2 0.25 can be found in Appendix C. As before, adding importance-rankinn for sampling the policy decreases the number of required samples to verify the policy. We performed RT

---

Figure 5: The initial clustering and iterations the algorithm for an average cluster size 25.
with budget of 50.000 queries and maximum number of time steps per test case. Averaged over 10 runs, RT found 1120 (+76.29) failed test cases for the policy with 17 = 1.0 and 613 (+55) failed test cases for r) 0.75.
The runtimes for evaluating the policy are 269. 269.8 ((H.55) 73. ( (..1..1...001111111 0.02(+00.2) for IMT, and 1793 shows that for larger examples, adding importance-basse sampling significantly reduces the time needed to verify the policy.
Runtimes.
185.28(4:3.2) / /0.02 for MT for noise level of 0.2515 This
4.3 Atari Skiing
We have evaluated IMT with clustering. IMTc for short, by testing Iearned policy for Atari Sking [29]. In Skinng the player controls the tilt of the skies to reach the goal as fast as possible. The safety objective yp is to avoid collisions with trees and poles with probability of dG 2 1.0. A state describes the (x, position, the tilt E [1..8] of the ski, and velocity v E [0..5] of the skier. The state space S comprises roughly 2.2 10 states.
IMTU [8] RT Sale
IMTl By RT Falel
Tears Sale Stans
Textal Faltae States
Impliied Sode Statee
Implaa Pariune Stare
106
60k
60k
# States
40k
40k
10a
20k
20k
10"
0k
20k
40k
60k
25 50 150
25 50 100 150
Tests
Average Cluster Size
Average Cluster Size
(a) Verified States.
(b) Number of safe and failed tests.
(c) Number of states in the final clusters.
Figure 6: Atari Skiing Example: Evaluation results for the tested policy.
IMT parameters. We used time horizon of 200, minimal difference of 6, 0.05, and fraction k = 0.2 of tested states per cluster. The clusters have been computed using k-means for states with 6, 0.8 with a l to create average cluster sizes of ( E (25, 50, 100, 150).
Visualizing IMT. Fig. visualizes the initial clustering the highest-ranked states and the iterations of IMTc with average cluster size of ( 25. We show the results for states in which till = 4, ie. the skier aligned with the slope, and a = The visualization for different values of tilt and can be found in Appendix E. We depict states from which the policy has been tested with lighter colors. Darker colors depict implied results. The results show that the agent robustly learned to avoid collisions (it avoids any collision as long as it is not placed too close to an obstacle).
Evaluation results. We evaluated IMTc using different values for Ç and compared with IMT, ie. Ç = 1, and RT. Fig. 6a plots the total number of failure states S, and safe states S, for the whole state space over the number of executed test cases for different values of Ç. The green curves (left to right) plot the results for S, using the cluster sizes (25, 50, 100, 150, 1). the red curves for Sy accordingly. For comparison, we executed RT 10 times and plot the average number of failing (orange dashed) and safe test cases (teal dashed), where the shaded areas show the minimal and

---

maximal values. The results show that IMTc terminates faster with smaller cluster sizes. Larger cluster sizes overapproximate unsafe regions more heavily. Thus, more testing effort is needed around the unsafe regions in the subsequent iterations. However, all instances of IMTc reduce the testing budget required compared to IMT, which was to be expected since only 20% of the states of each cluster were tested. These facts are also underlined by Figures 6b and 6c, which show the number of safe and failed tests, and the implied verdicts for cluster states in the final iteration, respectively. Fig. 6b shows that clustering heavily increases the scalability of our approach since it lowers the needed testing budget by up to a factor for Ç 25.
The runtimes for evaluating the policy, excluding the time needed to render the testing results, for Ç E {25, 50, 100, 150} are 86 minutes (=8.3) 40 (#4.5) / 8.5 (#2.3). Evaluating the policy for = took 127 minutes / 59 (+7.3) 35.9 (+4.4).
Runtimes.
5 Conclusion & Future Work
We presented importance-driver testing for RI. agents. The process iteratively (1) ranks the states based on the influence of the agent's decisions on the expected overall safety, (2) samples the DRL policy under test from the ranking, and (3) restricts the model of the environment. By utilizing probabilistic model checking, our algorithm provides upper and lower bounds on the expected outcomes of the policy execution across all modeled states in the state space. These estimates provide formal guarantees about the violation or compliance of the policy to formal properties. We presented an extension of the basic algorithm by introducing clustering to increase scalability. In future work, we will adapt IMT to allow the testing of stochastic policies by adapting the restriction of the MDP and the verification procedure. We will Furthermore, we will introduce several abstraction techniques to further increase the scalability of our approach. Finally, we will use recently proposed approaches to both learn discrete models of domains that continuous in both their state and action spaces increase the applicability of IMT and learn the MDP online during the training phase of the policy.
Bettina Könighofer and Stefan Pranger were supported by the State Government of Styria, Austria Department Zukunftsfonds Steiermark, Martin Tappler was supported by the WWTF project ICT22- 023. and Hana Chockler was supported in part by the UKRI Trustworthy Autonomous Systems Hub (EP/V00784X/1), the UKRI Strategic Priorities Fund to the UKRI Research Node on Trustworthy Autonomous Systems Governance and Regulation (EP/V026607/1), and CHAI EPSRC Hub for Causality in Healthcare AI with Real Data (EP//Y28856/1) ). We thank both Antonia Hafner and Martin Plank for their proof-of-concept implementations of the experimental evaluation.
References
[1] H.-n. Wang. N. Liu, Y.-y. Zhang, D.-w. Feng. F. Huang, D.-s. Li, and Y.-m. Zhang, "Deep rein- forcement learning: survey." Frontiers of Information Technology & Electronic Engineering. vol. 21, no. no. 12. pp. 1726-1744, 2020.
[2] B. R. Kiran, I. Sobh, V. Talpaert, P. Mannion, A. Sallab, S. K. Yogamani, and P. Pérez, "Deep reinforcement learning for autonomous driving: A survey," IEEE Trans. Intell. Transp. Syst. vol. 23, no. 6. pp. 4929, 2022.
[3] C. Baier and J. Katoen, Principles of Model Checking. MIT Press, 2008
[4] M. Landers and A. Doryab, "Deep reinforcement learning verification: A survey," ACM Comput. Surv, vol. 55, jul 2023.
[5] H. Pouget, H. Chockler, Y. Sun, and D. Kroening, "Ranking policy decisions," in Advances in Neural Information Processing Systems 34: Annual Conference on Neural Information Processing Systems (NeurIPS), pp. 8702-8713, 2021.
[6] R. S. Sutton and A. G. Barto, Reinforcement learning - an introduction. Adaptive computation and machine learning, MIT Press, 1998.
[7] A. Heuillet, F. Couthouis, and N. Díaz BädziRodrgguez "Explainability in deep reinforcement learning," Knowledge-Bais Systems, vol. 214, p. 106685, 2021.
[8] S. Milani, N. Topin, M. Veloso, and Fang, "Fxplainable reinforcement learning: A survey and comparative review," ACM Comput. Surv., 2024.
10

---

[9] M. Uehara, C. Shi, and N. Kallus, "A review of off-policy evaluation in reinforcement learning." arXiv preprint arXiv:2212.063355, 22.22550 2022.
[10] Y. Chandak, S. Niekum, B. da Silva, E. Leamed-Miller, E. Brunskill, and P. S. Thomas, "Universal off-po evaluation," Advances in Neural Information Processing Systems, vol. 34, pp. 27475-27490 2021.
[11] N. Jiang and L. Li, "Doubly robust off-policy value evaluation for reinforcement learning"" in International conference on machine learning, pp. 652-661, PMLR, 2016.
[12] J. Uesato, A. Kumar, C. Szepesvári, T. Erez, A. Ruderman, K. Anderson, K. D. Dvijotham, N. Heess, and P. Kohli, "Rigorous agent evaluation: An adversarial approach to uncover catastrophic failures," in 7th International Conference on Learning Representations, ICLR 2019, 2019.
[13] M. Biagiola and Tonella, "Testing of deep reinforcement learning agents with surrogate models," CoRR, vol. abs/2305. 12751, 2023.
[14] Q. Pang, Y. Yuan, and S. Wang, "Mdpfuzz: testing models solving markov decision processes," in ISSTA '22: 31st ACM SIGSOFT International Symposium on Software Testing and Analysis, ACM, 2022.
[15] A. Zolfagharian, M. Abdellatif, L. C. Briand, M. Bagherzadeh, and R. S, "A search-based testing approach for deep reinforcement learning agents," IEEE Trans. Software Eng., vol. 49, no. 7. pp. 3715-3735, 2023.
[16] M. Tappler, F. C. Córdoba, B. K. Aichernig, and B. Könighofer, "Search-based testing of reinforcement learning," in Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, IJCAI 2022, 2022.
[17] Z. Li, X. Wu, D. Zhu, M. Cheng. S. Chen, F. Zhang, X. Xie, L. Ma, and J. Zhao, "Generative model-based testing on decision-maaing policies," " in 38th IEEE/ACM International Conference on Automated Software Engineering, 2023.
[18] M. Gerhold and M. Stoelinga, "Model-basee based testing of probabilistic systems." in Fundamental Approaches Software Engineering 19th International Conference, FASE 2016. 2016.
[19] F. Den Hengst, V. François-Laved M. Hoogendoorn, and F. van Harmelen, "Planning for poten- tial: efficient safe reinforcement learning," Machine Learning, vol. 111, no. 6. pp. 2255-2274 2022.
[20] J. Song, X. Xie, and L. Ma, "SIEGE: A semantics-guided safety enhancement framework for ai-enabled cyber-physical systems." IEEE Transactions on Software Engineering, vol. 49, no. pp. 4058-005888 2023.
[21] M. Alshickh, R. Bloem, R. Ehlers, B. Könighofer, S. Nickum, and U. Topcu, "Safe reinforcement learning via shielding," in Proceedings of the 32th AAAI conference on artificial intelligence, 2018.
[22] W.-C. Yang, G. Marra, G. Rens, and L. De Raedt, "Safe reinforcement learning via probabilistic logic shields," in Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence, IJCAI-23 (E. Elkind, ed.), pp. 5739-5749, International Joint Conferences on Artificial Intelligence Organization, 8 2023. Main Track.
[23] D. C. McNamee and H. Chockler, "Causal policy ranking," CoRR, vol. abs/211 0tis/2111.000 1.08155, 2021.
[24] Gerasimou, F. Eniser, A. Sen, and A. Cakan, "Importance-driven deep learning system test- ing." in Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering, pp. 702-713, 2020.
[25] M. I.. Puterman, Markov decision processes: discrete stochastic dynamic programming. John Wiley & Sons, 2014.
[26] Y. Ren, Pu, 7. Yang, Xu, Li, X. Pu, P.S. Yu, and I.. He, "Deep clustering: A comprehen- sive survey," CORR, vol. abs/2210.04142. 2022.
[27] M. Bnevalier-Boisverr I.. Willems, and S. Pal, "Minimalistic gridworld environment for gym- nasium," " 2018. https///ithub..co/faaaaa htwpa////eooooaaaaaooaaaoaaaannn
Foundation/Minigrrd..
[28] T. S. Badings, I. Romao, A. Abate, D. Parker, H. A. Poonawala, M. Stoelinga, and N. Jansen, "Robust control for dynamical systems with non-gaussian noise via formal abstractions." Artif. Intell. Res., vol. 76, pp. 341-391, 2023.

---

[29] E. Beeching, "Trained policy for atari skiing." http:s/hnnggnniiiieewwweeeeehnnn _ atari skiing 1111 This work licensed under the Apache 2 license.
[30] S. Pranger, B. Könighofer, L. Posch, and R. Bloem, "TEMPEST synthesis tool for reactive systems and shields in probabilistic environments," in Automated Technology for Verification and Analysis, ATVA 2021, 2021.
[31] A. Raffin, A. Hill, A. Gleave, A. Kanervisto, M. Ernestus, and N. Dormann, Staale-baseliness" Reliable reinforcement learning implementations. Journal of Machine Learning Research, vol. 22, no. 268. pp. 1-8, 2021.
[32] V. Mnih, K. Kavukcuoglu, D. Silver, A. A. Rusu, J. Veness, M. G. Bellemare, A. Graves, M. Riedmiller, A. Fidjeland, Ostrovski, al., "Human-level control through deep reinforcement learning," Nature, vol. 518, no. 7540, pp. 529-533, 2015.
A General Experimential Setup
All experiments have been executed on a desktop computer with 3.9GHz Intel i5-8265U CPU and 16GB of RAM using single worker, i.e. we did not any form of multithreading.
We implemented our importance-driven testing framework in Python and used the probabilistic model checking tool Tempest [30] to compute the estimates and the importance ranking.
B Details for the Gridworlds Experiments.
In this section, we give the details of the experiments in Section 4.1 and Appendix D.2.
Environmental Details. The agent behaves in the style of an omnidirectional robot. It is able to perform seven actions: Moving forward, turning left, turning right, picking up objects, dropping the object being carried, interacting with doors or other objects, and idlying. The slippery tiles in 2a introduce stochastic behaviour. the agent tries to move forward on slippery tile, it only manages to move to its intended tile in front of it with probability of 3 Otherwise, it slips
with probability of J to either the adjacent tile its left or its right, respectively,
with a probability of to either the tile to the left or to the right of the tile in front of the agent, respectively.
The tiles belonging to one-way streets in 8a, depicted by a blue arrow, do not allow the agent to move against the direction of the one-way. This especially means that agent is not allowed enter one-way from the wrong side.
RL Training Details. We used standard implementation of DQN from wable-baselines! [31] with a CnnPolicy. The network to classify and train the agent follows standard approach taken from [32]: It features convolutional layers and a linear activation layer. The learning parameters have been slightly altered with the following modifications:
discount factor y,: 0.95
exploration scheme: A linear decay from 0.7 0.01 over the first 90% of the learning duration.
The agents for policies T1, T2, Ts. and have been trained with total number of 500000 steps. An episode lasted maximum number of 100 timesteps or ended prematurely the agent caused safety violation or if it reached the goal.
12

---

C Additional Results for UAV Reach-Avoid Experiment
DMT
MT Sy
DMT
MT 15
1NT (S2) MI 18.) MT IS.)
DMT [S.
NI1 1S.
IMT 8
IMT (8.)
MT 18.
20k
20k
States
States
10k
10k
0k
0k
0k
10k
20k
Ok
10k
20k
Policy Queries
Policy Queries
(a) Results for noise 0.25
(b) Results for noise 0.5
IMT S1)
MT 15g
IMT (8)
MT 18
18T [5.
MT 18
13T [S NIT 18
IMT MT
[NT MI 18.
20k
20k
# States
# States
10k
10k
0k
0k
0k
10k
20k
0k
10k
20k
Policy Queries
Policy Queries
(c) Results for noise 0.75
(d) Results for noise 1.0
Figure 7: Evaluation results for the UAV Reach-Avoid task under noise levels 0.25, 0.5, 0.75 and 1.0.
7
0.1
0.25
0.5
IMT
269sec.
(#5.5)
320sec. (+16.1) 2227sec. (=.2))
1264sec. (+3.8)
MT
1793sec. (#21.7)
2570sec. (=125.4)
Y
0.75
IMT
1383sec. (+444)
2422sec. (#3.87) 4016sec. (1.6233
MT
2844sec. (+34.3)
Table 1: Average synthesis times for the different policies.
D Testing for Performance
In this section we discuss the necessary background and definitions needed adapt IMT for testing for performance.
Model checking of performance objectives. Model checking be used to compute the expected accumulated reward for all states and actions in M. In particular, for a given MDP M, policy n and reward function R S IR, it computes the following values:
E R S x N + R gives the expected accumulated reward in M from state within n steps. M. (s, m)) = max EE R n) gives the maximal expected accumulated reward over all policies II from state s within steps.
Emin (s, n) min EM R (2,, n) gives the minimal expected accumulated reward over all
policies in II from a state s within n steps.
performance objective (R. 8R) is defined over the reward function and threshold 8R that defines the lowest-acceptabl expected accumulated reward over n steps.
13

---

10
(b) Selected results for iterations i 0, 10, i 14 of
Map of area in Barcelona.
testing ms-
Figure 8: Urhan navigation example: setting (left) and visualization of evaluating स3 (right).
Failed Test Instances
Estim. Performance
400
400
50
300
# States
200
0
200
50
100
0
100
50
100
150
0
50
100
150
#
1,000
2,000
Policy Queries
Policy Queries
Policy Queries
(a) Verified States.
(b) Average safety estimates.
(c) Results for random testing.
Figure Urban navigation example: Evaluation results of IT.
Definition D.1 (Performance objective). Given an MDP M = (S, p1), reward function R R. and a threshold 5R E R. A policy satisfies the performance objective (R, (R) from given state s E S within a given number of steps n if
R. (8, EM
2 8R.
D.1 Importance-driven Performance Testing
IMT can be easily adapted to evaluate policy for performance objectives. To tailor Alg. for performance testing, we provide as inputs a performance objective (R. 8R), and minimal difference in performance ER between optimistic and pessimistic estimates. These inputs replace the corresponding safety-relater parameters ip, 8,p. and Ep. The performance estimates (Line 3) are defined by:
Definition D.2 (Performance estimates). For given MDP M = A, A, p), a reward function R. S R. and given number of steps, the optimistic and pessimistic performance estimate R, Pes,R S x N R are defined as follows:
Vs E S: (s,t, n) EM (s. n), and Vs E S: epe,, (M,
For the optimistic performance estimate, the computation assumes that the policy т selects the action that maximizes the expected reward in each unrestricted state. Conversely, for the pessimistic estimate, the assumption is that the least optimal actions concerning the reward are chosen. A state S satisfies the performance objective (R, δअ) if épea, R (s, 2 गR (Line 4). A state E S violates the performance objective Copt, (s, S 6R (Line 5).
For the stopping criterion, the difference between performance estimates is compared to ER (Line 7).
D.2 Urban Navigation Task
modeled part of Barcelona Minigrid environment as illustrated Fig. 8a. The size of
the state space is |S| 426. The agent's task is to navigate to Sagrada Família (within 100 steps), while respecting the traffic rules, i.e., not driving against the one-ways. We trained and evaluated two policies ø3 and J4.
14

---

RL training parameters. and Ty were trained utilizing DQN, The agent is given the reward of 1 for reaching the goal and additionally -0.01 per step. Both policies have been trained using initial states uniformly sampled from |S].
IMT/MT parameters. We used the same parameters for the experiment in Section 4.1, but used m 15.
Visualizing IMT. Fig. 8b visualizes the sets of verified states for in selected iterations of Alg. 1. visualize S,, Sy. and S, in the same way as our first experiment. Brighter colors again represent states where тT sampled. IMT iteratively samples the agent's decisions at crossings ranked on the difference the decisions of the individual roads have on the total length of the path to Sagrada Família. Figures 10 and 11 visualize S., Sy. and S. for πΙ IMT needs 9 iterations to fully verify that T4 behaves optimally in any of the modelled states.
Evaluation results. Fig. 9a plots the number of verified states and Fig. 9b plots the estimates when evaluating T3- As above, we compare IMT and the average results for MT over 10 runs. Even though Ta performed well on large parts of the state space, IMT and MT identified wrong decisions at several crossings that do not allow the agent to reach the goal in time. For RT we executed т3 with a budget of 2000 policy queries and maximum number of 100 time steps. Fig. 9c plots the average number of identified violations. While IMT and MT only have to sample the agent's ' decisions at the crossings to verify the entire state space, RT average only found 13.25 (+2.75) states from which test case failed. Fig. 12a plots the number of verified states and 12b plots the estimates when evaluating TT.
Runtimes. The runtime to verify Ty was 36.79 sec (+2.0) with MT and 24.70 see (+2.2) with IMT. Both approaches MT and IMT needed similar total runtime of about 8.s.. (=:0.) to verify T4-
Figure 10: The intermediate results for iteration for the verification of Ia using IMT.
Figure 11: The intermediate results for iteration for the verification of .a using IMT.
15

---

Estim. Performance
400
50
#States
200
-50
100
0
50
100
150
0
50
100
150
Policy Queries
Policy Queries
(a) Verified States.
(b) Average safety estimates.
Figure 12: Urban navigation example: Evaluation results TT.
E
Additional Results for Atari Skiing Experiment
E.1 Results for = 25
Figure 13: The initial clustering and iterations of IMT for an average cluster size of 25, tilt 2, and v = 2.
Figure 14: The initial clustering and iterations of IMT for an average cluster size of 25, tilt 4, 4.
Figure 15: The initial clustering iterations of IMT for average cluster size of 25, tilt and 4.
16

---

Figure 16: The initial clustering iterations of IMT for average cluster size of 25, till 3.
Figure 17: The initial clustering and iterations of IMT for average cluster size of 25, till v 2.
E.2 Results for Ç 100
Figure 18: The initial clustering and iterations of IMT for an average cluster size of 100, till = 2, and 2.
Figure 19: The initial clustering and iterations of IMT for average cluster size of 100, tilt 4, and v 4.
17

---

Figure 20: The initial clustering and iterations IMT for an average cluster size 100, till 5, and V
Figure 21: The initial clustering and iterations of IMT for average cluster size of 100, filt 6, and
Figure 22: The initial clustering and iterations of IMT for an average cluster size of 100, tilt = 7, and v = 2.
1. Claims
Question: Do the main claims made in the abstract and introduction accurately reflect the paper's contributions and scope?
Answer: [Yes]
Justification: We present the first model- based testing approach that gives formal verification guarantees. We discuss the method detail and provide detailed evaluation in the form of several experiments.
Guidelines:
The answer NA means that the abstract and introduction do not include the claims made in the paper.
The abstract and/or introduction should clearly state the claims made, including the contributions made the paper and important assumptions and limitations. A No or
NA answer to this question will not be perceived well by the reviewers.
The claims made should match theoretical and experimental results, and reflect how much results can be expected to generalize to other settings.
is fine to include aspirational goals as motivation as long clear that these goals not attained by the paper.
18

---

2. Limitations
Question: Does the paper discuss the limitations of the work performed by the authors?
Answer: [Yes]
Justification: The method currently assumes that the policies under test are determinisitic, stated in the introduction. We will extend IMT test stochastic policies in future work.
Guidelines:
The answer NA means that the paper has no limitation while the answer No means that the paper has limitations, but those are not discussed in the paper.
The authors are encouraged to create a separate "Limitations" section their paper.
The paper should point out any strong assumptions and how robust the results are to violations of these assumptions (e.g., independence assumptions, noiseless settings, model well-specification, asymptotic approximations only holding locally). The authors should reflect on how these assumptions might be violated in practice and what the implications would be.
The authors should reflect on the scope of the claims made, e.g., if the approach was only tested on a few datasets or with a few runs. In general, empirical results often depend on implicit assumptions, which should be articulated.
The authors should reflect on the factors that influence the performance of the approach. For example, facial recognition algorithm may perform poorly when image resolution low or images are taken in low lighting. Or speech-to-tex, system might not be used reliably to provide closed captions for online lectures because it fails handle technical jargon.
The authors should discuss the computational efficiency of the proposed algorithms and how they scale with dataset size.
If applicable, the authors should discuss possible limitations of their approach to address problems of privacy and fairness.
While the authors might fear that complete honesty about limitations might be used by reviewers as grounds for rejection, worse outcome might be that reviewers discover limitations that aren't 't acknowledged in the paper. The authors should use their best judgment and recognize that individual actions in favor of transparency play an impor- tant role in developing norms that preserve the integrity of the community. Reviewers will be specifically instructed to not penalize honesty concerning limitations.
3. Theory Assumptions and Proofs
Question: For each theoretical result, does the paper provide the full set of assumptions and a complete (and correct) proof?
Answer: [NA]
Justification:
Guidelines:
The answer NA means that the paper does not include theoretical results.
All the theorems, formulas, and proofs in the paper should be numbered and cross- referenced.
All assumptions should be clearly stated or referenced in the statement of any theorems.
The proofs can either appear in the main paper or the supplemental material, but if they appear in the supplemental material, the authors are encouraged to provide a short proof sketch provide intuition.
Inversely, any informal proof provided in the core of the paper should be complemented by formal proofs provided in appendix or supplemental material.
Theorems and Lemmas that the proof relies upon should be properly referenced.
4. Experimental Result Reproducibility
Question: Does the paper fully disclose all the information needed to reproduce the main ex- perimental results the paper to the extent that affects the main claims and/or conclusions of the paper (regardless of whether the code and data are provided or not)?
19

---

Answer: [Yes]
Justification: We provide a docker image containing all the necessary data and code to reproduce the experiments. The README containing instructions on how to reproduce the and the docker image
results is available via https://igssaarecom///// http:/hhw.....ooooocccoooooaaaa3 can be downloaded from: https///iigsaar..com////// 108 181111104444444000555
Guidelines:
The answer NA means that the paper does not include experiments.
If the paper includes experiments, a No answer to this question will not be perceived well by the reviewers: Making the paper reproducible is important, regardless of whether the code and data are provided or not.
If the contribution is dataset and/or model, the authors should describe the steps taken make their results reproducible or verifiable.
Depending on the contribution, reproducibility can be accomplished in various ways. For example, if the contribution is a novel architecture, describing the architecture fully might suffice, or if the contribution a specific model and empirical evaluation, may be necessary to either make it possible for others to replicate the model with the same dataset, or provide access to the model. In general. releasing code and data often one good way to accomplish this, but reproducibility can also be provided via detailed instructions for how to replicate the results, access to a hosted model (e.g., in the case of large language model), releasing of a model checkpoint, or other means that appropriate to the research performed.
While NeurIPS does not require releasing code, the conference does require all submis- sions to provide some reasonable avenue for reproducibility, which may depend on the nature of the contribution. For example
(a) the contribution is primarily a new algorithm, the paper should make it clear how reproduce that algorithm. (b) If the contribution is primarily new model architecture, the paper should describe the architecture clearly and fully.
(c) If the contribution is a new model (e.g., a large language model), then there should either be way to access this model for reproducing the results or way to reproduce the model (e.g., with an open-source dataset instructions for how to construct the dataset).
(d) We recognize that reproducibility may be tricky in some cases, in which case authors are welcome describe the particular way they provide for reproducibility. In the case of closed-source models, it may be that access to the model is limited in some way (e.g., registered users), but it should be possible for other researchers to have some path to reproducing or verifying the results.
5. Open access to data and code
Question: Does the paper provide open access the data and code, with sufficient instruc- tions to faithfully reproduce the main experimental results, as described in supplemental material?
Answer: [Yes]
Justification: As stated above, we provide a docker image as artifact that contains all data and code reproduce the experiments.
Guidelines:
The answer NA means that paper does not include experiments requiring code.
Please see the NeurIPS code and data submission guidelines (https:/nips..c/ppblic
Suiide/Coaeeubmmssiiooooiii for more details.
While we encourage the release of code and data, we understand that this might not be possible, so No is an acceptable answer. Papers cannot be rejected simply for not including code, unless this is central to the contribution (e.g., for new open-source benchmark).
The instructions should contain the exact command and environment needed to run to reproduce the results. See the NeurlPS code and data submission guidelines (https: Wiingseepppiignnnsssooooibisssss
for more details.
20

---

The authors should provide instructions on data access and preparation, including how access the raw data, preprocessed data, intermediate data, and generated data, etc.
The authors should provide scripts to reproduce all experimental results for the new proposed method and baselines. If only subset of experiments are reproducible, they should state which ones are omitted from the script and why.
At submission time, to preserve anonymity, the authors should release anonymized versions (if applicable).
Providing as much information as possible in supplemental material (appended the paper) is recommended, but including URLs to data and code is permitted.
6. Experimental Setting/Details
Question: Does the paper specify all the training and test details (e.g., data splits, hyper- parameters, how they were chosen, type of optimizer, etc.) necessary to understand the results?
Answer: [Yes]
Justification: Each experiment is accompanied by paragraph stating the parameters chosen for our method IMT.
Guidelines:
The answer NA means that the paper does not include experiments.
The experimental setting should be presented in the core of the paper to level of detail that is necessary to appreciate the results and make sense of them.
The full details can be provided either with the code, in appendix, as supplemental material.
7. Experiment Statistical Significance
Does the paper report error bars suitably and correctly defined or other appropriate information about the statistical significance of the experiments?
Question:
Answer: [Yes]
Justification: Our method is designed verify a deterministic policy against safety objective with fixed threshold. The verification process is therefore not subject to random sampling and cannot report any statistical significance. For the comparison with random testing, we plot the variability over multiple runs. For evaluating the effect of clustering to increase scalability, values of ( and have therefore not statistically verified this.
have observed clear, and expected, trend in the results for different
Guidelines:
The answer NA means that the paper does not include experiments.
The authors should answer "Yes" if the results are accompanied by error bars, confi- dence intervals, or statistical significance tests, at least for the experiments that support the main claims of the paper.
The factors of variability that the error bars are capturing should be clearly stated (for example, train/test split, initialization, random drawing of some parameter, overall run with given experimental conditions).
The method for calculating the error bars should be explained (closed form formula, call to a library function, bootstrap, etc.)
The assumptions made should be given (e.g.. Normally distributed errors).
should be clear whether the error bar is the standard deviation the standard error of the mean.
It is OK to report 1-sigma error bars, but should state it. The authors should preferably report a 2-sigma error bar than state that they have 96% CI, if the hypothesis of Normality of errors is not verified.
For asymmetric distributions, the authors should be careful figures symmetric error bars that would yield results that are out of range (e.g. negative error rates).
show in tables or
If error bars are reported in tables or plots, The authors should explain the text how they were calculated and reference the corresponding figures tables in the text.
21

---

8. Experiments Compute Resourees
For each experiment, does the paper provide sufficient information on the com- puter resources (type of compute workers, memory, time of execution) needed to reproduce the experiments?
Question:
Answer: [Yes]
Justification: Each experimental accompanied by a paragraph stating the runtimes for each individual experiment. In A we state that each experiment has been conducted on consumer laptop, using single-threaded implementation.
Guidelines:
The answer NA means that the paper does not include experiments.
The paper should indicate the type of compute workers CPU or GPU, internal cluster, or cloud provider, including relevant memory and storage.
The paper should provide the amount compute required for each of the individual experimental runs well estimate the total compute.
The paper should disclose whether the full research project required more compute than the experiments reported in the paper (e.g., preliminary or failed experiments that didn't make into the paper).
9. Code Of Ethics
Question: Does the research conducted in the paper conform, in every respect, with the NeurIPS Code of Ethics http:://euiis..cpppiiiihhhhcuulp
Answer: [Yes]
Justification:
We are not in violation with the NeurIPS Code of Ethics.
Guidelines:
The answer NA means that the authors have reviewed the NeurIPS Code of Ethics.
If the authors answer No, they should explain the special circumstances that require deviation from the Code of Ethics.
The authors should make to preserve anonymity (e.g., .., if there is special consid- eration due to laws or regulations their jurisdiction..
10. Broader Impacts
Question: Does the paper discuss both potential positive societal impacts and negative societal impacts of the work performed?
Answer: [NA]
Justification:
Guidelines:
The answer NA means that there is no societal impact of the work performed.
If the authors answer NA or No, they should explain why their work has no societal impact or why the paper does not address societal impact.
Examples of negative societal impacts include potential malicious or unintended uses (e.g., disinformation, generating fake profiles, surveillance), fairness considerations (c.g., deployment of technologics that could make decisions that unfairly impact specific groups), privacy considerations, and security considerations.
The conference expects that many papers will be foundational research and not tied to particular applications, let alone deployments. However, if there is a direct path to any negative applications, the authors should point it out. For example, it is legitimate to point out that an improvement in the quality of generative models could be used to generate deepfakes for disinformation. On the other hand, is not needed to point out that a generic algorithm for optimizing neural networks could enable people to train models that generate Deepfakes faster.
The authors should consider possible harms that could arise when the technology is being used as intended and functioning correctly, harms that could arise when the technology being used as intended but gives incorrect results, and harms following from (intentional unintentional) misuse of the technology.
22

---

If there are negative societal impacts, the authors could also discuss possible mitigation strategies (e.g., gated release of models, providing defenses in addition attacks. mechanisms for monitoring misuse, mechanisms to monitor how system learns from feedback over time, improving the efficiency and accessibility of MI.).
11. Safeguards
Question:
Does the paper describe safeguards that have been put in place for responsible release of data models that have a high risk for misuse (e.g., pretrained language models, image generators, or scraped datasets)?
Answer: [NA]
Justification:
Guidelines:
The answer NA means that the paper poses no such risks.
Released models that have high risk for misuse or dual-use should be released with necessary safeguards to allow for controlled use of the model. for example by requiring that users adhere usage guidelines or restrictions to access the model or implementing safety filters.
Datasets that have been scraped from the Internet could pose safety risks. The authors should describe how they avoided releasing unsafe images.
We recognize that providing effective safeguards challenging, and many papers do not require this, but we encourage authors to take this into account and make best faith effort.
12. Licenses for existing assets
Question: Are the creators or original owners of assets (c.g., code, data, models), used in the paper, properly credited and are the license and terms of use explicitly mentioned and properly respected?
Answer: [Yes]
Justification: We have used two different existing assets, namely a policy from huggingface, which is attributed in our references and licensed under Apache 2, and the policies for the SWV-Reech-Avoid-Taaee -ask. The latter have been computed using the source code which available on Github: http://tthbbcoo///AAAAAAABBB
Guidelines:
The answer NA means that the paper does not use existing assets.
The authors should cite the original paper that produced the code package or dataset.
The authors should state which version of the asset used and, if possible, include a URL.
The name of the license (e.g., CC-BY 4.0) should be included for each asset.
For scraped data from a particular source (e.g.. website). the copyright and terms of service of that source should be provided.
If assets are released, the license, copyright information, and terms of use in the package should be provided. For popular datasets, paperswithcode. www.:ithcoode.om/aattaaaaaaaa com/datasets has curated licenses for some datasets. Their licensing guide can help determine the license of dataset.
For existing datasets that are re-packaged, both the original license and the license of the derived asset (if it has changed) should be provided. If this information is available online, the authors are encouraged to reach out the asset's 's creators.
13. New Assets
Question: Are new assets introduced in the paper well documented and is the documentation provided alongside the assets?
Answer: [NA]
Justification:
Guidelines:
23

---

The answer NA means that the paper does not release new assets.
Researchers should communicate the details of the dataset/code/mooel as part of their submissions via structured templates. This includes details about training, license, limitations, etc.
The paper should discuss whether and how consent obtained from people whose asset is used.
At submission time, remember to anonymize your assets (if applicable). You can either create an anonymized URL or include an anonymized zip file.
14. Crowdsourcing and Research with Human Subjects
Question: For crowdsourcing experiments and research with human subjects, does the paper include the full text of instructions given to participants and screenshots, if applicable, as well details about compensation (if any)?
Answer: [NA]
Justification:
Guidelines:
The answer NA means that the paper does not involve crowdsoureing nor research with human subjects.
Including this information in the supplemental material is fine, but if the main contribu- tion of the paper involves human subjects, then as much detail as possible should be included in the main paper.
According the NeurIPS Code of Ethies, workers involved in data collection, curation, or other labor should be paid at least the minimum wage in the country of the data collector.
15. Institutional Review Board (IRB) Approvals or Equivalent for Research with Human Subjects
Question: Does the paper describe potential risks incurred by study participants, whether such risks were disclosed to the subjects, and whether Institutional Review Board (IRB) approvals (or an equivalent approval/review based on the requirements of your country or institution) were obtained?
Answer: [NA]
Justification:
Guidelines:
The answer NA means that the paper does involve crowdsourcing nor research with human subjects.
Depending the country in which research is conducted, IRB approval (or equivalent) may be required for any human subjects research. If you obtained IRB approval, you should clearly state this in the paper.
We recognize that the procedures for this may vary significantly between institutions and locations, and we expect authors to adhere to the NeurlPS Code of Ethics and the guidelines for their institution.
For initial submissions, do not include any information that would break anonymity (if applicable), such the institution conducting the review.
24


Reviews:
[{"review_id": "R7ZZBqBTGr", "reviewer": "Reviewer_nWP9", "summary": "The paper proposes an algorithm (IMT) to test a deterministic policy in finite MDPs where a model of the MDP is available. The primary contributions of the paper are algorithmic and empirical. IMT works by iteratively partitioning the state space into safe, unsafe or undetermined. Using the MDP model, IMT is able to construct optimistic and pessimistic bounds on the property being tested (e.g., safety). These estimates are used to identify the states with the largest gap in their optimistic estimates between any pair of actions. IMT prioritizes testing these states next, which has the effect of tightening the bounds and taking the largest possible step towards convergence and halting. The final result includes a partitioning of the state space into safe and unsafe states, which is valuable feedback for improving the policy (offline). The paper also includes a clustering-based variant to scale the algorithm to larger MDPs. Experiments on 3 domains demonstrate the utility of IMT against a random baseline and a variant which does not rank the states.", "questions": "- What is the exact implementation of `computeEstimates`? How does it scale with the size of the input (restricted) MDP? Similarly, how exactly is $e_opt(s, a, n)$ estimated?\n\n- What steps are involved in adding a new domain from scratch? How easy or hard is it to create the simulator, specify the CTL objective, etc.?\n\n- Is it feasible to quantify or conduct investigations into how AMT might handle noise in the transition function in the current experimental setup?\n\n- What is the precise definition of a robust policy in Line 195?\n\n- What is the computational cost of the clustering approach used here? Should it be reflected in the complexity analysis in Lines 214 - 219?\n\n- How does the quality of the resulting clusters affect performance? Does Alg 2 degrade gracefully as cluster quality decreases?\n\n- Is it necessary to use a different mechanism (sink states) to restrict the MDP when clustering? How does terminating the trajectory at the sink state affect the e_opt, e_pes estimates, if at all? Does the approach still work if the restriction mechanism from Alg 1 is used?\n\n- Does it make sense to compare safety-violation detection rates against other baselines (MDPFuzz, STARLA)?\n\n- Does it make sense to consider continuous state and / or action MDPs using this framework? If yes, what modifications might be needed to make it work on cMDPs?", "limitations": "Yes", "rating": 6, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 2, "strengths": "+ The paper studies the important problem of verifying black-box policies used in control applications. This is an important question as RL-learned controllers are deployed more widely. Advances here are likely to be of significant interest to the community.\n\n+ The paper is well written. The main ideas, algorithms, ideas and experiments are generally explained clearly. Although some important implementation details are missing, the paper is nevertheless easy to read.\n\n+ The proposed algorithm is intuitively clear and using the estimates to identify \"important\" states to test next seems to work well. In cases where a model of the discrete MDP is available (or perfectly learnable), this seems like a useful technique to rigorously test a policy and uncover states where the policy does not behave safely. The experiments and appendices include a good amount of detail.", "weaknesses": "- The paper does not provide sufficient detail on important algorithmic implementation details. Examples include the prerequisites for the algorithm (simulators, CTL), implementation of `computeEstimates`, $e_opt(s, a, n)$, clustering similarity/distance function, etc.\n\n- The assumption of a correct model of the MDP is a somewhat large one in many domains. A discussion of the effort needed to obtain such a model would improve the paper and make its applicability to new domains clearer. Additionally, exploring the use of noisy simulators with varying levels of noise in the dynamics would be really interesting to see. As the paper mentions in Line 331, being able to leverage models of the environment learned from data is likely to increase the applicability. However, these are likely to include noisy dynamics so an experimental evaluation of the impact of noisy dynamics in the current experimental setup would have strengthened the paper.\n\n- A comparison to stronger baselines would make it easier to assess the empirical contributions of the paper. Currently, the only comparison is to random testing. Comparing safety-violation detection rates against black-box policy testers (e.g., MDPFuzz, STARLA) using the same budget would have helped place this paper in the larger body of work on DRL testing as well as understand the applicability of these techniques in domains with different characteristics (size, model availability or learnability, etc.).", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We thank the reviewer for the detailed evaluation of our paper. We believe that our proposed testing framework has the potential to significantly impact testing for DRL. Although testing DRL is intrinsically challenging, the problem has only recently garnered attention from the testing community. Currently, there is no common framework for RL testing methods, and most papers explore search-based strategies. Our paper is the first to introduce model-based testing into the DRL setting, a method that has proven highly relevant in many other domains and we believe has much potential also in the DRL setting.\n\n## Q1: Details on computation of estimates, scalability, and what is estimated.\n\nThe optimistic and pessimistic estimates are computed using the probabilities $ P^{max} $ and $P^{min}$, which define the expected maximal and minimal probability to satisfy a property $\\varphi$, respectively (see definition 3.1 paper). These probabilities can be computed with standard algorithms for solving MDPs. Many tools allow to compute these probabilities efficiently using various algorithms, e.g., using sound value iteration (SVI) [1], a dynamic programming approach, or a translation into a linear program. Thus, the estimates are computed using exact probabilities, when sound algorithms are used.\nThe core of SVI is the iterative computation of the probabilities using the transition matrix of $M^i$. The complexity therefore scales polynomially with the number of states. The powerful tool support in the community allows to compute these probabilities for MDPs with tens of millions of states efficiently [2].\n\n[1] Quatmann et al. “Sound Value Iteration”\n\n[2] Katoen. “The Probabilistic Model Checking Landscape”\n\n## Q2: Steps for adding a new domain.\n\nOur framework requires an MDP model of the environment and a CTL specification. The work involved in adding a new domain mostly amounts to creating an MDP. That is, you need knowledge about the environment dynamics on an abstract level. Most probabilistic model checkers accept inputs expressed in the symbolic modeling language PRISM [3]. For simulation, we generally rely on a gymnasium-like interface with a step and a reset functionality.\nThe objectives specified in CTL are relatively easy to define. For safety, it is generally sufficient to define events that must not happen. We also refer to our global rebuttal.\n\n[3] Kwiatkowska. “PRISM 4.0: Verification of Probabilistic Real-time Systems.” \n\n## Q3: Consequences of noise in transition relation.\n\n\nIMT is only little affected by noise in the transition probabilities: the noise might only change the order in which states are tested. Let’s assume that from a certain state, a transition wrongly underrepresents the probability of traversing to an unsafe state. Our testing framework might then assign a lower rank to this state. However, if our algorithm is executed until convergence, the state will eventually be tested.\nOur approach benefits from being a testing framework, with its primary task being the automatic selection of test cases. Even if the MDP model used to select the next test cases is not perfect, our approach will likely still identify interesting test cases. We thank the reviewer for this question and will emphasize the robustness of our approach against noise in the paper.\n## Q4: Definition of a robust policy in Line 195.\nWe consider a policy to be robust if small changes in the input do not significantly change the chosen action. We mention this when discussing the testing approach with clustering: The intuition is that if we assume that the states in the cluster are similar and the policy makes similar decisions in similar states, testing only a fraction of the states within each cluster yields good testing results.\n## Q5: Costs for clustering.  \nFor the complexity analysis, we focused on the steps of the approach proposed in the paper. We refrained from including clustering because it is problem-dependent. However, as we applied k-means, which scales very well, we found that its runtime is negligible in practice. \n## Q6: Impact of the clusters' quality on performance  \nLow-quality clusters can lead to an unnecessarily large testing effort or missed unsafe behavior. \n\nConsider the case when a cluster is identified as unsafe: If the cluster is too large and includes states that are actually safe, our iterative testing framework will needlessly cluster and test the predecessor states of the cluster. For example, in the context of skiing, our framework would end up testing states that are not critical for avoiding collisions with trees or poles. Now, consider a scenario where all states in a cluster are deemed safe: If the clustering method groups states that are not sufficiently similar, our testing approach may fail to detect unsafe behavior in the policy.\nPlease note that we provide verification results (guarantees that any unsafe behavior will be detected) only when no clustering is used.\n## Q7: Necessity and impact of sink states.  \nYes, it is necessary to adapt the restriction of the MDP in Alg2.\nIf a single state of a cluster is assigned a failing verdict, we mark all states of this cluster as failing states and turn them into sink states. This allows the generalization of testing results to whole clusters, increasing scalability since not all states of a cluster need to be queried. \nTerminating the trajectories at the sink states in clusters generally decreases the values of both estimates. By following a conservative approach, we consider all states in a cluster as unsafe if even one state is assigned a failing verdict. As a result, the estimates of the MDP with sink states are generally smaller than they would be in the unrestricted MDP. We will add a discussion to the paper.\nTo use the approach from Alg1, test executions for all states in a cluster would be necessary, which contradicts the goal of minimizing the testing budget.\n## Q8 and Q9\nWe refer to our answer in the global 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": "", "extra_scores": {}}, {"review_id": "Vl2z0bQk0g", "reviewer": "Reviewer_ak3E", "summary": "This work looks into the RL testing problem. RL policies are complex and hard to understand in terms of safety and performance. This work aims to test the policies via states in which the agent’s decisions have the highest impact on the expected outcome. This paper proposes a model-based method to compute a ranking of state importance and focus the testing on the highest-ranked states. The evaluation covers multiple benchmarks and shows that this approach can find unsafe policies.", "questions": "1. How is the ranking computed? Do you cover continuous space?\n2. What’s the scalability of this approach? Are there any cases where testing fails?", "limitations": "The limitations are not discussed in the main test.", "rating": 4, "confidence": 4, "soundness": 2, "presentation": 3, "contribution": 2, "strengths": "1. RL testing is important and few works touched on this.\n2. The idea of using the highest impact states to test the policies is interesting and seems effective.", "weaknesses": "1. The guarantee about the correctness of the ranking does not seem to be clarified. Do you iterate over all the actions in the action set? What if the action space is large and continuous?\n2. The testing is based on probabilistic model checking instead of worst-case checking. It would be good to bring out this in the abstract and introduction explicitly.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We appreciate the reviewer’s interest in our idea of guiding DRL testing through an importance ranking. We also agree that there is a current lack of testing methodologies for DRL. Additionally, considering the many potential extensions of our approach, we believe our method could significantly impact the development of DRL testing strategies. As it is the first paper that brings model based testing into DRL, we hope it will inspire follow up research.\n\n## Question - Computation and correctness of the ranking (W1)\n\nThe optimistic and pessimistic estimates are computed using the probabilities $P^{max}$ and $P^{min}$, which define the expected maximal and minimal probability to satisfy a property $\\varphi$, respectively (see definition 3.1 paper). These probabilities can be computed with standard algorithms for solving MDPs. Many tools allow to compute these probabilities efficiently using various algorithms, e.g., using sound value iteration (SVI) [1], a dynamic programming approach, or a translation into a linear program. Thus, the estimates are computed using exact probabilities, when sound algorithms are used to compute the probabilities. Hence, if the MDP model is accurate, the provided estimates are exact.\n\nTo compute the ranking, we indeed iterate over all the actions in the action set (we are currently not considering continuous action spaces. With our current approach, we would need to discretize the action space).\nThe rank of a state s is given as the maximal difference between the optimistic estimates with respect to the available actions ($max_{a,a′} (e_{opt}(s, a, n) − e_{opt}(s, a′, n))$. $e_{opt}(s, a, n)$ is computed using the probabilities $P^{max}$.\n\nFor a detailed discussion about the definition of the ranking, please see our answer to Q1 of  reviewer xBae.\n\n## Question -  Scalability \n\nBeing based on probabilistic model-checking, which internally uses value iteration,  the test-case generation scales to tens of millions of states in the MDP that serves as the test model [2]. \n\nPlease note that the size of the environment under test can be far larger. In model-based testing, a common strategy for large and complex systems is usually to create different models that capture different aspects of the system under test. Furthermore, to test for safety, it is often sufficient to consider abstract MDP model with a reduced feature space. States in an MDP typically encompass all relevant features of an agent and its environment. States then become vectors of feature values, where each combination of these constitutes a state. Not all features may be relevant to safety, though. By disregarding any features irrelevant to safety, the original model can be pruned to a\nmuch smaller model. Retaining the safety-relevant dynamics of the environment allows the use of model-based techniques for high-dimensional environments.\n\nThus, it is often possible to construct MDP models with a manageable size (tens of millions of states are fine) that are suitable for safety testing, even if the environment under test is continuous or very high dimensional. This concept is also deployed in other areas like enforcing safe exploration during training via shielding [3]. As soon as such an MDP is available, our testing approach can be deployed. \n\n\n## Question -  Continuous states and actions spaces\n\nWe refer to our answer in the global rebuttal.\n\n## Question - Are there any cases where testing fails?\n\nWhen using the approach in Section 3.1, our approach provides verification guarantees: Thus, after our testing framework terminates, the policy is verified to adhere to the safety requirements.\nAs soon as clusters are used, the formal verification guarantees are lost, and unsafe behavior might be missed, even if the algorithm terminates. The advantage of using our testing approach is that similar states are clustered: Thus, states close to a certain safety hazard are clustered together and the agent's behavior with respect to this hazard is tested several times (even if not exhaustively). Unsafe behavior is only missed if all tested states within a cluster are found to be safe, but there is an untested state within the cluster from which the agent selects an unsafe action.\nNote that as soon as we detect a single unsafe behavior in a cluster, all states in the cluster are marked as unsafe. \n\n[1] Quatmann et al. “Sound Value Iteration”\n\n[2] Katoen. “The Probabilistic Model Checking Landscape”\n\n[3] Jansen et al. ”Safe Reinforcement Learning Using Probabilistic Shields”", "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": "", "extra_scores": {}}, {"review_id": "ZMIg7T55R6", "reviewer": "Reviewer_sLgt", "summary": "This paper presents a framework called importance-driven model based testing for RL models.  ​ It uses a model-based approach to compute estimates of safety based on the MDP explored so far using the policy and ranks the importance of states based on the impact of decisions on safety.  Then it samples the policy on these state to further restrict the MDP. ​ The framework provides formal verification guarantees and partitions the state space into safe and unsafe regions. ​ The authors also propose a version to cluster similar states to further reduce the number of samples but at the cost of a relaxed guarantees. Experimental evaluations on different environments of various sizes demonstrate its effectiveness in reducing number of samples needed compared to random sampling both with and without the model. ​", "questions": "- How can number of policy queries in Fig 3c be greater than the number of states in the environment? \n\n- For runtimes, it will also be useful to break it down into model checking and policy sampling times for both IMT and MT approaches. \n\n- Please add legends to Figure 3", "limitations": "The authors briefly talk about limitation about the requirements of the current approach, but they could definitely expand a bit more on these limitations early on the paper.", "rating": 6, "confidence": 4, "soundness": 4, "presentation": 3, "contribution": 3, "strengths": "- **Relevance**: Policy testing is an important area of research in reinforcement learning.\n- **Novelty**: The paper introduces a novel algorithm that uses model-based approaches to reduce sample complexity while providing strong guarantees.\n- **Soundness and clarity**: The experiments are thorough. The results clearly illustrate the system's effectiveness and are presented clearly with appropriate images and plots. Figure 2, in particular, best illustrates the effectiveness of this system.", "weaknesses": "Some of the weaknesses of this paper are:\n- The approach relies on very strict assumptions on having a model for the environment with fixed set of states and actions, which could be very restricting for real world RL tasks. \n\n- The introduction and abstract could better motivate and establish the problem. Currently, they only explain the algorithm without much context. For example, it is not clear how the safety estimates are computed until sections 2 and 3 or why computing them iteratively is easier than sampling the action on every state.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We thank the reviewer for the detailed evaluation of our paper and for seeing the relevance of our proposed testing approach. We believe that our approach has the potential to significantly impact testing for DRL and hope that it will lead to additional interesting follow up research. In the following, we will address the mentioned weaknesses and answer the questions posed.\n\n\n## Q1: How can the number of policy queries in Fig 3c be greater than the number of states in the environment?\nOne of the significant advantages of our model-based testing approach is that we only need to sample the policy once per test case, as the model immediately provides information about the safety of the selected action (including induced safety risks in the following steps).\n\nThis is not the case in random testing. Since random testing does not have a model in the background, it cannot measure the induced safety risks of a particular decision. Thus, we sample the policy and simulate the environment for multiple steps. This is the predominant approach in (software) testing, where a system is executed for a predetermined number of steps in order to reveal defects encountered along the way.\n\nHence, for every test from a selected state, we query the policy several times. \n## Q2: Breaking down the runtimes into times for model checking and policy sampling and Q3: Add legends to Figure 3\nFor both Q2 and Q3 we thank the reviewer for the comment and will extend the paper to make the requested adjustments.", "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": "", "extra_scores": {}}, {"review_id": "ydngjENh9E", "reviewer": "Reviewer_xBae", "summary": "This paper proposed a novel model-based importance-driven framework for testing trained DRL policies. By focusing on testing the cases with higher importance ranks, the proposed framework improves the testing scalability. The evaluation of several case studies demonstrates that the proposed framework can more efficiently discover unsafe policy behavior with low testing effort.", "questions": "1. The importance ranking is based on the maximal difference between the optimistic estimates concerning the available actions, which considers the impact of decisions on the optimistic estimates. Why not use the pessimistic estimate, as it is more concerned about safety violations?", "limitations": "No", "rating": 5, "confidence": 3, "soundness": 2, "presentation": 3, "contribution": 2, "strengths": "1. The paper is well-structured and easy to follow. \n2. The idea of testing on important samples is interesting.", "weaknesses": "1. The definition of the safety formula $\\phi$  and the formula for calculating $\\mathbb{P}\\_{\\mathcal{M}^\\pi, \\phi}$ should be stated clearly.\n2. The current framework depends on several human-defined thresholds, for instance, $\\delta_{\\phi}$, $\\epsilon_{\\phi}$ $\\delta_{i}$. How those parameters are determined and sensitive to the final testing result should be discussed more clearly.\n3. The current framework is shown to be applicable in a discrete state and action space. It would be nice to see the discussion on the potentials and limitations applied to the continuous state and action space.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We thank the reviewer for finding our testing approach interesting. We believe our method could significantly impact the development of testing strategies for DRL and hope that it will lead to interesting follow up research. We will answer the questions and address the mentioned weaknesses in the following.\n\n## Q1. Why is the importance ranking based on the maximal difference between the optimistic estimates? Why not use the pessimistic estimate, as it is more concerned about safety violations?\nTo evaluate the safety of executing action a1​ in state s0​, we must assess the safety of any state s1​ that can be reached from s0​ via a1​. To avoid sampling the agent’s policy in s1​ and subsequent states, we can either assume the agent follows the safest policy (using $P_{max}$​) or the least safe policy (using $P_{min}$​). Here, we justify why our testing framework uses $P_{max}$​ ($e_{opt}$) rather than $P_{min}$ ($e_{pes}$) to assess safety.\n\nUsing $e_{opt}$:\nIf for a given state s0​, there exist actions a1 and a2 with a large difference in the maximal expected probability of satisfying $\\varphi$, this state will be highly ranked.\n\nSuppose we want to evaluate how safe it was to take action a1 in s0. Assume the transition (s0,a1,s1) occurs with high probability and s1​ has a high optimistic estimate. In this case, there exists a safe policy from s1​ (which the agent could choose to follow). Thus, entering s1​ was not safety-critical since any safety issues could be avoided from s1​.\n\nFurther, assume that if the agent selects action a2​ from s0​, the transition (s0,a2,s2) occurs with high probability and s2 has a low optimistic estimate (i.e., it is not possible to execute a safe policy from s2 anymore). In this scenario, state s0 is highly ranked as it is crucial to choose action a1 over a2.\n\nUsing $e_{pes}$:\nThe pessimistic estimate does not have this property since it is based on the minimal expected probability of satisfying $\\varphi$. Due to the possibility of reaching unsafe states from most states, the difference between actions a1​ and a2​ does not reflect the impact of the action choice on mitigating a safety violation as the optimistic estimate does. This leads to similar rankings for most states.\n\nConsequently, we would need to test any state from which the agent could cause a safety violation. For example, in a skiing scenario, even if the agent is far from any object, we would still need to test the state even if from any successor state, crashes can still easily be avoided. This is exactly what we want to avoid.\n\nOnce we have sufficiently restricted the environment MDP, the pessimistic estimate becomes more informative. It can then identify candidate states that have not been tested and from which unsafe areas cannot be entered. This is highlighted in lines 151 to 155.\n\n## W1: Clearly state the safety formula $\\varphi$ and the formula for calculating the probabilities\nWe consider objectives in the safety fragment of computation tree logic (CTL) [1]. This allows us to express objectives like: $AG \\neg collision$, which says that “on all paths (A) globally (G) no collision should occur”. We will add such an example in the paper.\n\nThe probabilities used in the paper ($P^{max}$, $P^{min}$ for MDPs, P for Markov Chains) can be computed using standard algorithms for solving MDPs. Many tools allow to compute these probabilities efficiently (like PRISM, STORM, or TEMPEST) using various algorithms, e.g., using sound value iteration (SVI) [2]], a dynamic programming approach, or a translation into a linear program. Thus, the estimates are computed using exact probabilities, when sound algorithms are used to compute $P^{min}$ and $P^{max}$.\nThe core of SVI is the iterative computation of the probabilities using the transition matrix of $M^i$. The complexity therefore scales polynomially with the number of states in the MDP. The powerful tool support in the community allows to compute these probabilities for MDPs with tens of millions of states efficiently [3]. We will point this out more clearly in the paper.\n[1] C. Baier and J. Katoen, “Principles of Model Checking”.\n\n[2] T. Quatmann et al. “Sound Value Iteration”\n\n[3] J. Katoen, “The Probabilistic Model Checking Landscape”\n\n## W2:  Selection and sensitivity to the parameters.\nWe thank the reviewer for the comment. While we think that the used parameters are quite natural, we agree that a discussion of the selection and the effects of the parameters will improve the paper. \n\n$\\delta_\\phi$: The probability of visiting an unsafe state should be below some threshold $\\delta_\\varphi$. This threshold is part of the safety specification.  For example, the $P (AG \\neg collision) <= \\delta_\\varphi$. The higher the threshold, the fewer risks the agent is allowed to take. Extreme cases: if $\\delta_\\varphi = 1$, the framework classifies an action as unsafe if there is any risk that safety will be violated. If $\\delta_\\varphi = 0$, any behavior is safe.\n\n$\\epsilon_\\phi$: IMT stops if the difference between the optimistic and the pessimistic safety estimate is below this threshold for all states. Thus, the smaller this threshold is selected, the more test cases have to be executed until the algorithm terminates, but the more accurate is the estimated expected probability of the agent's policy to satisfy safety. \n\n$\\delta_i$: When using clustering, we want to cluster highly ranked states. Thus, this threshold defines the states that will be clustered and potentially tested. The lower the value, the more states will be clustered and potentially tested. The chosen value for $\\delta_i$ in the skiing experiment is $0.8$ (Line 297) since this value successfully excludes states that are far from any potential safety critical states. We apologize for not using the defined variable. \n\n## W3: Continuous states and action spaces.\nWe will add a paragraph to discuss this extension. Please also see our answer in the global 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": "", "extra_scores": {}}, {"review_id": "qAPENkrdNP", "reviewer": "Reviewer_4erK", "summary": "This paper proposes a model-based method for testing the safety properties of Deep Reinforcement Learning (DRL). The method computes a ranking of state importance across the entire state space, dividing the state space into safe and unsafe regions. The approach provides optimal test-case selection and guaranteed safety by providing formal verification guarantees over the entire state space. The method is evaluated on several examples, showing it discovers unsafe policy behavior with low testing effort.", "questions": "In general, the idea of ranking the importance of the state and leveraging it as the testing guidance is very interesting. I believe this work would have a certain impact on the further development of DRL testing. \n\nThere are a few technical points unclear.\n\n1. Page 2, Line 60. It would be good if the authors gave a more concrete concept of the formal guarantee provided by IMT, like probabilistic certification.\n\n2. Page 5, Line 175. What do you mean by \"significantly larger\"? Do you perform statistical testing here?\n\nMoreover, some related work is missing:\n\n- Gerasimou, Simos, Hasan Ferit Eniser, Alper Sen, and Alper Cakan. \"Importance-driven deep learning system testing.\" In Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering, pp. 702-713. 2020.\n- Song, Jiayang, Xuan Xie, and Lei Ma. \"$\\mathtt {SIEGE} $: A Semantics-Guided Safety Enhancement Framework for AI-enabled Cyber-Physical Systems.\" IEEE Transactions on Software Engineering (2023).\n- Shi, Ying, Beibei Yin, and Zheng Zheng. \"Multi-granularity coverage criteria for deep reinforcement learning systems.\" Journal of Systems and Software 212 (2024): 112016.", "limitations": "Yes, the authors address it in the guideline.", "rating": 7, "confidence": 5, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "+ The paper introduces a novel method to rank state importance across the entire state space, which further assist the testing procedure.\n+ The use of optimistic and pessimistic safety estimates provides a range of expected outcomes and is interesting\n+ The authors conduct a detailed evaluation of the method on several popular DRL tasks and demonstrate its effectiveness.", "weaknesses": "- Some technical details should be explained more clearly.\n- The authors doesn't compare IMT with the SOTA DRL testing method, like [15] mentioned by the authors in the paper.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We thank the reviewer for finding our idea of guiding DRL testing through an importance ranking interesting. Given the current lack of testing methodologies for DRL and the numerous potential extensions of our approach, we believe our method could significantly impact the development of testing strategies for DRL. We will address the identified weaknesses, especially we will clarify the technical details. Please also see the global rebuttal, where we address the comparison to other baselines.\n\n## Q1: Concept of formal guarantees\n\nWe agree that the provided formal guarantees should already be stated clearly in the introduction. We will amend this in the introduction. \n\nIn Section 3.1. (Lines 149-158), we explain the provided formal guarantees:\n\nThe estimates provide lower and upper bounds on the expected outcomes of the policy execution across all modeled states in the state space.\nIf the optimistic estimate violates a safety objective, then the policy is guaranteed to violate the safety objective, i.e., the probability that the safety CTL formula is satisfied using the agent’s policy is lower than the defined safety threshold.\nOn the other hand, any safety objective assured by the pessimistic estimate are formally proven to hold for the policy, i.e., the probability that the safety CTL formula is satisfied using the agent’s policy is greater or equal than the defined safety threshold.\n\nWe will give a similar explanation in the introduction. \n\n## Q2: “significant” difference (Line 175). Are you performing statistical testing? \n\nThe values for $e_{opt}(s,a,n)$ and $e_{opt}(s,a',n)$ are directly computed using sound value iteration which yields exact probabilities. Thus, we are not performing statistical testing. \n\nWe consider a state important if the maximal difference for two distinct actions is substantially larger than 0, i.e. if the decision of the agent has an important impact on the expected probability to ensure safety.  We apologize for the misleading phrasing. We will rephrase this and clarify it in the camera-ready version.\n\n## Other Comments - Related Work\n\nWe thank the reviewer for giving us pointers to related work. We will include all three references in the related work section.\nHighly relevant are [1] and [3]. [1] defines importance over the most-important neurons and tests the behavior of the most important neurons. In contrast, we define the ranking over the environment states, from which the policy should be explored. [3] is relevant since they are the first that discuss coverage criteria for DRL testing. \nAdditionally to comparing to other testing frameworks for DRL, we compare with approaches that combine model-based formal methods with model-free RL. [2] is clearly relevant in that regard, as they are combining DRL and model learning to design controllers that satisfy STL properties.\n\n[1] Gerasimou, Simos, Hasan Ferit Eniser, Alper Sen, and Alper Cakan. \"Importance-driven deep learning system testing.\"\n\n[2] Song, Jiayang, Xuan Xie, and Lei Ma. \"SIEGE: A Semantics-Guided Safety Enhancement Framework for AI-enabld Cyber-Physical Systems.\"\n\n[3] Shi, Ying, Beibei Yin, and Zheng Zheng. \"Multi-granularity coverage criteria for deep reinforcement learning systems.\"", "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": "", "extra_scores": {}}]

Author rebuttal:
We sincerely thank the reviewers for their valuable feedback. Our paper introduces model-based testing to the reinforcement learning setting.  Since this is the very first paper in that direction, we agree with the reviewers that there are numerous intriguing directions yet to be explored, such as continuous state and action spaces. We hope that this work will inspire future research in model-based testing for deep reinforcement learning (DRL).

In this global rebuttal, we aim to address the questions and concerns raised by multiple reviewers.

## The approach relies on the assumption of having an MDP model of the environment.

We agree that needing an MDP model of the environment may be considered a hurdle toward the adoption of model-based testing (MBT). Indeed, it is often perceived as such in industrial applications of MBT for testing of conventional software. However, experience reports [1,2] from industry reveal benefits resulting from the activity of modeling software systems and their environments beyond just enabling test-case generation.  The benefits include a better understanding of the system, environment, and requirements. The model commonly resolves ambiguities and helps to communicate between different stakeholders. It also opens venues for other activities such as the verification of temporal properties. In RL, environmental models enable safe exploration during training via techniques like shielding. Furthermore, the application areas of neurosymbolic AI are constantly growing, utilizing the same concept of combining model-based symbolic AI (e.g., to guarantee safety) with subsymbolic AI (e.g., to achieve high scalability and performance). Additionally, the software engineering community showed several successful applications of model learning to create test models automatically, thus circumventing manual modeling.  
This paper is the first to introduce MBT into the testing of reinforcement learning. In line with related model-based techniques in other areas, we believe the benefits—such as using the model to select the most important test cases, reducing the number of policy samples, and computing estimates over the entire state space—outweigh the drawback of needing a model.



[1] Emil Alegroth et al. “Practitioners’ best practices to Adopt, Use or Abandon Model-based Testing with Graphical models for Software-intensive Systems”, Empirical Software Engineering (2022) 27: 103

[2] Robert V. Binder et al. “Model-Based Testing: Where Does It Stand?”, COMMUNICATIONS OF THE ACM (2015), 58: 2

## Extension to continuous state and action spaces

Indeed, extending our framework to environments with continuous state and action spaces is possible, and we plan to pursue this as our next step. We plan to learn abstract finite-state models of the environment. To automatically learn such a model, we are currently evaluating two potential approaches: (1) Compute an abstract state-space of the MDP model representation through dimensionality reduction and clustering of observed environmental states. The stochastic transitions are learned via a combination of active and passive model learning, as proposed in [5].
(2) Apply world model learning via neural networks, as in DreamerV3 [4], from which we extract finite-state models via quantized bottleneck insertion as in [3]. 
In this paper, we provide the first step: We introduce the notion of importance-driven testing and show its potential via the Atari Skiing game. To handle continuous domains, we will apply importance rankings in abstract environment models. We believe that the learned MDP models will be sufficiently precise to compute good importance rankings across all states, thereby identifying critical situations that need to be tested. Thus, we believe our method will evolve into a valuable testing method for intricate control policies in complex environments. 

[3] Anurag Koul et al. "Learning Finite State Representations of Recurrent Policy Networks"

[4] Danijar Hafner et al. "Mastering Diverse Domains through World Models" 

[5] Martin Tappler et al. "Learning Environment Models with Continuous Stochastic Dynamics"

## Comparison to stronger baseline 

A comparison to existing search-based testing is difficult for two reasons. (1) There is no common framework for RL testing methods yet. For example, MDPFuzz only fuzzes the initial states, while STARLA creates complete episodes that must end in a terminal state. Therefore, our approach would be hardly comparable due to the difference in setting. (2) A fair comparison would likely need to go beyond safety-violation detection rates, which has been the focus of existing work, toward more comprehensive criteria. For example, STARLA might create different test cases for the same failure states, i.e., different episodes that traverse a common subset of states. As a result, STARLA might have an artificially high failure-detection rate, although certain states are covered multiple times, which we strictly avoid. In our comparison to random testing, we check how many of the failure states are found, which is not easily enforceable in the meta-heuristic search performed by STARLA. 
Hence, we need suitable quality metrics for test cases in RL, which we are currently exploring in addition to model learning. Note that quality metrics (called adequacy criteria in software testing) and test-case selection criteria are two sides of the same coin, thus our approach presents a step toward defining proper quality criteria.

Meta-review: The paper introduces a novel technique for safe RL leveraging differentiable NN verification tools. The algorithm uses the $\alpha,\beta$-crown verification method. 

The reviewers agreed that the approach is novel, and the authors addressed their main concerns during the rebuttal phase. The main concern was the assumption of having an environment model at hand. Nonetheless, it seems to be the first successful application of Model-Based Testing in RL; there are numerous applications where the world model is accessible.

I therefore accept the paper for the NeurIPS conference.
 
In the final version of the paper, please include the discussion on the neural network-controlled systems, the missing related work, and the additional benchmarks and clarifications provided in the response to the reviewers.
Decision: Accept (poster)