Safety Verification of Decision-Tree Policies in Continuous Time
Authors: Christian Schilling
Anna Lukina
Emir Demirović
Kim Guldstrand Larsen
Venue: NeurIPS 2023 spotlight (2023)
Keywords: safety verification
decision tree
reinforcement learning
controller
continuous time
TL;DR: We present the first approach to safety verification for continuous-time decision-tree policies.

Abstract: Decision trees have gained popularity as interpretable surrogate models for learning-based control policies. However, providing safety guarantees for systems controlled by decision trees is an open challenge. We show that the problem is undecidable even for systems with the simplest dynamics, and PSPACE-complete for finite-horizon properties. The latter can be verified for discrete-time systems via bounded model checking. However, for continuous-time systems, such an approach requires discretization, thereby weakening the guarantees for the original system. This paper presents the first algorithm to directly verify decision-tree controlled system in continuous time. The key aspect of our method is exploiting the decision-tree structure to propagate a set-based approximation through the decision nodes. We demonstrate the effectiveness of our approach by verifying safety of several decision trees distilled to imitate neural-network policies for nonlinear systems.

Safety Verification of Decision-Tree Policies in Continuous Time
Christian Schilling
Anna Lukina TU Delft Delft, The Netherlands a lukina@tudelft. nl
Aalborg University
Aalborg, Denmark
chr peristianss@ca aau. dk
Emir Demirović
Kim Guldstrand Larsen
TU Delft
Aalborg University Aalborg, Denmark kg10cs .wa..aaa.... dk
Delft, The Netherlands e, demirovii@tudelffe .nl
Abstract
Decision trees have gained popularity as interpretable surrogate models for learning- based control policies. However, providing safety guarantees for systems controlled by decision trees is an open challenge. We show that the problem is undecidable even for systems with the simplest dynamics, and PSPACE-complete for finite- horizon properties. The latter can be verified for discrete-time systems via bounded model checking. However, for continuous- tottinuuuu-tmeeeeeee systems, such an approach requires discretization, thereby weakening the guarantees for the original system. This paper presents the first algorithm directly verify decision-tree controlled systems in continuous time. The key aspect of our method is exploiting the decision- tree structure to propagate set-based approximation through the decision nodes. We demonstrate the effectiveness of our approach by verifying safety of several decision trees distilled to imitate neural-network policies for nonlinear systems.
Introduction
Deep reinforcement learning has shown success in deriving control policies for nonlinear systems for which classical optimal control theory provides no solution [Mnih et al. 2013). Despite impressive performance, there are key drawbacks: (i) the resulting policy is difficult to interpret, and (ii) there are no guarantees that the system always reaches the desired goal and avoids unsafe states. The interpretability challenge has led review of decision trees as well-performing, compact, and transparent surrogates for deep neural networks [Asho et al.) 2020 2019) David et al. 2015) Alamdari et 2020 Vos and Verwer 2023]. To provide safety guarantees, prior work proposed to encode a discrete, tmme-boudde system controlled by decision-tred policy set of logical constraints Bastani 20188. However, this approach does not apply to continuous cietiuuuuu--mmeeee dynamics.
To illustrate the problem, we consider a quadrotor system [Ivanov al.) 2019 in Figure [[a] where the task is to follow the brown reference trajectory from (0, 0) and stay within the blue dashed safety corridor. Illustrated schematically in Figure [[b) we may observe a trajectory that exhibits safe behavior for each discrete time point but leaves the safety corridor in between. Since the trajectory returns quickly enough, this violation is missed by a discrete-time analysis.
Example 1.
In this work, we address, for the first time, the problem of verifying safety (reach-avoid) properties of a decision-tree controlled system (DTCS) with (nonlinear) continous time dynamics. We propose an algorithm that exploits the structure of the decision-tree policy and propagates sets of reachable states,
37th Conference on Neural Information Processing Systems (NcurIPS 2023).

---

time
(b) Discrete-time analysis may miss property violations of con- tinuous systems. The threshold (dashed blue line) is breached for short time (red curve). which is detected the dis- crete time points (black dots).
inttal reference -boundary
0.
0.2
0.4
0.6
0.8
10
1.2
(a) Sketch the quadrotor system (arly plane) with sample trajectories.
Figure 1: A sketch of the quadrotor system and motivation for continuous-time analysis.
splitting at the decision boundaries. This way we obtain a sound enclosure of the true reachable states even for continuous dynamics, which guarantees safe goal reachability for all behaviors of the controlled system. Furthermore, our approach naturally generalizes to discrete-time systems, for which, compared to the aforementioned approach based on logical encoding [Bastani al. 2018). our approach provides visual interpretability of the verification process.
To summarize our contributions, we first provide an algorithm to verify a decision -tree policy of nonlinear continuous-time system. Our general algorithm parameterized two procedures for respectively analyzing the dynamical system and the policy. For these procedures, we formulate sufficient conditions for the algorithm be sound and relatively complete. Second, we describe an instantiation of the algorithm for nonlinear systems based on Taylor models [Berz and Makino 1998). In nutshell, this procedure propagates a set of states through the system dynamics. For analyzing the decision-tree policy, focus the common class of axis-aligned predicates ("xr < c")) and propose an instantiation that exploits this structure. Third, we show that the problem of verifying decision-tree policies is PSPACE-comples even for very simple (namely, state-independent dynamics. Finally, demonstrate that our algorithm can verify several werfforeemen--eeanniin benchmarks from classical control and the quadrotor from Figure I even for unbounded time.
1.1 Related Work
decision tree a popular machine-learning model that has recently regained interest due to its high interpretability (Du al. 2020) Decision-tree policies can be trained directly from tabular
dataset state-action pairs Quinlan 1996), c.g., using the CART algorithm [Breiman et al. 1984]
or dtControl [Asho et al.) 2020 Since these algorithms perform
equivalence transformation.
safety guarantees transfer from the dataset to the decision tree. Ashok et al. 2019 show how to extract safe-by-desipe decision tree from safe policy synthesized with Uppaal Stratego (David jet al. [013) for priced timed game. However, for nonlinear systems is generally unclear how policies. In practice one uses best-effort methods such reinforcement
to obtain learning. As these approaches cannot guarantee that the resulting policy is safe, there need for approaches to verify given policy after learning.
Decision trees can be trained imitate another model such as a neural network. For instance, the Viper algorithm incorporates decision-tree learning into the imitation procedure [Bastani et al.) 2018). As this imitation provides no correctness guarantees, a separate analysis is required. The authors encode the bounded-time reachability problem for discrete-time system in logical constraints. This encoding is the only verification approach for discrete-ting DTCS we are aware of. Other verification efforts for decision trees have focused robustness and adversarial examples in supervised setting (Urban and Miné 2021]. which are orthogonal problems to our setting verifying a policy.
For purely dynamical systems (without control policy), reachability analysis has been studied extensively [Doyen et al. 2018 Althoff al., (022T. One prominent approach based on Taylor models [Berz and Makino 1998), which we also employ in implementation. Combining

---

dynamical system with a control policy results in a hybrid system [Henzinger, 1996]. Applying tools for general hybrid-system verification DTCS not feasible because they do not exploit the specific structure (we discuss this further in Appendix D). The reach-avoid problem is undecidable for nonlinear dynamies (even without a control policy), and most approaches (including ours) consider only time-bounded analysis. However, as we discuss later, under certain conditions, our results still generalize to unbounded time via fixpoint techniques [Giacobbe| 2019 [acci et al. [021]. For piecewise-constane dynamics, axis-aligned policies resemble systems that can be efficiently dealt with using interval-based arithmetic constraint solving Fränzle et al. 2007 Fränzle and Herde 2007].
Closely related to DTCS are neural-netwote controlled systems (NNCS), where the policy is imple- mented by a neural network. Recently, many reachability approaches have been proposed [Dutta
et al. 2019
Tran et al. 22200] Fan et al., [2020] Akiintudde et al., [022] Ivanov et al. [221]] Schiiling
et al. 2022
Kochdumper et al. [023], and implementations compete a yearly competition [Lopez
et al.
2022
The main difference to DTCS is that the control action comes from a continuous domain
and the neural network implements a smooth function. Hence such policies typically yield a similar control action for similar states, which benefits set-based reachability analysis. In contrast, given two similar states, a decision tree can yield vastly different control actions. Thus tools for verifying NNCS are not applicable to our problem. NNCS are Turing-complete (Hyötyniemi 1996]. We show the same result for DTCS even with the simplest environment dynamics, which yields an undecidable problem in unbounded time and a PSPACE-complie problem in bounded time.
To summarize, decision-tree policies are highly desirable due to their interpretability. The most successful methods in obtaining such policies use machine learning, which do not guarantee safety of the resulting policy. While previous work managed to verify discrete-time policies, continuous-time policy verification remains an open problem. Our work bridges this gap with the first algorithm to verify decision-tree policies for continuous-time systems.
Outline. We organize the remainder of the paper as follows. First we formalize DTCS and the reach-avoid problem. Then we describe our verification algorithm and discuss the problem complexity. Next we report on experimental results. Finally we conclude and discuss directions for future work.
2 Preliminaries
2.1 Decision-Tree Treee Controlled Systems
Let C R be an n-dimensional state space and U/ C Rm an m-dimensional action (or input) space. A decision tree T over S and 2/ is binary tree such that each inner node is labeled with a predicate p: + B (with B = 1)) ) and each leaf is labeled with an action u E U. The nodes in the tree are organized in levels, with the root node being at level 1. Let rool(T) denote the root node of T, (T) resp. IT) denote the left resp. right sub-tree of T, and E(T) denote the label at the root of (i.e., if T is a leaf, L(T) is an action and otherwise a predicate). We can interpret T as function from S to 24 as follows. Given a state x E S, the image under T, written act recursively. For leaf T. (2t T) is just E(T). For proper tree with root predicate p. act(z, T) is act(x, (T) if p(z) = T, and (ct (T) otherwise. In this paper, we restrict our analysis to predicates of the form 2; I c where x; is the i-th state and e E R is constant. Geometrically, these predicates are axis-aligned half- salf--spaes. This class of predicates is commonly used, e.g., in the tools Uppaal Stratego (David et al.) 2015) (with industrial applications in control of smart homes [aasen et al. 2016 and traffic lights Eriksen et al. (017)) and dtControl [Ashok et al. 2020).
resp.
(ct( (z, T) E 24, is defined
We consider environments modeled by a system of ordinary differential equations (ODEs), à f(z, u). where xtt) E S is the state vector and u(t) e U is the vector of control actions. Given an initial state z0) Zo and an action uo. assume that the solution to the corresponding initial-valuc problem at time t 2 O, written {( ug, t, f). exists and is unique (c.g., by Lipschitz continuity).
A decision-tree controlled system (DTCS) is a triple (f, T,)) where f describes system of ODEs, T is a decision tree, used as policy, and sketch. The DTCS periodically queries the policy for a new control action. At time points kT, k E N, the current state x((7)) is passed to the policy T, which instantaneously yields the new control action :a: this action is then used for the next control period in the system dynamics f. Formally, given an initial state To at O, we recursively define the sequence of actions d = (x(k))))))) T), k E N. and the evolution of the state (t) = {Z((kT), uk, t KT, f) (i.e., a trajectory) for t E (KT, (k + 1)7].
IR + is a control period. Figure 2 shows a conceptual
3

---

clock ft = kT x(kr)
x(t)
Environment à far u)
Sampler
Decision-tree policy T
(c((T((kT::))
Figure 2: A decision-tree controlled system (f.
2.2 Reachable States and Reach-Avoid Problem
Given DTCS and set of initial states No S S, we are interested in the reachable states, either at time as R₂ {x(t) =00) E Xo) or the generalization time intervals R(To.Ti] UlE[To.2)) R2
Similarly, a discrete-time DTCS is a pair TJ where ʃ describes a recurrence 7k++1 = Fy+ (Tx ux) and T is a decision tree. The reachable states at step l are RR = {Ix Ih E Xo and analogously R1K UkE(Ko,Ai]
Rx. By default, DTCS refers to the continuous-time DTCS introduced above.
The reach-avoid problem for DTCS is, given a DTCS (f.T.7) over S, a set of initial states Ng S S, bounded number of control cycles kmax. and two sets G,E S S, to decide whether all trajectories a(t) reach the goal set 9 without reaching the error set & before time Tiax kmax i.c., 3t s Timx. z00) E Xo A z(t") G A Vt E [0, (0,t*] xxt) & E. If we assume that the goal states G are absorbing, this is equivalent to checking
RTI.: S G A R =
(1)
Example 2. Consider again the quadrotor model from Figure [ A full model description is given in Appendix B.I. The reach-avoid problem here consists of the shaded area at the top the goal set G. the set of states outside the red corridor as the error set E, and kmax = 30 control cycles.
Determining reachability is already undecidable for uncontrolled nonlinear dynamical systems (Hainry. 2008). and hence also for DTCS with nonlinear dynamics. A DTCS can be seen as hybrid conttte-conniuuuss) system, for which reachability is undecidable even with linear dynamics (mixed discrete-contee
(Doyn et al., 2018). Due to these complexity barriers, we aim at enclosing, or overapproximating. the reachable states up to time horizon max by computing a set R 2 R Rm..T.
3 Approach
In this section, we present our approach to reachability anal- ysis for DTCS. We first describe general high-level algo- rithm, which resembles standard reachability schemes for hybrid systems. is, however, tailored to policies over a finite action space U. As such, it is applicable to policies beyond decision trees, but for instance not to typical neural- network policies. We then outline conditions under which the algorithm is sound and relatively complete (i.e., does not introduce additional approximation errors). Finally, we in- stantiate the algorithm specifically for decision-tres tree policies, which is novel contribution of this paper.
Algorithm Reachability algorithm for DTCS
Input: DTCS (J,T,T), -). initial set Xo. time/cycle bounds T kmax
Output: set of states R 2 Rro.
1: R + Xo
2: Q + ((X,, 0))
3: while isempty(() do
4: (X' to) + pop(Q)
5: if ia Tmax then
6: continue end if
Algorithm T shows our high-level reachability method, which can be used to solve the reach-avoid problem (Sec- tion 2.2p. The algorithm is parametric two procedures, posty and post,- which together compute enclosure of the reachable states for one control cycle. The queue Q contains pairs (X,,)) where X' set of states that needs to be explored, and t is time point. Each iteration of the while loop (line analyzes one control cycle from and
7:
8:
41 min(lo + T, Tmax)
9:
for (Ku, u) post (X, 22,77 T) do
10:
(Y, Zr,) +
post (Zhrr u, f, (1)
11:
R-RUD
12:
pu, (Zi,,t)) (1))
13: end for
(unless the time horizon Tmux is reached, line 6 The result added to the set of reachable states in line Next we describe the requirements for the post procedures.
end while
15: return R

---

The procedure posty, which is new contribution of this paper, takes set of states A' and decision tree and returns a finite set of pairs (>r", uu), where y is a set of states and 2 is an action. Since multiple leaves of a decision tree can be associated with the same action u, we allow multiple sets D to be associated with u as well. For each action u, the union of the sets y should enclose the set act,, (X, T) {xr E X (z, T) = u.) so we have an index set Ta (possibly empty) for each action u such that
a T) S User. V".
Procedure posty wraps the sets y together with action u.
posty (x, - - wEU U Vel, {(37" u)}
For posty be sound, we connect equations (2 and (3) and untangle the pairing with u as follows:
Yu E u. Ut+ E y (VP) u) E posty((' T)) 2 act (Xt,
The procedure post, receives a set of states X, a control action the environment S. and a time interval [ f1]. (Note that actually only need the duration to, which is most of the time, because we consider time-invariant systems. We only pass the time interval for notational purposes to refer to t1-) The goal is to perform a classical
bounded reachability computation and return two sets y and such that y encloses the reachable states for the given time interval and 2 encloses the reachable states the final time point 4, Thus for post, to be sound, the following must hold:
posty(X, u, f. [to: til) = (1', 2) = y ((oo.1) A 2 Re,
(5)
Algorithm I in combination with equations 4 and (5) computes a sound enclosure. Let us write posty and post for the procedures such that the inclusions in equations (4) and ( are satisfied with equality. With such procedures, the algorithm even produces the exact result (proven in Appendix C.I).
Theorem 1 (Termination, soundness, relative completeness). Assume Eq. (4 and Eq. (5) are satisfied. (1) Algorithm terminates all calls to post, and post, terminate. (2) Let 3
=}.. The result
R of Algorithm encloses (2) resp. equals (=) the reachable states, R 3 R Ro,,Tall if in all steps post, (X, T) posty (X, T) and post ( u, f, [to,tt]) t,l) 2 posty (K u, f, [to til) hold.
3.1
Implementing the Post Procedures
For implementing post,, we use an algorithm based on Taylor models (Berz and Makino 1998] for reachability analysis of nonlinear dynamical systems. A Taylor model approximates a function as a polynomial together with an interval remainder over domain [Makino and Berz, 2003), which we interpret as sets of states. For exam- ple, the one-dimensional Taylor model with polynomial p(x) = x² - I + 1 and remainder [-0.5, 0.5] over the domain [- around expansion point 0 encodes the set {p(x) +r x E [-1, 1],
Algorithm 2 Post for the environment
Input: set X' control action environ-
ment f. interval [fo, tı]
Output: pair (2) 2) such that y 2
R to.A,] and Z 2 Rr,
1: (()) < TM_ T0M_reach(X,,.m
(1))))
2: y evaluate( (()), (lo, 41)
3: <- evaluate( (1),
4: return (),
E [-0.5, 0.5]]. Taylor models subsume common set representations. Thus we assume that the initial set X, is given as a Taylor model.
Algorithm 2 summarizes the implementation of post Here TM "M_reach(X,, u, J, [4),4] (line ! computes special Taylor model P(t) that depends on time t. To obtain y and Z, evaluate this Taylor model with different values for t: For ) we evaluate with the time interval [fo, 41], which results in an enclosure of R- For Z evaluate with the time point t,, which results in enclosure of R2,- Algorithm 2 can be adapted for discrete-time systems, where the procedure TM reach is replaced appropriately, line 2 skipped, and the result is (Z, Z).
Proposition 1. Algorithm implements procedure post, satisfying Eg. 5
Algorithm 3 instantiates posly. Recall that the goal of this procedure is to compute enclosures of nct,,,'' 7 which are the sets of states that result an action u. Given set X' and decision tree T, the idea is to propagate X' down the branches that the states E X would take. While the algorithm is
5

---

box(z.)
1.5
bux((,
0.9
0.6
0.3
(a) Enclosures of the reachable states Rjo,r y (bluc) and R, Z (purple) starting from Xo (yellow).
(b) Bisection wrt. (red) into Z1 (green) and 22 (brown), and interval enclosures (cyan, orange).
Figure Example execution Algorithm for the first control cycle.
agnostic of the predicates T (interpreted as sets of states) on a conceptual level, generally diffi- cult to implement the algorithm for arbitrary predicates. In our implementation, we exploit the struc- ture axis-aligned half space-pacee predicates P. Let box(Xt) be the interval enclosure of X. which is casy to obtain for Taylor model. In line we check if all states in X' take the left branch of T. We have X C P if and only box (x) C P. In line II we check if all states in X' take the right branch T. We have X n P = 0 if and only if box
P 0.
Algorithm 3 Post for the decision tree
both conditions fail, X is bisected into 21 = x X' P} and 2₂ {o x E X' n PC} in line 14 Here pC denotes the complement
Input: set X', decision tree T
P. which is also a half-space. Since the above sets hard to compute, replace X' by box(2() in the implementation. Note that box(X') P 2 box in P) in setting. We diseuss this further in Appendix A.l
Output: set of pairs (Xu, u)
S 0
2: Q + [(X', (T))
3: while -isempty(() do
4: (y),Ty) < pop(()
5: if isleaff Tyy) then
Proposition 2. Algorithm 3 implements procedure post.
6:
push(S, ()5))()))
satisfying Eq. (4). Furthermore, if all bisections are exact, Eq. (4p is satisfied with equality.
7: else
8:
P P i' C P then
Further details relevant for using our method in practice given in Appendix [
9:
10:
push(Q, (J), left(T))))
11:
else y = then push(Q, (3), right (Ty)))
Example 3. We walk through Algorithm [for the first control cycle, illustrated Figure 3 Figure shows how Algorithm 2 computes the pair ()), 2), consisting of enclosure R. of the reachable states up to time point T and an enclosure R, of the reachable states at the last time point. Figure Tigure{3(b) shows how Algorithm bisects the set Z along the predicate I into sets Zı and Zz. We furthermore illustrate the approximation with interval enclosures. Assuming this the only predicate of the decision tree, Algorithm wooll continue the analysis from these two sets in the next iteration.
12:
13:
else
14:
(Z,, 22) bisect()), P) push(Q. (21, left(Ty)) ))
15:
16:
push(Q, Q (Zz, right(Ty)))
17: end if
18: end if
19:
end while
return
3.2 Generalization to Unbounded Time via Fixpoints
Next we discuss how employ set-based fixpoint check; for details refer to the literature Giacobbe) 2019). Roughly speaking. if we do not encounter new states after an iteration, we have found a fixpoint. Algorithm ittertively adds states to R to enclose the sequence (k+))()++1)7) kmax (Section 2.2). Let us View the exploration of the elements (X,4) in the queue Q as a search tree. First, the search the other nodes (i.e., if a fixpoint has been found). Second, if this condition holds in all branches, have computed the reachable states in unbounded time. However, due to the discrete nature of
node can be terminated if the set X' is contained in the union of the sets in

---

the policy, the time points at which to check for fixpoints are relevant. A sufficient condition is to only compare the sets at the beginning of each control cycle, i.e. Rar SUiek Rjr for some k >> 0. However, when dealing with enclosures, this condition would become Rar S UJcc Rjr, which is not sufficient. The set Ray on the left-hand side must additionally contain the reachable states from all sets R-- on the right-hand side. Fortunately, our algorithm satisfies this additional condition.
In our implementation, all sets are (unions of) Taylor models, for which inclusion checking is hard. While can overapproximate the left-hand side, we would have to underapproximate the right-hand side, which is difficult for Taylor models. However, whenever we bisect sets in posty: we obtain box-shaped sets, for which inclusion checks are easy. Thus, in our implementation, we only perform a fixpoint check after a bisection. We shall see in the evaluation that this is often sufficient in practice.
3.3 State-Independent Dynamics and Computational Complexity
We call control system state-independent if f(x,, u) = u for all x (for which must be n- dimensional). This is arguably the simplest possible control system. If the system dynamics are blate-independent and &g is a polyhedron (i.e., the intersection of linear inequalities), post, can be implemented exactly and yields polyhedron [Alur et al. 1996]. Given polyhedron, posty returns a union of polyhedra. Under these assumptions, Algorithm I can be implemented to compute the exact reachable states and thus satisfy Theorem [ with equality. Finally, Algorithm [] can be turned into a decision procedure for the reach-avoid problem (namely: also output RT.... and check Eq. ①). Nevertheless, state-independent DTCS can encode Turing machines. Hence the reach-avoid problem undecidable unbounded time and PSPACE-comples
bounded time (proven in Appendix C.2).
The reach-avoit problem for both continuous time and discrete-time DTCS over rational numbers with stteeindeeenneett dynamics and polyhedral initial, goal, and error sets (No, G,E) is PSPACE-complete, and undecidable when considering the unbounded-time version.
Theorem 2.
Note that Algorithm T solves not only the decision problem but computes the full reachable states. Thus it needs to collect all the sets resulting from bisections. If the number of iterations kmax is given in binary, the algorithm is doubly exponential, even if we ignore a potential complexity growth in the set representation. We conjecture that this bound is optimal for the full computation. More precisely, in each iteration, may be bisected into several (but at most E, where E is the number of leaves of the decision tree) sets, With kmax control cycles, the algorithm may end up with tlmss sets in the end.
4 Evaluation
We implemented our method in a tool based
on JuliaReach [Bogomolov et al. 2019] for the Taylor-model algorithm (TM reachin Al-
Table 1: Sizes of the decision-tree policies, and cor-
responding verification times averaged over 10 runs.
gorithm 2 [Benet et al. 2019] and LazySets [Forets and Schilling [021] for the set compu- tations. We demonstrate our approach on the quadrotor system (Figure T(a) and three clas- sical control problems from the Gymnasium [Brockman al., 2016): cart/pole, acrobot, and mountain/car. In the following, we use our proof-of-come of-concept implementation to ver- ify and visually explain that, within the given time constraints, the quadrotor safely reaches the end of the corridor, the cart manages to stabilize the pole, the acrobot swings to the goal height, and the car reaches the top of the mountain. It is crucial to maintain high precision during the analysis to avoid divergence. The systems illustrate different aspects: Our approach applies to time-dependent policies (quadroior control), proves infinite-time stability (Section 3.2) (cart/pole), handles transformations (Appendix A.2) (acrobot), and deals with discrete-time dynamics (mountain/car), while preserving high precision.
System
Policy T
Verification
nodes depth actions
time
Quadrotor
177
10
8
84 sec
Cart/Pole
5
15 sec
Acrobot
7
101 sec
9
2 113 sec
Mountain/Car
7 sec
'The implementation and experiments are available at hattps://ithhnn cottub..co///eriAA Safety- Verification of Decision Tree Policies in Continuous Timme
7

---

0.3
0.9
Pv
initial
-06
goal
reference
boundary
Pr
Figure 4: Reachable states (red) and simulations (colored) for the quadrotor system. The initial states are shown in yellow on the left, the goal region shown in blue at the top, the reference plan is shown in brown, and the dashed blue lines mark the safety corridor.
We obtain decision-tree policies via neural-network distillation (see Table on the depth and number of nodes and actions). For the quadrotor system collected 500 samples of state-action pairs from a neural-network policy used by [vanov et al. (2019) and learned a decision tree of depth 10 using behavioral cloning. For the three other systems (cart/pole, acrobot, mountain/car)
first used deep Q-learning to train a two-layer convolutional neural network (Mnih et al. 2013) and then adopted the Viper algorithm [Bastani al. 2018 imitation-learn decision trees for these systems. We manually prune the resulting trees of redundant nodes (as Viper produces balanced trees).
All experiments were conducted on laptop with an i7 1.80 GHz CPU and 32 GB RAM.
4.1 Evaluation on Decision Tree for Quadrotor Control
We evaluate our verification approach on decision tree controlling six-dimensional quadrotor, tasked follow a piecewise- lineer plan (see, Example The actions represent possible combinations of pitch, roll, and thrust acceleration. This is complex continuous-time system (see Appendix [.]] for full details). The policies for such high-dimensional systems are typically approximated by learned model, e.g., neural network [Royo et al. 2019]. We train decision-tree policy of depth 10 imitating the neural network from [vanov et al. 2019
Figure showws the set of reachable states, Ivanov et al. (2019) verified the neural-network policy, for which they had to split the initial set into 16 subsets tame the approximation error. Computing the reachable states took between 10 and 59 minutes for each subset. Our method can be applied to the full initial set directly and verifies the system 6.5 minutes.
4.2 Evaluation Decision Trees for Classic Nonlinear Control Problems
Next we study three classical control systems, for which we trained small, interpretable decision trees (see Table T). Small decision trees are often sufficient for optimality (os and Verwer 2023
A description is given in Appendix B.2 The goal is for the pole to remain vertically stable within an angle of +0.06". This system is challenging because of quick alternations in the control action. In Figure reachable states in the 0/w projection together with the decision boundaries (c.g., the policy moves the cart the left in the green region). The analysis terminates in 40 seconds and proves that the blue dashed line 0 = 0.06 is not exceeded. Furthermore, the fixpoint check allows to generalize the results to infimite time; thus can conclude that the policy is able balance the pole forever.
Cart-Pole System. We consider the cart-pole system Barto al. 1983
show the

---

ctt rihht
05 goal
Svoid
00
05
-1.5
101
-05
-10
time
(a) Cart-pole system. The imitial states are shown as yellow borders. The angle safety threshold is shown dashed blue. The background (green, cyan) shows the decision boundaries.
(b) Mountain-car system. The goal height is shown as dashed blue.
Figure 5: Reachable states (red) and simulations (black) for the cart-pole and mountain-car systems.
goal
goal
Inttal
-50
800 25
-50
000
25
Figure 6: Reachable states (red) and simulations (black) of the acrobot system. The goal regions are shown in blue and the initial states around the origin are shown in yellow (magnified to make them visible). The left (right) plot shows the results for the depth-2 (depth-3) decision-tree policy.
Acrobot. We consider the acrobot system [Sutton] 1995). which consists of two links connected by joint, one of which can swing freely. A full description is given in Appendix B.3 The goal is that the free end reaches a desired height, expressed as the condition - (0s( cos( 02 + 01) > where 0 is the joint angle and 02 is relative the angle of the first link. This system has complex nonlinear dynamics that require high precision. We obtain two decision-tree policies and compare their performance. The system applies nonlinear transformation to the state before passing it to the policy. We discuss handling transformations Appendix AA. Figure Toreeoollluss iillustrates that all trajectories reach the goal regions. The analysis takes 100 (first policy) resp. 112 seconds (second policy).
Mountain- System. To demonstrate applicability to discrete-time systems, we consider the mountain-car system, where has to reach from one mountain another [Moore [990]. A description is given in Appendix B.4, Figure ((b) shows that the car always reaches the top of the mountain within most 132 steps. The analysis terminates in 16 seconds.
4.3 Comparison with State-of-the-Art Reachability Tool for Hybrid Automata
As explained before, a DTCS can be seen special case of hybrid automaton. We encoded the various DTCS from the evaluation hybrid automata (a description of the encoding given in Appendix D) and then applied the waaee-o-thhe-e reachability tool JuliaReach [Bogomolov et al. 2019) to them. The result was that tool got stuck as soon had to bisect the set of states for first time, and we had to terminate the tool after several minutes of no progress. For instance, when we evaluated the reachability tool on the cart-pole system, the tool can analyze the first four control periods (out of 25) in 22 seconds, but then gets stuck in the fifth control period when the bisection

---

starts, and prints enrors about numerical instability. This demonstrates that our algorithm is the first feasible solution to the reach-avoid problem for DTCS.
Our algorithm exploits the decision-tree structure to only explore the feasible automaton transitions (most of the time this is just one). Furthermore, given the periodic control policy, we only have to check the transitions at specific time points (an observation we already made in earlier work (Forets) al. 2020]). Moreover, since we focus on axis-aligned predicates, interval enclosures are often sufficient. Finally, often only one branch of the decision tree is relevant, which allows us to ignore the complement branch and avoid unnecessary calculations. Even if several leaves of the decision tree are reached, these may still all be annotated with the same control action. In that case we do not have bisect the set (which avoids the main source of approximation error).
The other tool views the automaton as black-box model and thus cannot make use of this structure; instead it needs perform many intersection operations, which are expensive and typically force to use a more complex set representation. These structural insights make our analysis not only more efficient but also more precise in practice because general hybrid-automata tools would typically approximate these operations.
5 Conclusion
In this paper, we studied the reach-avoid problem for continuous-time and discrete-time dynamical systems controlled by a decision tree. The problem is undecidable for nonlinear systems, and we showed undecidability even for the simplest dynamics as well as PSPACE--ompllteness in the bounded-time setting. We proposed the first practical algorithm to solve this problem in continuous time. The abstract algorithm is sound and, for simple systems, complete. We implemented the algorithm for nonlinear systems and decision trees with axis-aligned predicates. Our evaluation shows that the algorithm is precise and performant on typical problems. Our approach enriches the verification toolset for machine-learnin challenges. Our approach lends itself to visualization and can serve for further analysis and refinement of decision trees, which themselves are interpretable surrogates for black-box policies.
based systems and opens novel cross community research
Coming to the limitations of our approach, we have only considered inne-invariant systems. While the algorithms are general, the fixpoint check we used does not apply to time-varying systems. In our experiments, with the exception of the quadrotor, we focused on small decision trees. We note that the size of the decision tree is not necessarily a good measure for complexity. Multiple leaves may share the same action, and some leaves may not be used at all during the execution. The main impact the verification method, in experience, is the number of times the decision boundaries are partially crossed by the reachable states (after a time step). Furthermore, the control systems we verified in the evaluation, while nontrivial from verification perspective, have relatively simple control tasks where a decision tree is not required. We plan to investigate how our method performs on systems with more challenging control tasks, e.g., the cart/pole system starting with the pole hanging downward (which we were not able to verify in a preliminary attempt).
In future work we will also study how the analysis can be improved both in terms of precision and scalability. For precision, we plan to employ set representations that are closed under bisection, e.g., constrained polynomial zonotopes (Kochdumper and Althoff, 2023). which generalize Taylor models. For scalability, we aim to improve the fixpoint check using simulation-be based heuristics. Another natural direction is to apply the approach to learning safe decision-tree policy, for which methods to compute underapproximations in order to refute unsafe models would be useful. Finally, our recent algorithm synthesize safety shield for policies of systems with complex hybrid dynamics Brorhhlt et al. 2023] only detects discrete-time safety violations; hence we aim to find synergies with the method presented in this paper.
Acknowledgements. We are grateful for the anonymous reviewers' helpful comments to improve the paper and suggesting the swing-up cart/pole experiment future challenge. Anna Lukina thanks Mustafa Mert Çelikok and Alexandru Bäbeanu for their timely feedback. This research was partly supported by DIREC- Digital Research Centre Denmark under reference number 9142-0001B and the Villum Investigator Grant S4OS under reference number 37819.
10

---

References
M. Akintunde, Botoeva, P. Kouvaros, and A. Lomuscio. Formal verification of neural agents in non-deterministic environments, Anton, Agents Multi Agent Syst., 36(1):6, 2022. URL https: //doi. odbi..org/1..1000 1007 /s 000-568-021-9955500 021-09529-3
A. Alamdari, G. Avni, T. A. Henzinger, and A. Lukina. Formal methods with a touch of magic. 10. 347277 /2020/22222/ /isbn In FMCAD, pages 138-147. IEFE, 2020. URL https://doi...... wtwp:i...o./100000/
978-3-888 111-3-85448--42---
M. Althoff, Frehse, and A. Girard. Set propagation techniques for reachability analysis. Annual Review of Control, Robotics, and Autonomous Systems, 4(1):369-395, 2021. URL httL:ttps::. //doi
org/ 10. 1146/
R. Alur, T. Henzinger, and Ho. Automatic symbolic verification of embedded systems. IEEE Trans. Software Eng., 22(3):181-200 1996.
http////oooo/////////////// 10.110./....1111111 489079
P. Ashok, J. Kretínsky, K. G. Larsen, A. L. Coënt, J. H. Taankvist, and M. Weininger. SOS: safe, opti- mal and small strategies for hybrid Markov decision processes. QEST, volume 1 17785 of LNCS, pages 147-164. Springer, 2019. URL
P. Ashok, M. Jackermeier, P. Jagtap, J. Kretínský, M. Weininger, and M. Zamani. dtControl: decision tree learning algorithms for controller representation. In HSCC, pages 17:1-17:7, ACM, 2020. UtLhttss::/ddd /wi. org/ 10. 145/3365365.... 3382220
E. Bacci, M. Giacobbe, and D. Parker. Verifying reinforcement learning up to infinity. In IJCAI, pages 2154-2160. ijcai.org. 2021. URL JRLLhtpps://oo..rr///1 wttp:////....2220///............
A. G. Barto, R. S. Sutton, and C. W. Anderson. Neuronlike adaptive elements that can solve difficult learning control problems. IEEE Trans. Syst. Man Cybern., 135))834-846, 1983. URL
httpa://doi.org:
1ww11/199MTCC.. 1983. 63130777
O. Bastani, Y. Pu, and A. Solar-Lezama. Verifiable reinnorrceemntet learning via policy extraction. In neur haaa://6556aa2222ccc00006677---3 Abstract. html
NewrlPS, pages 2499-2509, 2018. URL.Btttss:/pproceediigg neur http://.....reppppppp/p/////////
L. Benet, M. Forets, D. Sanders, and C. Schilling. TaylorModels.i:: Taylor models in Julia and its application to validated solutions of ODEs. In SWIM, 2019. URL httttttt////wwiii
-asta-paristeer ft/ prrrppppr////// httpppppa/bbeetttt bearrr/bbbeet.ppp. .dff
M. Berz and K. Makino. Verified integration of odes and flows using differential algebraic methods on high-order Taylor models. Reliab. Comput., 4(4):361-369, 1998. httpss//:///oo org/ 10. 1021003/AAs A: 1024467732637
S. Bogomolov, M. Forets, G. Frehse, K. Potomkin, and C. Schilling. JuliaReach: toolbox for set-based reachability, In HSCC, pages 39-44. ACM, 2019. https:::://// 1145/
1145/
3302504 33118844
L. Breiman, J. H. Friedman, R. A. Olshen, and C. J. Stone. Classification and Regression Trees. Wadsworth, 1984. ISBN 0-534-98053-8.
G. Brockman, V. Cheung, L. Pettersson, Schneider, J. Schulman, J. Tang, and W. Zaremba. OpenAI Gym. CoRR, 2016. URL htttps:/arxxv..rrg/ wttp://wwwww..aba///.....11 01540
A. H. Brorholt, P. G. Jensen, K. G. Larsen, F. Lorber, and C. Schilling. Shielded reinforcement learning for hybrid systems. In (A)ISoLA, 2023. URL htttp:://di..rgg//e 48550/a Xiv
2308. 14424
A. David, P. G. Jensen, K. G. Larsen, M. Mikucionis, and J. H. Taankvist. Uppaal Stratego. In TACAS, volume 9035 of LNCS, pages 206-211. Springer, 2015, URL http::://///ooorrr/////// 1007 197899---665 ----666-2--661--16
L. Doyen, G. Frehse, G. J. Pappas, and A. Platzer. Verification of hybrid systems. In Handbook of Model Checking, pages 1047-1110. Springer, 2018. URL. httpp::
1007
978- 3- 3-8-3-319- 10575-0171100

---

M. Du, N. Liu, and X. Hu. Techniques for interpretable machine learning. Commun. ACM, 63(1): 68-77. 2020. URL httLhhtts::/ooiie /ttpp:://aa...orr//01111///////3
Dutta, X. Chen, and S. Sankaranarayanan. Reachability analysis for neural feedback systems using regressive polynomial rule inference. In HSCC, pages 157-168. ACM, 2019. URL https:
//doi.org/10.. 210.:0111144/30000.33111111
A. B. Eriksen, C. Huang, Kildebogaard, H. Lahrmann, K. G. Larsen, M. Muniz, and H. Taankvist. Uppaal Stratego for intelligent traffic lights. In ITS European Congress, 2017.
Fan, C. Huang, X. Chen, W. Li, and Q Zhu. ReachNN A tool for reachability analysis of neural-network controlled systems. In A7VA, volume 12302 of LNCS, pages 537-542. Springer, 2020. httLltttp::///..rrrg////// http://///....0000///-/-------00 000.0009990000000----0---------0
M. Forets and C. Schilling. LazySets.jl: Scalable symholic-numeric set computations, Proceddin Proceedings of the JuliaCon Conferences, 1(1):1 2021. URL//ttps:///0boorr///10 http:////o..11//ccooooooooo 70009 00097
M. Forets, D. Freire, and C. Schilling. Efficient reachability analysis of parametric linear hybrid systems with time- triggered transitions. In MEMOCODE, pages 137-142. IEEE, 2020. URL
httpa://doi org/ 10. 1091 /Mt////DEEEE113333 200000001111100000....2222 9314994
M. Fränzle and C. Herde. Hysat: An efficient proof engine for bounded model checking of hybrid systems. Formal Methods Syst. Des., 30(3):179-198, 2007. htLp:ttss:/ /ttb:ttt////ooi.o////00..
810703-006 0000--0000000---00
M. Fränzle, C. Herde, T. Teige, S. Ratschan, and T. Schubert. Efficient solving of large non-linear arithmetic constraint systems with complex boolean structure. J. Satisf. Boolean Model. Comput., (33-4):209-236, 2007. URLpttps: /ttttp::/doi.orre 10. 3233/ sat190012
M. Giacobbe. Automatic time-unbounded reachability analysis of hybrid systems. PhD thesis, IST Austria, 2019.
E. Hainry. Reachability in linear dynamical systems. In CiE, volume 5028 of LNCS, pages 241-250. Springer, 2008. URL
T. A. Henzinger. The theory of automaataaaaaaaaaa automata. In LICS, pages 278-292. IEEE Computer Society, 1996. URL htt.lhttps://// /ttttp::/doi. 1109/IIc.. 1996. 561342
H. Hyötyniemi. Turing machines are recurrent neural networks. Proceedings of step, 96, 1996.
R. Ivanov, J. Weimer, R. Alur, G. Pappas, and I. Lee. Verisig: verifying safety properties of hybrid systems with neural network controllers. In HSCC, pages 169-178. ACM, 2019. URL https: http:::/ddoi.ooo 10. 1145/3302504. 331 1806
R. Ivanov, T. J. Carpenter. J. Weimer, R. Alur, G. J. Pappas, and I. Lee. Verisig 2.0: Verification of neural network controllers using Taylor model preconditioning, In CAV, volume 12759 of LNCS, pages 249-263 Springer, 2021. URL http::/:://aao..o///000/000/00 00010//999770--00-8------------0 011---88-00-------------- 8_11
N. Kochdumper and M. Althoff. Constrained polynomall zonotopes. Acta Informatica, 2023. URL https://doi.org//1 10. 1077//000026-000--00333333
N. Kochdumper, C. Schilling, M. Althoff, and S. Bak. Open- and closed-loop neural network verification using polynomial zonotopes. In NFM. volume 13903 of LNCS, pages 16-36. Springer, 2023. wtR.stttsss// //to::///do...o http:///ooo.../////.// 1007 3-077-----01-3310--233
K. G. Larsen, M. Mikucionis, M. Muñiz, J. Srba, and J. H. Taankvist. Online and compositional learning of controllers with application to floor heating. In TACAS, volume 9636 of LNCS, pages 244-259. Springer, 2016. URL httpss//://o org/ 10. 1007 39700799773--111 662 49674-9_144
D. M. Lopez, M. Althoff, L. Benet, X. Chen, J. Fan, M. Forets, C. Huang, T. T. Johnson. T. Ladner, W. Li, C. Schilling, and Q Zhu. ARCH-COMP22 category report: Artificial intelligence and neural network control systems (AINNCS) for continuous and hybrid systems plants. In ARCH, volume 90 of EPIC Series Computing, pages 142-184. EasyChair, 2022. URL,https: //ttps:///oil //doi org/10. 29007 39007/wfgr
12

---

K. Makino and M. Berz. Taylor models and other validated functional inclusion methods. Int. J. Pure Appl. Math, 4(4):379 2003.
V. Mnih, K. Kavukeuoglu, D. Silver, A. Graves, Antonoglou, D. Wierstra, and M. A. Riedmiller. Playing Atari with deep reinforcement learning. CoRR, 2013. 1312.5602
ora.iiv..rggaaa /bs/
V. Mnih, K. Kavukcuoglu, D. Silver, A. A. Rusu, J. Veness, M. G. Bellemare, A. Graves, M. A. Ried- miller, A. Fidjeland, G. Ostrovski, S. Petersen, C. Beattie, A. Sadik, I. Antonoglou, H. King, D. Ku- maran, D. Wierstra, S. Legg, and D. Hassabis. Human-level control through deep reinforcement learning. Nat., 518(7540):29-533 2015. URL https: ptttps://do... org/10. /03///ature1/11////aaaaaa11 4236
A. W. Moore. Efficient Memory-based Learning for Robot Control. PhD thesis, University of Cambridge, 1990.
A. Neumaier. The wrapping effect, ellipsoid arithmetic, stability and confidence regions, pages 175-190. Springer, 1993. URI.httss:/ ortp://///oooooo//////o/// 10. 10011111000777---701-----00
J. R. Quinlan. Learning decision tree classifiers. ACM Comput. Surv., 28(1):71-72, 1996. URL https://doi.org/ .tte:/1011155555
234346
V. Royo, D. -riiovich-Keil, S. L. Herbert, and J. Tomlin. A classification approach for approximate reachability, In ICRA, pages 7697-7704. IEEE, 2019. URL URL/attpp://doo.orr//10 1109/ICRA. 2019.
W. Savitch. Relationships between nondeterministicc and deterministic tape complexities. Comput. Syst. Sci., 4(2):177-192, 1970. URL httpppp://..1..o//11111111////// (70)) 80006-X
C. Schilling, M. Forets, and S. Guadalupe. Verification of neural-network control systems by integrating Taylor models and zonotopes, AAAI, pages 8 8169-8177, AAAI Press, 2022. URL
https://ojs. aaai. org/ /i///iidddxx////e http////AA/aaaaaace/////////////
J. C. Shepherdson and H. E. Sturgis. Computability of recursive functions. J. ACM, 1022:211-2555 1963. httt://ttts:///aa org/ /ww.//////...../.....111/1 160. 321170
R. S. Sutton. Generalization in reinforcement learning: Successful examples using sparse coarse coding. In D. S. Touretzky, M. Mozer, and M. E. Hasselmo, editors, NeurlPS, pages 1038-1044. MIT Press, 1995. http: www.eeeddinnnnnnnnnsneeomee /eeprrppp.ccoppppe///9/////eeeee / Bf:d::000cb330066600000666 Abstract.html hht
H. Tran, X. Yang. D. M. Lopez, P. Musau. L. V. Nguyen, W. Xiang, S. Bak, and T. T. Johnson. NNV: the neural network verification tool for deep neural networks and learning-enabled cyber- physical systems. In CAV, volume 12224 of LNCS, pages 3-17. Springer, 2020. URL. fhttps //doi. org 10. 10000778----00 53288-822
C. Urban and A. Miné. A review of formal methods applied to machine learning. CoRR, 2021. URL atttp:://axiias org/ abs 2204 02466
D. Vos and S. Verwer. Optimal decision tree policies for Markov decision processes, In IJCAI, pages 5457-5465. ijeai.org. 2023. URL
2tt.//100.949//jjcaaa http:///iiaaaa223////33 2023/606
B. Xue, Easwaran, N. Cho, and M. Fränzle. Reach-avoid verification for nonlinear systems based on boundary analysis. IEEE Trans. Autom. Control., 62(7):3518 3523, 2017. URL httss 7/doi. ridoi.org/1..o 1109 TTCC 2016. 2615599
13

---

A Additional Information on our Method
This section contains some technical remarks on the precision of our method as well as on how to deal with state transformations. The latter is relevant for solving one of the benchmark problems in the evaluation (Section 4
A.1 Precision of the Algorithm
The precision of the Taylor-model implementation of post, (Algorithm 2 is good in practice most of the time. The main approximation error in Algorithm T comes from the bisections in post, (Algorithm (3) and the subsequent approximation, as exemplified in Figure (3b] This is hard to avoid with nonlinear dynamics, for which bisection of non-convex sets is challenging, With iterative algorithms like ours, the issue with approximation errors is that they accumulate over time, which is known the wrapping effect [Neumaier] 1993]. especially if there control actions (i.e., crossings of the decision boundary). To reduce the likelihood of a bisection and accumulation of errors, one can subdivide Xo into smaller subsets and run an analysis from each of them so that either all or none of the states cross the decision boundary at the same step (for instance, as mentioned in Section 4.1, this idea was used by Ivanov et al. [0019] for the quadrotor model). This can sometimes be achieved more efficiently by only considering the set boundaries [uue et al. 2017
frequent changes of the
A.2 State Transformations Before Evaluating the Decision Tree
So far we have assumed that the decision tree T takes the current state as input, as shown in Fig- ure However, some policies instead receive a transformation of the state. This is particularly useful for decision-tree policies with linear predicates (like ours) because a nonlinear transforma- tion effectively augments them with nonlinear predicates. For instance, the acrobot model (see Appendix B.3 for more information) has the state vector (01, 02 01, 02). but the input T is the vector (cos( 0, ), sin(01), (02) sin(02), 0,, 02). To account for transformations, we can modify Algorithm as follows. First we apply the transformation to the input set X' which is easy if X is given Taylor model. Then we apply Algorithm 3 and finally
have to "undo" the transforma- tion for the output. We distinguish three cases. In the first case, if the output is a single pair (Ku, u) (i.e.. there was no bisection). we replace it with (X, u). In all other cases, there was bisection. If the transformation is invertible, as in the above case, we apply the inverse transformation (here: (arccos(a1) ) arcsin(x2)) 25; Ra). where x is state of the output set Xx,) to each set Xx the output pairs (Ka, u). Otherwise, if the transformation is not invertible, we conservatively replace each pair (Xy,, u) with the pair (X' u).
B Additional Information on the Benchmark Systems
Below we provide further information on the systems from the evaluation (Section
B.1 Quadrotor System
A quadrotor is tasked to follow a piecewise-linear reference trajectory via bang- bang control (see Figure [(a)). The six-dimensional state space consists of two 3D vectors for position and velocity. The action space consists of 3D vector representing possible combinations of pitch (0), roll (d), and thrust acceleration (a). Using the gravity constant = 9.81, the continuous dynamics are:
P2 = Uz
by
Un
P U2
dz (0)
i = -g (a)
d a
The policy's 's task is to minimize the difference between the reference and the actual trajectory. The set of initial states is X, |-0.5 0.05]2 x {0)a 4 The control period is 0.2 time units and the number of control cycles is 30. The decision-tree policy T has depth 10 and is too large to depict here.
B.2 Cart-Pole System
pole is vertically attached on top of a cart that can moved left or right along a frictionless track. The goal is to move the cart such that the pole is kept in upright pose (i.c., the pole angle is small).
14

---

The state consists of the cart position p. cart velocity pole angle 6, and angular velocity w. The action space is U [-1.1} ("left", "right") with control variable u. The continuous dynamics are:
1 e 0 co)
9.8 ()) cos (8)
p p= u
22
2/3 + 5/11 cos
10u + 0.05w² sin(O)
Ô=w w
Φ
1.1
The set of initial states is the union of two hyperrectangles X6 1-0.05, 0.05]* and {0}² x [-0.025, 0.025] x [-0.2, 0.2]. (We added the second hyperrectangle to make the problem more challenging.) The control period is 0.02 time units. The decision-tre tree policy T is shown Figure ((a) and works as follows. If the pole is leaning to the left (0 < -0.014) or moving in the left direction (w I 0..201), the cart is moved the left (action 1 in the leaves), and otherwise the right.
The goal is to keep the pole angle 0 within a small range around O. Figure @egure&shooe shows simulations from the corners of Ng plus 100 random initial states inside Xg for 2 time units. From these simulations, we can see that seems to stay in the interval [-0.06, 0.06]. but some trajectories come close to the upper bound. In the evaluation (Figure ((a) we prove this property for Rjo,u.5]-
The fixpoint check allows to conclude that the policy able to balance the pole forever. The fixpoint is only found in the l/w projection, but this is sufficient because the cart's 's position and velocity are irrelevant for the decisions of the tree.
B.3 Acrobot System
The acrobot system consists of two links connected by a joint to form a chain. One end is fixed while the joint and the other end can swing freely. There are four state dimensions: angles 01 and 02 and their velocities á and dg. The action space = {0, 1, 2] ("left", "none", "right") with control variable u. The continuous dynamics of the velocities are:
d2bb + Ø1
8,
02 vb
di
where
di m iei + m2 mz( + 1o2 + 21, cos()))) + T + Tz
d2 = m2(1c2 + l lc2 cos() + Iz
Φ m2le2g cos 01 + 02
7 2
Φi -mal 10262 (in) 2m2li Icg020 sin(O2)
(m1le1 + m2h1)2 cos (0:
2 02
3 u + d2 01 mzh 1c sin()2) - Φ2
m2le + 1/
d3
z
The goal is that the free end reaches desired height, expressed as the condition cos(6;) ( (02 01) > 1, where 0 is the joint angle and 0g is relative to the angle of the first link.
The initial condition No is union of point and hyperrectangle Xo ({-0.0005) x {0} U [-0.0705, 0.0695] [-0. 0.00050, 0.0005)) {0)². The control period 0.2 time units and the time
S 0
0 < -0.014
< 0..04
S
0.37
< 00.01
x 0.391
2
2
(a) decision tree for the cart-pole system.
(b) decision tree the mountain car system.
Figure 7: Decision trees for the cart-pole and the mountain-car systems.
15

---

0.06
0.00
-0.06
0,0
0.5
10
1.5
2.0
time
Figure 8: Simulations for the cart-pole system.
01 < -0.99
0 S 00.97
02
-1335
02 S 1.123
0 < - 1.113
02 S 1.582
01 < 2.661
2
Figure 9: Two alternative decision trees for the acrobot system.
horizon is 100 time units. For this system obtained two different decision-tres policies of depth resp. 3, shown in Figure 9
The system applies a transformation to the state before being passed to the decision-tree policy. Concretely, the state vector (01, 02 02) is mapped to the six-dimensional vector (cos(01), sin(()). cos() sin()),, 02). (This transformation is technically irrelevant for the two policies obtained, because they only consider Ó and 0z. which can be read from the transformed vector; but we do not exploit that.) We explain how to modify our algorithm in order to cope with transformations in Appendix A.2
B.4 Mountain-car system
The mountain-cal car system consists of a sinusoidal valley between two mountains and a car in between. the top of the higher mountain the right. The engine is not strong
The goal is to bring the enough to drive up the mountain by itself, so the car must drive up the left mountain and gain momentum reach the top of the right mountain.
The control actions are U = {0, 1, ("left", "none", "right") with control variable u. The system state consists of the car's position and velocity With constants F = 0.001 and g 0.0025, the discrete-time dynamics are:
Uk+ Uk (u 1)F cos(33x)g
Tk+1 = Ii + Uk+1
The set of initial states is X [- 0.505, -..445 (0). The decision-tree policy T is given in Fig. 7 The maximum number of discrete steps is 200, but as shown Fig. 5(b) trajectories reach the goal region within most 132 steps.
16

---

C Proofs of the Theorems
C.1 Proof of Theorem
Proof. We show (i) termination and (ii) soundness and relative completeness of Algorithm |
(i) The inner loop line terminates by assumption. The outer loop in line removes one element at time point to from Q and adds only elements at time point t min(to + T, m > to to Q (line 8). Elements after time point T max are not processed (line 6
(ii) We only show the equality case; the inclusion case follows because, in each step, all sets are overapproximated. The algorithm starts with X, Ro. In the first iteration, by assumption, post, only returns states To E An together with the corresponding action act( T) Similarly, post, only returns states reachable within [o, r]. By the end of the first while-loop iteration, we thus obtain R = rr), and the queue Q contains pairs (K,, -) such that the union of the sets Xy is the set Ry,
Further loop iterations work similarly. While the iteration order of Q (line 4) is not prescribed, all policies lead to the same result. Let us choose the implementation of Q as a LIFO (last-in, first-out) queue. This corresponds to breadth-first search where on level i + of the search tree have elements (Z,, f the union of these sets X; is again Rky. The claim follows by induction.
C.2 Proof of Theorem
We first prove PSPACE-completeneee in bounded time. For the membership, sketch nonde- terministic algorithm with polynomial space requirements for the complement of the reach-avois problem, which is sufficient by Savitch's 's theorem (Savitch] 1970) and because PSPACE is closed under complementation. The algorithm guesses an initial state and simulates the DTCS. In continuous time, the trajectory in one control cycle is line segment. In each step, the algorithm checks whether (i) the current line segment intersects with the error states and does not intersect with the goal set G. (ii) the final state in the last iteration kmax is outside the goal set G: these checks can again be performed efficiently. The number of iterations may be exponential, but we can maintain a counter with logarithmically many bits.
For the hardness, we show a polynomial time reduction from the word problem for deterministic linear bounded automata (LBA). Here we consider the LBA model with accepting state, total transition function, and the input tape containing the input word plus two bound markers for simplicity.
For better intuition, we provide an example after the proof, which we recommend reading in parallel.
Given is an input word w {0, 1]" and LBA A A, 8, qu, quce #1, #,) with states Q } 2 {0, 1, #1, # transition function 5 C Q x A -
{go, .1,....................... }. tape alphabet A = {0o, ..,...,
Q x A (L, R} (where L. and R denote moving the left resp. right), initial state To, accepting state Zasz, and bound markers #1, #r.
We define two bijections N₂ Q + (O..... 1} and No : (O...., |A| 1} to associate natural number with each state and tape symbol such that Jace is associated with |Q| 1.
We construct a DTCS with n + 4 state variables 2u...., Jq. Tp. + 4 control actions Vo,,.. .., Un++1 , Myy Up. control domain U = g (and control period T = 1 for continuous sys- tems). The environment dynamics J are state-independent, i.e., fxx u) u.
The decision tree is more complex, and we first establish some intuition. The state variables encode the LBA configuration, where the first (i.c., the value of z; encodes the tape symbol at position i), 2y encodes the current LBA state, and xp encodes the current position one transition. For that we construct the tree from four gadgets: a gadget to select the current LBA state, gadget to select the current position the tape, gadget to select the current tape symbol, and a gadget to apply the transition function to the current configuration.
2 dimensions
encode the tape contents
the tape. The execution of one control cycle corresponds to taking
The first gadget (LBA state selection) is degenerated tree only expanding to the right with [Q] - decision nodes. On the k-th level the predicate xig I k 1. The left leaf node at level + 1 the sub-tree Tk-1 corresponding the second gadget. On the last layer, the right leaf node is T
17

---

24
S
Zq
50
Tp
0
Tk,e,0
To
I
1
7k.0
PP S
T
Tg
S
2
T1
T2
T
Tk.2
Tk,e,
TKge,
(a) Gadget Outer spine with three states.
(b) Gadget 2: Sub-tree Tx with three tape positions.
Gadget Sub-tree Th. with four tape symbols.
Figure 10: Decision-tree structure from Example
The second gadget (position selection) is analogous tree Tk over Ep with decision nodes. On the ê-th level the predicate is p. S 1. The left leaf node at level + 1 is the sub-tree Te,e-1 corresponding to the third gadget. On the last layer, the right leaf node is Th,
The third gadget (symbol selection) is an analogous tree Th. over xy with |A|
decision nodes, 1. The left leaf node at level m + 1 is the sub-tree T
the 1n-th level the predicate is S corresponding to the fourth gadget. On the last layer, the right Ieaf node is Ts.,,1A1-1-
The fourth gadget (application of the transition function) is single leave node Tk. The indices encode that the LBA is currently in state (k) at position é and reads tape symbol No (m). Let us assume that the transition function prescribes to switch to state g', write tape symbol a', and move the right. Correspondingly, the state of the system is Fgg Ng(g) (((()))))))))))) & 1, It Na(a") and all other state variables remain unchanged. This is achieved by choosing
want to choose the control actions such that in the next step
Ug Ng(d')
up
Ug = = No(a') m, u, (for all E).
(For moving the left, choose up 11 instead.) Observe that the state variables keep track of the LBA configuration and that we have corresponding leaves in T for each transition in d. For fixed transition (g, a, q' a', dd) we actually have multiple leaves; they only differ in the choice of the control action (corresponding to the current cell index on the tape).
Finally, let w, be the i-th symbol of (starting with 1). The initial state is Bg Ng Tp
(first symbol of w), To = (1)))). Tn+1 = No and F; = Na (w:) for other i. The set of (ncc) (Mnce
goal states G consists of all states where I, = N2
Q 1. The set of error states & is 2) (encoded in binary).
not needed. The step bound is kmax [Q||A] --
The above construction is polynomial the size of the LBA and the word (the decision has O([Q) + ||| n) nodes), and the following equivalence shows that it is a reduction.
w is accepted by A
the configuration (go. #(w#+) leads to configuration with state Gace
the DTCS reaches state with ø = Ny within Amax steps
the DTCS satisfies the reach-avoid specification
The critical step (+), for which we rely on the intuition established above. Note that in the continuous-time case we have to make sure that a goal state is not reached accidentally between two control cycles. This is ensured by letting (gcc [Q]
This concludes the proof of CUPACE-completeneee unbounded time, we give an example to better illustrate the previous reduction.
Before we continue with the undecidability in
Example 4. Consider the LBA with states qo, Ass quees tape symbols 0, 1, #ts #r. and the only explicit transition 5(go. = (gace: O, R) (all other transitions lead to the sink state with appropriate
direction L/ L/R). R). The LBA accepts words starting with a (and changes to 0), We use the mappings
0 0
0 q 90
Ng(2)
1 q qs
Na(a)=
a
a #1
2 q = quee
3 a #
18

---

Now consider the input word w 1, which means we have the initial configuration (gu, #1 We construct a independeed DTCS with state variables (Zg, F I2, Fq Fp) and control actions (ug, U1 U2, Uq. Up). The initial state is (2,
#
position
The decision tree T is quite large (36 leaves), and we only depict its structure Fig. [0] first cartoon shows the outer structure. Each leaf node follows the structure in the second cartoon, and each leaf node shown there follows the structure in the third cartoon. Finally, we give one example leaf To.1,1 of the whole free, which stands for state qo lape position 1, and reading symbol 1. vector Observe that this is the leaf the decision tree chooses in the initial state. The control in that leaf is
The
0 0.0-1 1
Thus, in the next time step, the new state will be
coll O cell 1. cell sime
position
(2,033 #+
2
2
)r,
which a goal state. This concludes the example.
Rose position
Now we prove undecidability in unbounded time. For that, we reduce from the termination problem for deterministic two-counter machines (2CMs). We consider the model from [Shepherdson and Sturgis 1963 Theorem 4.1] with two counters C1 C2 E N and instruction set INC( (..) (increment counter C₂). DEC(c,) (decrement counter c₂ with zero lower bound), JZ(c,, E) for E {1, 2} (jump to location é if counter c₂ is zero), and STOP (terminate). Each instruction I comes with a position k in the program, which we write "k I". The initial value of the counters is C1 C2 0 and the program starts at instruction 1.
Given is 2CM with n instructions. We construct DTCS with 3 state variables zo, 3 pes 3 control actions U1, U2, Upe. control domain U = 2 (and control period 7 = for continuous systems). The environment dynamics are sate-indeeennent, i.e., f(x, u)
We first establish some intuition. The state variables I1 and i2 correspond to the counters e₁ and C2 and the state variable pe corresponds to the program counter. After each control cycle, these variables will have the corresponding values in the simulated 2CM. For the decision-tree policy, we construct gadget for each instruction in the 2CM, and one more gadget select the current instruction based on the value of Tpc-
We start with the latter gadget (instruction selection), which works precisely most gadgets in the previous proof. is a degenerated tree only expanding to the right with n 1 decision nodes. On the k-th level, the predicate is pe I k. The left leaf node at level + 1 is the sub-tree Ta corresponding to one of the other gadgets, depending on the k-th instruction. The last layer's 's right leaf node is T...
The other gadgets are trees substituted for Ta depending on the k-th instruction. We only describe the instructions for the counter c;; for e2 the construction is completely analogous by swapping 1 and in the indices. For instruction "k: INC(c1) )" we set Te to the leaf node with #1 = 1, U2 O, Upe 1. For instruction "k: DEC((1) (" we set Ta to the tree with decision node #1 S and two leaves; the left leaf node is M1 = 0, U2 0, Upc 1, and the right leaf node is
- -1, U2 0, Upe 1. For
instruction "k: : JZ(c1, E)" we set Ts to the tree with decision node I1 S and two leaves; the left
leaf node is 41 = 0, u2 0, Upe = l (- k, and the right leaf node is #1 0, u2 = 0, Upe 1. For instruction "k STDP" we set T to the leaf node with μ = 0, U22 = 0, Up kk.
Finally we define the (singleton) set of initial states X, (0, 0, 1)}. the goal region g = {(x y, 0) x, y R}. and the set of eиror states E = 0 (not used).
It is easy to see that each of the gadgets implements the 2CM instructions. Executing the action corresponding the STOP instruction the only way that Tepe can reach the value 0. Thus the above construction is a reduction.
the 2CM terminates
the STOP instruction is reached from the configuration 6j C2 0, pC
the DTCS reaches a state with Tepc
the DTCS satisfies the reach-avoid specification
19

---

D Modeling Decision-Tree Controlled Systems as Hybrid Automata
Here we expand on the discussion from Section 4.3 and explain the encoding.
Systems with mixed continuous and discrete dynamics can be modeled as a hybrid automaton [Henzinger [996]. As such, DTCS also be encoded as a hybrid automaton. The reach-avoid problem has been studied extensively for various subclasses of hybrid automata (Doyen et al.) 2018 Althoff al. 202T]. One could thus argue that solutions the reach-avoid problem for DTCS exist. However, when modeling DTCS as a hybrid automaton, the problem structure gets lost, and thus tools analyzing this hybrid automaton will not scale. Hence argue that our algorithm is the first feasible solution to the reach-avoid problem for DTCS.
Below present one possible encoding of a DTCS as a hybrid automaton, for which we assume that the reader is familiar with the terminology of hybrid automata. We encoded the systems from evaluation (Section 4) accordingly and applied the state-of-the-arr reachability tool JuliaReach [Bogomolov et al. 2019 (which also implements an algorithm based on Taylor models (Benet et al., as it had biseet the set of states for
2019]) to them. The result was that the tool got stuck the first time, and we had to terminate the tool after several minutes of no progress.
We encode a DTCS (T) t for time. We use one location by for each control action u E 2/ that occurs in T. The continuous dynamics in l, are given by f(x, v) At 1, where we substitute the value for the second argument v. Each location e, has an invariant t S т, restricting time to one control period. For each location and big
hybrid automaton as follows. First we introduce a fresh variable
there is transition to every location l,' with a guard condition consisting of t disjunction of conjunctions of the predicates along the paths in T to leaves with action u'. For instance, for T given in Figure 7(a). the guards on the transitions leading f-1 are V (e > 00.014 A I 0.2201)). Finally, each transition has a reset t := 0.
A (0 s
Such an automaton is challenging for black-box analysis tools because they always have to explore all transitions. For instance, when we evaluated the reachability tool on the cart-pole system, the tool can analyze the first four control periods (out of 25) in 22 seconds, but then gets stuck in the fifth control period when the bisection starts, and prints errors about numerical instability. By knowing the problem structure, just one), for which it only has to evaluate d predicates, where is the depth of the tree. Furthermore, given the periodic control policy, we only have perform these checks at specific time points. For general hybrid automata, this has to be found out via intersections with invariants and guards. These structural insights make analysis not only more efficient but also more precise in practice because general hybrid-automata tools would typically approximate these operations.
approach only explores the feasible paths of the decision tree (often there is
20


Reviews:
[{"review_id": "ytiOYaO7MC", "reviewer": "Reviewer_jTr9", "summary": "This paper presents a method to solve the reach-avoid problem for dynamical systems controlled by a decision tree in continuous time. The authors assert that this is the first paper to solve the problem in the continuous time setting. In the paper, the authors first provide a good overview of decision trees, the use of decision trees as neural network surrogates, and verification of decision tree controlled systems (DTCS). They also explain why tools developed for verification of neural network controlled systems are not directly applicable to DTCS. The authors then explain their approach, which is based on a typical reachability algorithm and determines the set of reachable states for an iteration of the control loop.\n", "questions": "Please see the comments above on weakness.", "limitations": "The paper could use more discussion on its limitations, particularly regarding scalability. The work does not have obvious negative societal impact.", "rating": 6, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "1. The problem of DTCS verification is interesting and well motivated.\n2. The paper is clearly and concisely written, and the justification of the paper as described is sound. The authors describe in great detail how their algorithms satisfy the equations necessary for the reach-avoid problem in DTCS. The authors also provide evaluations of their approach using multiple benchmark problems.", "weaknesses": "1. The novelty of the approach is not adequately explained. I believe that it is novel, but the authors need to explicitly state which parts of the algorithm are specifically designed for use with DTCS and which are just adapted from the typical reachability algorithm. \n2. Section 3.2, which describes the generalization of the solution to unbounded time problems, could perhaps use more details.\n3. The authors should also include some statement on how common axis-aligned predicates may be found in real-world DTCS. Is this a reasonable assumption?\n", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you for the excellent review.\n\n> The novelty of the approach is not adequately explained. I believe that it is novel, but the authors need to explicitly state which parts of the algorithm are specifically designed for use with DTCS and which are just adapted from the typical reachability algorithm.\n\nAlgorithm 3 as well as Theorem 2 are completely new. We will restructure the paper to clarify this point. Compared to analyzing a DTCS with a generic hybrid-system tool, the most important aspects of the special structure our algorithm allows to exploit are as follows.\n\n(1) The decision tree partitions the set X. In particular, each predicate either cuts X in two or keeps it intact. Furthermore, if X satisfies a DT predicate, we do not have to explore the complement branch. In a general hybrid system, there is no \"else case\" and the conditions may overlap; hence the (expensive) intersection computations have to be performed repeatedly and the complement branch has to be analyzed as well.\n\n(2) If the set X only leads to leaves with the same action, we do not need to split it (this happens quite often), which avoids the main source for loss of precision altogether. In a general hybrid system, combined with aspect (1) above, the connection is lost.\n\n(3) Axis-aligned predicates allow to use (simple but efficient) box abstractions.\n\n> Section 3.2, which describes the generalization of the solution to unbounded time problems, could perhaps use more details.\n\nThank you for the feedback. This section is indeed a very brief overview. The discussion is considered folklore in the reachability community, and the reason we included it is to be self-contained with respect to the experiments. In short, once the system finds itself in a state that was already analyzed previously, we can conclude that the system has reached a fixed point. This observation naturally generalizes to sets of states. We will make the description more formal.\n\n> The authors should also include some statement on how common axis-aligned predicates may be found in real-world DTCS. Is this a reasonable assumption?\n\nAxis-aligned predicates are very standard, also for DTCS. The tool Uppaal Stratego (David et al. 2015) learns such DT controllers, which are applied in industrial applications (e.g., to control smart homes [1*] and traffic lights [2*]). The tool dtControl (Ashok et al. 2020) also uses axis-aligned predicates.\n\n> The paper could use more discussion on its limitations, particularly regarding scalability.\n\nOur experiments already include a relatively large decision tree (depth 10, 177 nodes) for the drone quadrotor problem to show that large trees are also admissible, and as we argued in the paper, there exists a generic hybrid-system algorithm to verify DTCS, which is however impractical (Section 4.3). The main message of the paper is that a dedicated verification algorithm significantly outperforms such a generic algorithm.\n\nNevertheless we agree that scalability is an interesting question, however in reachability analysis evaluating scalability is not straight-forward, since neither does 1) the size of the tree nor 2) the dynamics of the system impact the algorithm in a predictable way. Below we give examples for both points.\n\n1) The size of the tree is not necessarily dominating because multiple leaves may share the same action, or some leaves may not be used at all during the execution. What matters is the number of times the decision boundaries are partially crossed by the reachable states after each time step. Given that different controllers may implement different policies, we cannot simply compare analyses with controllers of different size, since the verification performance may even improve for larger controllers. For instance, please see the two alternative controllers for the acrobot system (Fig. 9 in the supplementary material), whose behaviors differ significantly (Fig. 6). Note that in general we are interested in smaller trees since this is one of the main motivations for using decision-tree controllers over other (learned) non-interpretable controllers.\n\n2) It is hard to characterize the 'size' of a dynamical system. For instance, the competition on verifying continuous and hybrid systems (see [3*]) showcases that most verification solvers struggle with the *three-dimensional* Robertson chemical reaction, whereas the *seven-dimensional* Laub-Loomis model has several solvers that easily solve it. Note that this part is orthogonal to our work since our contribution is not in the algorithm for dynamical systems.\n\nWe will add this discussion to the paper.\n\n[1*] Larsen et al.: Online and Compositional Learning of Controllers with Application to Floor Heating. 2016.\n[2*] Bilgram et al.: Online and Proactive Vehicle Rerouting with Uppaal Stratego. 2020.\n[3*] Geretti et al.: ARCH-COMP22 Category Report: Continuous and Hybrid Systems with Nonlinear Dynamics. 2022."}, {"review_id": "Gv1gu8YhPH", "reviewer": "Reviewer_xs5Q", "summary": "The paper puts forward a verification method for decision tree-based systems in\ncontinuous time. The method implements a reachability algorithm that computes\nover-approximations of the set of reachable states for a sequence of time\nintervals until a time horizon is reached. The approximations at each step are\nderived using Taylor models.", "questions": "I have no questions. I thank the authors for the clarity of the text.", "limitations": "Adequately addressed.", "rating": 6, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "While the contribution is based on standard reachability-based verification\nmethods for hybrid and neural network-driven systems, the development of said\nmethods to verify decision trees is novel. \n\nGood experimental evaluation which shows improvements over the state-of-the-art\nin reachability for hybrid automata. This can in my view further improved  by\nincluding the following:\n    1. a discussion of the scalability of the method with respect to a wider\n    range of model sizes.\n    2. a discussion of the comparative amenability to reachability-based\n    verification of decision tree-based and neural network-based systems.", "weaknesses": "The paper does not include a discussion on the scalability of the proposed\nmethod.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you for the excellent review.\n\n> The paper does not include a discussion on the scalability of the proposed method.\n\nOur experiments already include a relatively large decision tree (depth 10, 177 nodes) for the drone quadrotor problem to show that large trees are also admissible, and as we argued in the paper, there exists a generic hybrid-system algorithm to verify DTCS, which is however impractical (Section 4.3). The main message of the paper is that a dedicated verification algorithm significantly outperforms such a generic algorithm.\n\nNevertheless we agree that scalability is an interesting question, however in reachability analysis evaluating scalability is not straight-forward, since neither does 1) the size of the tree nor 2) the dynamics of the system impact the algorithm in a predictable way. Below we give examples for both points.\n\n1) The size of the tree is not necessarily dominating because multiple leaves may share the same action, or some leaves may not be used at all during the execution. What matters is the number of times the decision boundaries are partially crossed by the reachable states after each time step. Given that different controllers may implement different policies, we cannot simply compare analyses with controllers of different size, since the verification performance may even improve for larger controllers. For instance, please see the two alternative controllers for the acrobot system (Fig. 9 in the supplementary material), whose behaviors differ significantly (Fig. 6). Note that in general we are interested in smaller trees since this is one of the main motivations for using decision-tree controllers over other (learned) non-interpretable controllers.\n\n2) It is hard to characterize the 'size' of a dynamical system. For instance, the competition on verifying continuous and hybrid systems (see [1*]) showcases that most verification solvers struggle with the *three-dimensional* Robertson chemical reaction, whereas the *seven-dimensional* Laub-Loomis model has several solvers that easily solve it. Note that this part is orthogonal to our work since our contribution is not in the algorithm for dynamical systems.\n\nWe will add this discussion to the paper.\n\n[1*] Geretti et al.: ARCH-COMP22 Category Report: Continuous and Hybrid Systems with Nonlinear Dynamics. 2022."}, {"review_id": "JBTHj0eZzN", "reviewer": "Reviewer_yJkM", "summary": "The paper presents an approach for verifying safety (reach-avoid) properties of controlled systems where  the state space of the system is continuous, its dynamics are continuous-time, and the policy/controller is described by a decision tree that chooses actions from a continuous action space. The proposed reachability-based verification algorithm invokes two main sub-procedures $post_f$ and $post_{\\mathcal{T}}$. Given an initial set of states and an action, $post_f$ computes the reachable states induced by the dynamics using standard techniques based on Taylor models. On the other hand, $post_{\\mathcal{T}}$ uses the structure of a decision tree to compute an overapproximation of all possible state-action pairs induced by the policy given an initial set of states. The design of $post_{\\mathcal{T}}$ as well as the overall verification algorithm are the primary contributions of this work. The paper also includes theoretical results establishing the soundness and the relative completeness of the verification algorithm, as well as results establishing the computational hardness of the safety verification problem for systems with decision tree controllers. Moreover, empirical evaluation shows the scalability of the verification algorithm compared to other, more generic techniques.", "questions": "My questions are related to comments above in the Weaknesses section.\n\n1. What structure of decision trees does the algorithm exploit? Is the structure primarily used in the design of Algorithm 3, or does Algorithm 1 also exploit the structure?\n\n2. Repeating the second comment above, the fixed point check seems to assume time-invariant dynamics. Is this correct? If so, why pass $t_0$ and $t_1$ as parameters to $post_f$ instead of simply passing $\\tau$?", "limitations": "The paper does not explicitly discuss the limitations and might benefit from a small discussion about the same. For instance, a discussion about the scalability of the approach and loss of precision due to approximations (related to the discussion in the last para of the conclusion) would be helpful.", "rating": 7, "confidence": 3, "soundness": 4, "presentation": 4, "contribution": 4, "strengths": "The paper presents an elegant verification algorithm as well as establishes hardness results for an interesting, well-specified family of controlled systems. The overall verification algorithm is clean and generic, and provides precise specifications that need to be satisfied by the sub-procedures $post_f$ and $post_{\\mathcal{T}}$ for the overall algorithm to be a sound and complete verifier. The key idea for computing reachability through the decision tree policy---namely, using box abstractions for efficient calculation of inclusion checks and bisection operation---is sensible and intuitive, and suggests clear directions for future research. The paper also presents useful insights on extending the analysis to unbounded time settings. The empirical evaluation supports the claim that designing a verification procedure that exploits the structure of Decision Tree Controlled Systems (DTCS) can lead to efficiency wins. I also greatly appreciate the quality of the writing and the formal rigor of the presented ideas (barring a few concerns described below).", "weaknesses": "My primary concerns have to do with the presentation of the technical material and the comparison with related work.\n\n1. The paper repeatedly suggests that exploiting the special structure of DTCS for verification is one of the key insights of the presented work but a clear explanation of this special structure and how it is exploited is only cursorily explained in Section 4.3 (with a more detailed explanation in the appendix). I am not an expert on the topic and for readers like me, it would help if these structural insights were clearly explained in the initial sections of the paper.\n\n2. I find the presented ideas about generalizing to unbounded time via fixpoints very interesting. However, the text in Section 3.2 seemed handwavy, and I would very much appreciate a more precise explanation of the ideas. For instance, I found the comments on line 226 (\"However, due to the discrete ...\") and on line 230 quite cryptic. I am also confused about the fact that while $post_f$ takes both a set of states and a time interval as input parameters, the fixed point check only considers the input states (i.e., assumes time-invariant dynamics). If the dynamics is time-invariant, why does $post_f$ need $t_0$ and $t_1$ as parameters? Can $t_0$ and $t_1$ be fixed as 0 and $\\tau$?\n\n3. The evaluation would be much stronger if there were a head-to-head comparison of the algorithm in this paper with reachability tools for hybrid automata. Section 4.3 briefly touches upon this, but a direct comparison for all four examples would be quite instructive. Another minor comment is that given the amount of detail in Figures 4,5, and 6, it would help to make them higher resolution.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you for the excellent review.\n\n> exploiting the special structure of DTCS for verification is one of the key insights of the presented work but a clear explanation of this special structure and how it is exploited is only cursorily explained.\n\nThank you for the suggestion. We will improve the explanation. For context, remember that in our setting, Algorithm 3 receives a set of states X, which is then propagated down the branches of the decision tree. Compared to analyzing a DTCS with a generic hybrid-system tool, the most important aspects of the special structure are as follows.\n\n(1) The decision tree partitions the set X. In particular, each predicate either cuts X in two or keeps it intact. Furthermore, if X satisfies a DT predicate, we do not have to explore the complement branch. In a general hybrid system, there is no \"else case\" and the conditions may overlap; hence the (expensive) intersection computations have to be performed repeatedly and the complement branch has to be analyzed as well.\n\n(2) If the set X only leads to leaves with the same action, we do not need to split it (this happens quite often), which avoids the main source for loss of precision altogether. In a general hybrid system, combined with aspect (1) above, the connection is lost.\n\n(3) Axis-aligned predicates allow to use (simple but efficient) box abstractions.\n\n> Is the structure primarily used in the design of Algorithm 3, or does Algorithm 1 also exploit the structure?\n\nAlgorithm 1 does not exploit the structure of decision trees (it is actually generic in the type of controller). But it exploits the structure of a periodic control system: Algorithm 3 only has to be called at fixed points in time, and Algorithm 2 has to be run for a fixed amount of time.\n\n> I find the presented ideas about generalizing to unbounded time via fixpoints very interesting. However, the text in Section 3.2 seemed handwavy\n\nThank you for the feedback. This section is indeed a very brief overview. The discussion is considered folklore in the reachability community, and the reason we included it is to be self-contained with respect to the experiments. In short, once the system finds itself in a state that was already analyzed previously, we can conclude that the system has reached a fixed point. This observation naturally generalizes to sets of states. We will make the description more formal.\n\n> The evaluation would be much stronger if there were a head-to-head comparison of the algorithm in this paper with reachability tools for hybrid automata [...] a direct comparison for all four examples would be quite instructive.\n\nThank you for the suggestion. The other examples could also not be solved by the generic approach. We agree that it would be interesting to provide further evidence, however (1) conceptually our approach is more efficient than a generic approach (explained above), and (2) since the generic approach could not provide any results, a tabular comparison is not possible.\n\n> given the amount of detail in Figures 4,5, and 6, it would help to make them higher resolution.\n\nAgreed.\n\n> the fixed point check seems to assume time-invariant dynamics. Is this correct? If so, why pass $t_0$ and $t_1$ as parameters to $post_f$ instead of simply passing $\\tau$?\n\nIndeed, we consider time-invariant systems. Yes, we could pass tau instead most of the time, except potentially in the last time interval. The correct value is t1-t0. We can see that passing the time interval can lead to confusions. Since t1-t0 is unnecessarily complex, we will instead pass tau as suggested and assume that T is a multiple of tau to simplify the presentation.\n\n> The paper does not explicitly discuss the limitations and might benefit from a small discussion about the same.\n\nOur experiments already include a relatively large decision tree (depth 10, 177 nodes) for the drone quadrotor problem to show that large trees are also admissible, and as we argued in the paper, there exists a generic hybrid-system algorithm to verify DTCS, which is however impractical (Section 4.3). The main message of the paper is that a dedicated verification algorithm significantly outperforms such a generic algorithm.\n\nNevertheless we agree that scalability is an interesting question, however in reachability analysis evaluating scalability is not straight-forward, since neither does 1) the size of the tree nor 2) the dynamics of the system impact the algorithm in a predictable way. Below we give examples for both points.\n\n1) The size of the tree is not necessarily dominating because multiple leaves may share the same action, or some leaves may not be used at all during the execution. What matters is the number of times the decision boundaries are partially crossed by the reachable states after each time step. Given that different controllers may implement different policies, we cannot simply compare analyses with controllers of different size, since the verification performance may even improve for larger controllers. For instance, please see the two alternative controllers for the acrobot system (Fig. 9 in the supplementary material), whose behaviors differ significantly (Fig. 6). Note that in general we are interested in smaller trees since this is one of the main motivations for using decision-tree controllers over other (learned) non-interpretable controllers.\n\n2) It is hard to characterize the 'size' of a dynamical system. For instance, the competition on verifying continuous and hybrid systems (see [1*]) showcases that most verification solvers struggle with the *three-dimensional* Robertson chemical reaction, whereas the *seven-dimensional* Laub-Loomis model has several solvers that easily solve it. Note that this part is orthogonal to our work since our contribution is not in the algorithm for dynamical systems.\n\nWe will add this discussion to the paper.\n\n[1*] Geretti et al.: ARCH-COMP22 Category Report: Continuous and Hybrid Systems with Nonlinear Dynamics. 2022."}, {"review_id": "FGBaGUrn2m", "reviewer": "Reviewer_77nS", "summary": "This paper introduces a novel verification algorithm that enables the verification of decision tree policies for continuous-time systems (also applicable to discrete-time systems). This approach ensures a sound and compact representation of reachable sets using Taylor models, which can be efficiently propagated through non-linear dynamics systems. The algorithm leverages the decision tree structure to propagate a set-based approximation of abstract reachable states through decision nodes, allowing for splits at decision boundaries. The effectiveness of this approach is demonstrated through the verification of safety for several decision trees that imitate neural-network policies in classic low-dimensional nonlinear control systems (e.g. cartpole). This method can provide robust safety and reachability guarantees for all system behaviors in these benchmarks.", "questions": "+ Why does the cart-pole benchmark in the paper use a non-standard initial state set? Could the verification algorithm be applied to the cart-pole system using the initial state set provided in the Gym environment?\n\n+ Is the verification algorithm capable of scaling to slightly more complex benchmarks, such as the pendulum and cart-pole swinging up tasks? Can it provide proof for the safety and reachability properties of these systems over an infinite time horizon?", "limitations": "The paper lacks a specific discussion on the scalability of the approach in terms of the size and complexity of control systems and decision trees that can be effectively verified. It would be helpful to address this aspect in the final version of the paper.", "rating": 7, "confidence": 5, "soundness": 4, "presentation": 3, "contribution": 3, "strengths": "+ The proposed algorithm marks a significant advancement as the first formal verification method for verifying reach-avoid properties in a decision-tree controlled system (DTCS) with continuous-time dynamics, including nonlinear systems. \n+ It achieves this by efficiently propagating a set of states through the system dynamics and tailoring general hybrid system reachability verification specifically for decision trees. The algorithm effectively utilizes axis-aligned predicates and interval-based set approximations to enhance the precision of abstract states, mitigating the wrapping effect. \n+ Moreover, the algorithm showcases its capability to generalize to unbounded time horizons by conducting reachable states fixpoint calculations, providing the potential for inductive safety verification over infinite time horizons. \n+ The theoretical analysis conducted in this paper provides insights into the main algorithm. \n\nThe paper introduces a tool for ensuring safety and reachability guarantees in decision-tree controlled systems, pushing the boundaries of verification techniques for learning-enabled systems in the context of continuous-time dynamics.", "weaknesses": "+ The proposed method consists of two parameterized procedures: one for analyzing dynamical systems and another for decision tree policies. The verification algorithm for dynamical systems is well-established in the related literature. To enhance the clarity of the paper, it would be beneficial to treat the verification procedure as background information in a dedicated section, allowing the paper to primarily focus on its contribution to the analysis of decision tree policy reachability. \n\n+ The evaluation presented in the paper falls short in adequately showcasing the limitations of the verification algorithm in practical settings. To provide a more comprehensive analysis, it would be valuable to explore scenarios where the reachability analysis may potentially diverge. For instance, investigating the scalability of the reachability analyzer to deep decision trees with a significant number of nodes would be helpful. Additionally, conducting an ablation study on decision trees with various shapes may provide insights into the algorithm's behavior.\n\n+ Furthermore, the benchmarks used in the evaluation appear to be simple, and it seems that a linear controller could be trained directly using reinforcement learning for all of these benchmarks and verified using reachability analysis. To strengthen the evaluation, it would be beneficial to include a benchmark scenario where a linear controller fails, thus highlighting the necessity and added value of decision tree controllers that can be additionally verified. For example,  cartpole swinging up could be a suitable benchmark to demonstrate the necessity of decision tree controllers.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you for the excellent review.\n\n> To enhance the clarity of the paper, it would be beneficial to treat the verification procedure as background information in a dedicated section, allowing the paper to primarily focus on its contribution to the analysis of decision tree policy reachability.\n\nThank you for the suggestion. We will restructure the paper accordingly.\n\n> The evaluation presented in the paper falls short in adequately showcasing the limitations of the verification algorithm in practical settings. To provide a more comprehensive analysis, it would be valuable to explore scenarios where the reachability analysis may potentially diverge. For instance, investigating the scalability of the reachability analyzer to deep decision trees with a significant number of nodes would be helpful.\n\nOur experiments already include a relatively large decision tree (depth 10, 177 nodes) for the drone quadrotor problem to show that large trees are also admissible, and as we argued in the paper, there exists a generic hybrid-system algorithm to verify DTCS, which is however impractical (Section 4.3). The main message of the paper is that a dedicated verification algorithm significantly outperforms such a generic algorithm.\n\nNevertheless we agree that scalability is an interesting question, however in reachability analysis evaluating scalability is not straight-forward, since neither does 1) the size of the tree nor 2) the dynamics of the system impact the algorithm in a predictable way. Below we give examples for both points.\n\n1) The size of the tree is not necessarily dominating because multiple leaves may share the same action, or some leaves may not be used at all during the execution. What matters is the number of times the decision boundaries are partially crossed by the reachable states after each time step. Given that different controllers may implement different policies, we cannot simply compare analyses with controllers of different size, since the verification performance may even improve for larger controllers. For instance, please see the two alternative controllers for the acrobot system (Fig. 9 in the supplementary material), whose behaviors differ significantly (Fig. 6). Note that in general we are interested in smaller trees since this is one of the main motivations for using decision-tree controllers over other (learned) non-interpretable controllers.\n\n2) It is hard to characterize the 'size' of a dynamical system. For instance, the competition on verifying continuous and hybrid systems (see [1*]) showcases that most verification solvers struggle with the *three-dimensional* Robertson chemical reaction, whereas the *seven-dimensional* Laub-Loomis model has several solvers that easily solve it. Note that this part is orthogonal to our work since our contribution is not in the algorithm for dynamical systems.\n\nWe will add this discussion to the paper.\n\n[1*] Geretti et al.: ARCH-COMP22 Category Report: Continuous and Hybrid Systems with Nonlinear Dynamics. 2022.\n\n> it seems that a linear controller could be trained directly using reinforcement learning\n\nThank you for the suggestion. We understand that this is only a suggestion to strengthen the story. Our acrobot benchmark requires a nonlinear controller. Note that our acrobot is similar to an up-swinging cart pole since the acrobot starts in a downwards position. It is true that some of the benchmarks admit a linear controller, however, obtaining suitable controllers is not the focus of our work.\n\n> Why does the cart-pole benchmark in the paper use a non-standard initial state set? Could the verification algorithm be applied to the cart-pole system using the initial state set provided in the Gym environment?\n\nThe set is a union of two sets. The reason we added this set was simply to demonstrate that our approach can naturally deal with non-convex shapes. The first set is similar to the set from the Gym environment. Adding the second set makes the union larger (and hence makes the problem harder).\n\nWe re-ran the experiment using the set from the Gym for the first set (i.e., still a harder challenge) and obtained a very similar result as before without any noticeable impact on reachable states and verification time. In the final version, we can use this refined initial set.\n\n> Is the verification algorithm capable of scaling to slightly more complex benchmarks, such as the pendulum and cart-pole swinging up tasks? Can it provide proof for the safety and reachability properties of these systems over an infinite time horizon?\n\nThe acrobot benchmark from our evaluation is similar to a pendulum or an up-swinging cart/pole system. Thus we expect that our algorithm may be able to provide a proof, provided the controller is safe and sufficiently stable."}]

Author rebuttal:

Meta-review: This paper proposes the reach-avoid problem for decision tree controlled systems in continuous time. The reach-avoid problem for decision tree controlled systems is to decide whether all trajectories reach the absorbing goal state without reaching the error set before the time limit. The goal is to overestimate the reachable states up to the time horizon using Taylor methods due to the undecidability of the problem.

The authors are encouraged to incorporated the feedback from the reviewers in the final version: (1) explicitly state which parts of the algorithm are specifically designed for use with DTCS and which are adapted from existing reachability/verification of dynamical systems algorithms, (2) improve the exposition on how the special structure of decision tree policies are exploited, (3) include the swing-up cart pole system results which the authors did not managed to do during the rebuttal phase, (4) improve the presentation quality of the whole paper, such as vectorization of all figures.

Overall, this is a nice contribution on verification of interpretable decision tree control systems to the community.
Decision: Accept (spotlight)