{'fraction_non_alphanumeric': 0.031917172438414854, 'fraction_numerical': 0.016660716410805666, 'mean_word_length': 4.468697123519458, 'pattern_counts': {'":': 0, '<': 2, '<?xml version=': 0, '>': 4, 'https://': 3, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 5, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Neural Network Compression of ACAS Xu is Unsafe: Closed-Loop Verification through Quantized State Backreachability

ACAS Xu is an air-to-air collision avoidance system designed for unmanned aircraft that issues horizontal turn advisories to avoid an intruder aircraft. Due the use of a large lookup table in the design, a neural network compression of the policy was proposed. Analysis of this system has spurred a significant body of research in the formal methods community on neural network verification. While many powerful methods have been developed, most work focuses on open-loop properties of the networks, rather than the main point of the system—collision avoidance—which requires closed-loop analysis. In this work, we develop a technique to verify a closed-loop approximation of ACAS Xu using state quantization and backreachability. We use favorable assumptions for the analysis—perfect sensor information, instant following of advisories, ideal aircraft maneuvers and an intruder that only flies straight. When the method fails to prove the system is safe, we refine the quantization parameters until generating counterexamples where the original (non-quantized) system also has collisions.


Introduction
The Airborne Collision Avoidance System X (ACAS X) is a mid-air collision avoidance system under development [25], with the ACAS Xu variant focused on collision avoidance for unmanned aircraft [19]. Originally designed offline using dynamic programming and Markov decision processes (MDPs) [20], the large rule table was compressed by a factor of 1000 using a set of neural networks [18]. The proposed system is an example of a neural network control system (NNCS), where the system's execution alternates between the aircraft dynamics and a neural network controller. As collision avoidance is safety-critical, analysis of the neural networks has spurred a significant body of research on neural network verification. Most existing work, however, focuses on open-loop verification, such as property φ 3 from the original work [19], which states, "if the intruder is directly ahead and is moving towards the ownship, [a turn will be commanded]." Open-loop properties can be expressed in terms of constraints over the inputs and outputs of a single execution of the neural network. However, satisfying openloop properties does not prove the system is safe, as this requires reasoning with the physical system dynamics-how the aircraft responds to turn commands. Also, the system is running continuously and may change advisories at a future time, complicating safety analysis. Verification of closed-loop safety of ACAS Xu NNCS under all designed operating conditions is thus a sort of grand challenge.
While verification of neural networks is continuously improving, an intriguing alternate approach has recently been proposed based on input quantization [14]. Rather than verifying the neural network directly, which requires reasoning about the semantics at each layer, the system's execution semantics are changed to round the inputs to a discrete set of possible values before running the network. To be clear, this type of quantization is a preprocessing layer before the network runs; it does not change the representation of the floating-point values inside the network itself. Through input quantization, proving open-loop properties of a neural network is reduced to the problem of network execution for each of a finite set of possible inputs. Due to the possibility of combinatorial explosion, this strategy can only work if the number of inputs is small, which is often the case for neural networks used in control systems. When the strategy is applicable, however, it enjoys several advantages: (i) batch execution of neural networks is often used in training and so optimized hardware like GPUs can be leveraged to enumerate the possible inputs for verification, (ii) the performance of the final quantized system approximates the performance of the original neural network and the approximation can be tuned through the quantization parameters, and (iii) the verification method only requires execution, and works regardless of the network size, the network architecture, or the layer types, unlike most neural network verification methods. So far, however, quantization has only been considered for open-loop properties.
In this work, we propose an approach to formally verify quantized closedloop NNCS. Although the technique is general, we focus primarily on proving safety for quantized ACAS Xu. Two key ideas are needed to make this work: (1) we perform state quantization rather than input quantization and (2) we use backreachability from the unsafe states to reduce the number of partitions. We prove the approach is sound and complete, in the sense that by continuing to refining quantization parameters, either the quantized system will eventually be proven safe, or an unsafe counterexample will be found in the original system. When the method fails to prove safety of quantized ACAS Xu NNCS, we refine the quantization values until discovering cases where the original (unquantized) ACAS Xu system fails. We also show that with stricter assumptions on the ownship aircraft's velocity, the quantized system can guarantee safety.

Background and Problem Formulation
ACASXu Neural Network Control System. We are interested in safety verification and falsification of the closed-loop ACAS Xu system depicted in Figure 1. The system computes advisory commands to control an ownship aircraft with physical dynamics described by a set of ordinary differential equations (ODEs), trying to avoid collisions with a nearby intruder.
A detailed description of the inputs and actions in the system is shown in Table 1. The system receives 7 inputs about the state of an ownship and a nearby intruder aircraft, I = {ρ, θ, ψ, v own , v int , τ, a prev }, and produces one of five possible advisories for the ownship, A = {coc, wl, wr, sl, sr}.
The ACAS Xu neural networks are a collection of 45 deep ReLU neural networks with 6 layers and 50 neurons per layer for each network. Control switches between different neural networks N aprev,τ based on the previous advisory a prev (total of 5 choices) and the time until loss of vertical separation τ = {0, 1, 5, 10, 20, 50, 60, 80, 100} (total of 9 choices). For example, the network N 5,3 will be invoked if the previous advisory is a prev = sr and τ = 5. If the ownship and the intruder are at the same altitude, then τ = 0 and only five neural network controllers need to be used, N 1,1 , N 2,1 , N 3,1 , N 4,1 , and N 5,1 .
ACAS Xu Plant Model. Before we describe the plant model used in analysis, we first state our system assumptions: (i) the intruder flies in straight-line trajectories with constant speed, (ii) the ownship flies with constant speed and  its heading is adjusted every second (the NNCS control period), (iii) the actions correspond to heading changes in the intruder of 1.5 deg/sec for weak turn commands, 3.0 deg/sec for strong turns and 0.0 deg/sec for clear-of-conflict commands [18], (iv) there is no sensor noise and (v) advisories are followed exactly and immediately. Many of these are fairly strong and the real system would need to be robust to maneuvering intruders, pilot delay and sensor noise. From a safety proof perspective, however, we would want the system to at least be safe under these ideal assumptions.
To model the state of the system with these assumptions, we use Cartesian coordinates. The values x own , y own , x int , y int refer to the x and y positions of the ownship and the intruder; v own = (v x own ) 2 + (v y own ) 2 and v int = (v x int ) 2 + (v y int ) 2 are the speed of the ownship and the intruder; θ own and θ int are the heading of the ownship and the intruder w.r.t the x axis. The system performs idealized turn maneuvers modeled with Dubins aircraft dynamics: Equation 1 does not show clearly how the aircraft can be controlled by changing their heading. Taking derivatives of the Equation 1 one more time and noticing thatθ own is a constant between advisories,θ own = (π/180)u = c(rad/s), and then takingθ int = 0, we obtain the following 8-d linear system dynamics: The linear model described in Equation 2 is valid for only one control step, with a fixed control signal u, which may be either −3, −1.5, 0, 1.5 or 3 deg/s depending on the specific command. Therefore, this model can be considered as a piece-wise linear model of the system. From the plant state variables, we can obtain the inputs for the neural network controller as follows.
Reachability with AH-Polytopes. An AH-polytope is a set representation that informally is an affine transformation of a half-space polytope, where the affine transformation and polytope terms are explicitly kept separate. This set representation is often used in hybrid systems reachability analysis for linear systems [4,2,26], where it is also called a linear star set [7], constrained zonotope [27], affine form [11], or symbolic orthogonal projection [10]. Importantly for this work, discrete-time reachability of systems with linear dynamics,ẋ = Ax, can be expressed exactly using this set representation, as it amounts to a linear transformation of the entire set by the matrix exponential e At , where t is the time step. Further, operations like intersections can be performed exactly on AH-polytopes, as well as optimization which uses linear programming. A formal definition and operation list is provided in Appendix A.
Problem Formulation. Verifying the safety of the closed-loop ACAS Xu NNCS system means proving the absence of unsafe paths under all operating conditions. For simplified presentation, we consider a discrete-time version of the problem, where we only check for collisions once a second when the system is activated. Our analysis could be extended to continuous time through conservative timediscretization approaches from hybrid systems reachability analysis [9], which essentially bloat the initial set and then perform discrete-time analysis.

Definition 1 (Path). A path is written as s
where successive values of s i and s i+1 correspond to the state of the system one second apart according to the plant dynamics in Equation 2. The command α i is the system output from state s i using α prev = α i−1 , with s 1 using the coc network. Paths can either be in-plane, whereτ = 0 and τ = 0 in all states and so the N 1, * networks get used to generate all commands, or out-of-plane, whereτ = −1. In the out-of-plane case, each state in the path should decrease τ by one second.
An unsafe path has s 1 as an initial state and s n as an unsafe state.
Definition 2 (Initial State). An initial state of the state of the system is one where the aircraft are outside of the system's operating range (ρ > 60760 ft).
Definition 3 (Unsafe State). Unsafe states are defined to be any states in the near mid-air collision (NMAC) cylinder [24], where the horizontal separation ρ is less than 500 ft and the time to loss of vertical separation τ is zero seconds.
The operating conditions where the ACAS Xu NNCS system should ensure safety are extracted based on the training ranges used for the neural networks. The system should be active when the distance between aircraft ρ ∈ [0, 60760] ft, otherwise clear-of-conflict is commanded. The valid values for the ownship velocity are v own ∈ [100, 1200] ft/sec, valid values for intruder velocity are v int ∈ [0, 1200] ft/sec, and the angular inputs θ and ψ are both between −π and π.

Quantized State Backreachability for ACAS Xu
Our verification strategy is to compute the backwards reachable set of states from all possible unsafe states, trying to a find a path that begins with an initial state. We first partition the unsafe states along state quantization boundaries.

Partitioning the Unsafe States
Since the system advisories are only based on relative positions and headings, we eliminate symmetry by assuming that at the time of the collision the intruder is flying due east and at the origin. We then consider all possible positions of the ownship to account for all possible unsafe states. Three quantization parameters are used in the analysis: q pos to quantize positions, q vel to quantize velocities, and q θ to quantize the heading angle. Based on these parameters, we partition the unsafe states into 8-d AH-polytopes covering the entire set of possible unsafe states. The eight dimensions correspond to the system states in the linear dynamics in Equation 2, including positions x, y, and velocities v x , v y for both the ownship and intruder. Associated with each partition, we also enumerate the five possible previous commands α prev and two possibilities for whether there is a relative vertical velocity-whether the time to loss of vertical separation is fixed at 0 or decreasing,τ ∈ {0, −1}.
To create partitions, the x own and y own values are divided into a grid based on q pos . The intruder position (x int , y int ) is set to (0, 0). The intruder and ownship velocities are partitioned based on q vel , which gets reflected in the x and y velocity state variables for the two aircraft. The intruder is moving due east, so v y int = 0 and v x int is set to the range of intruder velocities corresponding to the current partition. The heading of the angle of the ownship is partitioned based on q θ , where each partition has a lower and upper bound on the heading [θ lb own , θ ub own ]. From the current range of values for the ownship heading and the range of values for the ownship velocity, we can construct linear bounds on v x own and v y own . This is done by connecting five points (a, b, c, d, e), where a and b are the points at two extreme angles and minimum velocity, c and d are the two extreme angles and max velocity, and e is the point at the intersection of the tangent lines of the maximum velocity circle at c and d. A visualization is shown in Figure 2. We generally use q θ = 1.5 deg (as it makes for a cleaner backreachability step), which guarantee all possible v x own , v y own values are covered.

Backreachability from Each Partition
Once a covering of the entire set of unsafe states is performed, for each partition we compute the exact set of predecessor states that can lead to the states in the partition at a previous step. This process is repeated until either no predecessors exist or an initial state predecessor is found 3 , as described in Definition 2. In the latter case, a path exists from an initial state to a partition of the unsafe states in the quantized closed-loop system. Otherwise, if no partitions contain unsafe paths, then the quantized closed-loop system is safe.
The check state function in Algorithm 1 recursively computes and checks predecessors. The input is a state set S, which is initially an 8-d partition of the unsafe states represented as an AH-Polytope, as well as the associated value of α prev and the time to loss of vertical separation, τ = 0 in all unsafe states.
In line 1, backreach step is called, which returns the predecessor set of states as an AH-polytope P. This is done by taking the linear derivative matrix A c from Equation 2 with the value of c corresponding to α prev , and then computing the matrix exponential W = e −Ac . The resulting matrix is the solution matrix for the system one second prior. A linear transformation of the AH-polytope S is then performed by W in order to obtain P. In line 2, the value of the time to loss of vertical separation at the previous step τ prev is computed. This either always equals 0 ifτ = 0 for the current partition corresponding to in-plane flight, or increases by 1 at each call to check state ifτ = −1 for out-of-plane flight.
Next, the algorithm computes states in P where the command produced by the networks was α prev and the time to loss of vertical separation was the value at the previous step, τ prev . This requires iterating over the five possible networks that could have been used at the prior state (the loop on line 3). For each network (corresponding to α prevprev ), we check each quantized state in P (line 6).
The possible quantized states returns a list of quantized states, which are 5-tuples of integers, q = (dx, dy, θ own , v own , v int ). The dx and dy terms correspond to the difference in positions between the intruder and ownship, divided by the position quantum q pos . The θ own term is the heading angle divided by q θ , and the velocities v own and v int are the fixed aircraft velocities, integer divided by q vel . The function computes the possible quantized states by using linear programming to find P's bounding box, and then looping over possible quantized states to check for feasibility when intersected with AH-polytope P.
Line 7 runs the neural network corresponding to α prevprev on quantized state q to check if the correct command (α prev ) is obtained. This process requires converting from the quantized state (a 5-tuple of integers) to continuous inputs for the neural network. To do this, we use Equation 3, noting that the θ own is quantized using q θ , θ int is always 0, and the computation of ρ and θ uses the dequantized value of dx and dy (x int − x own is taken to be qpos 2 + dx * q pos ). When the network output matches the required α prev command, line 8 adds the quantized state to the valid list of predecessors predecessor quanta. Otherwise, line 12 sets the all correct flag to false, since some of the quantized states are not valid predecessors. Line 10 checks if the predecessor state satisfies the initial state condition, in which case an unsafe path has been found. On this line, ρ min (q) is the minimum aircraft separation distance in the quantized state q, which must be greater than 60760 ft in an initial state.
After classifying each quantized predecessor state, either all quantized states had the correct output or some did not. Based on this, we either recursively call check state on the entire set P (line 16), or we split the set P into parts, and only recursively call check state on parts that had the correct output. On line 22, quantized to state set returns the 8-d continuous states corresponding to the quantized state q, which is then intersected with P before being recursively passed to check state. When splitting is performed, it is possible that no states had the correct output (predecessor quanta may be empty).
An illustration of the algorithm is provided in Figure 3. In the figure, the set P is covered by nine quantized states returned by possible quantized states (the dots on the right side). Of these nine, eight have a correct output (blue dots), and one has an incorrect output (red dot). In this case, the algorithm would split the set P into eight parts and call check state on each recursively 4 . We next prove the described algorithm is sound with respect to the safety of the quantized closed-loop system. Theorem 1 (Soundness). If check state returns safe for every partition, the quantized closed-loop system is safe.
Proof. We proceed by contraction. Assume the quantized closed-loop system is unsafe and so these exists a finite path from an initial state to an unsafe state, Since the unsafe state partitioning covers the full set of unsafe states, the unsafe state s n is in some partition. We can follow the progress of s n ∈ S, through check state at each recursive call.
At each call, s i ∈ S has a predecessor s i−1 ∈ P that gets to s i using command α i−1 . In the call to check state, α prev will be α i−1 . The value of τ prev is incremented at each call on line 2 and so always correctly corresponds to s i−1 . Since s i−1 ∈ P, s i−1 will also be in one of the quantized states q i−1 checked on line 6. The existence of the counterexample path segment means that the condition on line 7 will be true when α prevprev = α i−2 , and so q i−1 will be added to predecessor quanta. Since s i−1 is both in P and in the state set corresponding to a quantized state in predecessor quanta, it will be used in a recursive call to check state. This argument can be repeated for all states in the unsafe path back to the initial state s 1 , which would have been returned as unsafe on line 10 rather than used in a recursive call. This contradicts the assumption that check state returned safe for every partition.

Falsification of Original (Unquantized) System
The algorithm in the previous section can be used to efficiently find unsafe paths of the original (unquantized) ACAS Xu closed-loop system. This is done by repeatedly calling the algorithm with smaller and smaller quantization constants q pos , q vel and q θ and checking the quantized system for safety.
At each step if the safety proof fails, with small modifications to check state we can get the trace corresponding to the unsafe path for each partition. In particular, rather than simply returning unsafe on line 10, we can instead return the set of unsafe initial states quantized to state set(q) ∩ P. A witness point inside this set can be obtained through linear programming 5 . This witness point is then executed on the original system, without quantization, checking for safety. If the witness point is safe in the non-quantized system, the quantization constants are refined by taking turns dividing each of them in half.
Theorem 2 (Completeness). By following the falsification approach above and repeatedly refining q pos , q vel and q θ , either we will prove the quantized system is safe or find an unsafe trace in the original, unquantized system.
Proof. First, consider the case that the system is robustly unsafe, which we define as there existing a ball B init of initial states of radius δ > 0 that all follow the same command sequence α 1 , α 2 , . . . , α n and end in the unsafe set. Since all the initial states follow the same command sequence, the linear transformations corresponding to the commands α 1 , α 2 , . . . , α n , which we call A c1 , A c2 , . . . , A cn can be multiplied together into a single matrix that transforms initial states to unsafe states, A C = A cn . . . A c2 A c1 . The matrix A C is invertible since all the transformations corresponding to each command A c1 , A c2 , . . . , A cn are invertible. The matrix A C being invertible means that since the volume of the ball in the initial states B init is nonzero, the corresponding set of states in the unsafe set is an ellipsoid with nonzero volume, which we call E unsafe . Through refinement of the quantization parameters q pos , q vel and q θ , eventually a partition will be entirely contained in E unsafe . When this happens, every witness point of the quantized counterexample from that partition will be in B init , and so will be an initial state of an unsafe oath of the original, unquantized system.
Perhaps less practically, even if the original system is not robustly unsafe, the process still will theoretically terminate when finite-precision numbers are used in the non-quantized system, such as with ACAS Xu neural networks that use 32-bit floats. As the quantization values are halved, the difference between the unsafe state in the quantized and nonquantized system is also reduced, until it reaches numeric precision.
The second case may seem like one needs to split the entire state space up to machine precision, which would make it very impractical. However, if the goal is to search for counterexamples, then the process can first refine the regions that were found as unsafe using the previous quantization values, in a depthfirst search manner. In this way, when the system is unsafe the process would not need to immediately refine the entire state space in order to find these counterexamples. Also keep in mind that the quantized system being safe is a valid outcome of this refinement process, and this does not mean that the original, unquantized system, is safe.

Evaluation
We implemented the approach and set out the prove the safety of quantized closed-loop ACAS Xu NNCS 6 . We ran the measurements on an Amazon Web Services (AWS) Elastic Computing Cloud (EC2) server with a c6i.metal instance type, which has an Intel Xeon processor with turbo frequency 3.5 GHz, 128 virtual CPUs, and 256 GB memory. The algorithm is easily parallelized as proofs for each partition of the unsafe states can be checked independently.

Complete Proof of Safety Attempt
We first attempted a proof of safety for the entire range of unsafe states for ACAS Xu. For this, we started with large quantization values, q pos = 500 ft, q vel = 100 ft/sec, and q θ = 1.5 deg. In this case, the unsafe near-mid-air collision circle of radius 500 ft can be covered with 4 partitions, the complete velocity range of the ownship [100, 1200] needs 11 partitions, the velocity of the intruder [0, 1200] needs 12 partitions, the heading angle of the ownship is divided into This quickly, within a minute, finds counterexamples in the quantized system. When the witness initial states of the quantized counterexample are replayed on the original non-quantized ACAS Xu system, according to the falsification algorithm from Section 3.3, these were also found to be unsafe. The exact runtime before an unsafe case is found depends on the order in which the partitions are searched, but we found that although changing this did affect the counterexample produced, the runtime was usually less than a minute. Two of the unsafe cases are shown in Figure 4 in parts (a) and (b).
In the situation shown in Figure 4(a), the intruder starts beyond the range of the network (ρ > 60780 ft). As soon as the intruder gets in range, a turn is commanded, but the velocity of the ownship is slow and a collision still occurs. This situation looks like it could be fixed by increasing the range of the system beyond 60780 ft-likely requiring retraining the networks-to allow a turn to be commanded earlier. Alternatively, perhaps adding a "do not turn" option as a possible output would be another way to address this scenario (clear-of-conflict could allow the ownship to maneuver as desired which may be unsafe here).  shows another unsafe case found that is particularly concerning. This is a tail-chase scenario, although the ownship is already moving away from the straight-line trajectory of the intruder. The system nonetheless commands a turn and actively maneuvers the ownship aircraft back into the path of the intruder. This situation demonstrates one of the dangers of the collision risk metric used to evaluate the effectiveness of original ACAS Xu system, which compares the number of near mid-air collisions (NMAC) with and without the system using a large number of simulations. Although the system can be effective by this metric, in specific cases it may still create collisions that would not otherwise have occurred, as demonstrated in this scenario.

Proving Safety in More Limited Operating Conditions
As the proof of safety for the entire operating range failed, we next tried to prove safety in restricted operating conditions. Many of the unsafe situations found, including the two above, had a slow ownship velocity and a fast intruder. By making the ownship fast enough, we hypothesized collisions could be avoided.
When we restricted the range of v own to be in [1000, 1200] ft/sec, using q pos = 250 ft, q vel = 50 ft/sec, and q θ = 1.5 deg, we were able to guarantee safety of the quantized closed-loop neural network control system. The proof requred checking 3.7 million cases and took about 32 minutes. The longest runtime for any single call to check state (checking a single partition) was 63 seconds.
Reducing v own further to [950, 1000] ft/sec made the quantized system unsafe. Following the falsification approach from Section 3.3, we refined the quantization parameters until we were able to find a counterexample in the original unquantized ACAS Xu closed loop system. In this case, the ownship was moving with v own = 964.1 ft/sec, and the time to loss of vertical separation τ was initially 75 secs (the quantized system was safe for in-plane flight, withτ = 0). This case is shown in Figure 4(c).
From the other side, we can alternatively attempt to prove safety under the assumption that the intruder is slow without restricting the ownship's velocity. In this case, the method also finds unsafe counterexamples in the unquantized system, such as the 159 second trace shown in Figure 4(d) with v int = 390.1 ft/sec. The full trace for this situation is provided in Appendix B.4 and has a peculiar characteristic. The command switch from weak-left to strong-right a few seconds before the collision corresponds to the relative position angle θ wrapping from −π to π. This discontinuity in the network input between successive steps is a strong candidate root cause of the eventual near mid-air collision.

Comparison with Other Approaches
As far as we are aware, the proposed method is the first to provide safety guarantees while varying all of the operating conditions of the ACAS Xu NNCS.
One related technique, based on computing discrete abstractions and forward reachability was able to provide safety guarantees for the similar Horizontal CAS [16]. This system is simpler to analyze than ACAS Xu: the inputs were modified to take in Cartesian state variables, the operating range was smaller (ρ < 50000), there were fewer neural networks in the system, each of which had half as many neurons per layer, and critically, fixed velocities of v own = 200 and v int = 185 were considered, rather than using velocity ranges. Despite these simplifications, analysis took 227 CPU hours, mostly on the neural network analysis step to analyze 74 million partitions. For a comparison, we analyzed the larger ACAS Xu neural networks with the proposed state quantization and backreachability method, using the same fixed v own and v int values. Using a quantized system with q pos = 250 ft and q θ = 1.5 deg, the method proved safety of all 38400 partitions of the unsafe states in 60.6 seconds. Also note that while the Horizontal CAS discrete abstraction approach can sometimes prove safety, it would be poor at generating counterexamples, as abstract reachability overapproximates the true reachable set; abstract counterexamples do not correspond to real counterexamples. In contrast, the backwards reachability performed in Algorithm 1 is exact with respect to the quantized system, and the gap between the quantized and original system can be reduced by refining the quantization parameters, making it highly effective for counterexample generation.
We also compared our method with simulation-based analysis, which cannot provide guarantees about system safety but should be able to find unsafe counterexamples if enough simulations are attempted, as the system was shown to be unsafe. In earlier work [17], 1.5 million encounters were simulated for the ACAS Xu NNCS system to evaluate the risk of collisions, sampling from probability distributions of actual maneuvers and taking into account sensor noise. We evaluated the same number of simulations without sensor noise and sampling over the entire set of operating conditions, in order to match the assumptions used in the safety proof. We generated uniform random initial states by considering an initial ρ ∈ [60760, 63160] and θ, ψ, v own and v int in their entire operating range. When consideringτ = −1, we assigned the initial value of τ between 25 and 160 seconds, as the unsafe case in Figure 4(d) was a 159 second trace. We repeated the process of running 1.5 million simulations one hundred times each for botḣ τ = −1 andτ = 0, in order to better account for statistical noise.
In theτ = 0 case, each batch of 1.5 million simulations found on average 17.07 unsafe paths. The unsafe cases were dominated by situations where the intruder velocity was low and the ownship velocity was high. The mean value of v int was 997.8, with a standard deviation of 147.5. The lowest values of v int over the unsafe cases in all 150 million simulations was 927.6, whereas Figure 4(d) showed a case with v int =390.1 found with our approach. The mean value of v own in the unsafe cases was 133.4 with a standard deviation of 43.0. The greatest value of v own over all the unsafe cases found with 150 million simulations was 452.3, whereas our approach found an in-plane case with v own =881.6.
The performance of simulation analysis for the out-of-plane case is even worse, as the initial state must also correctly choose the value of the time to loss of vertical separation τ in order to find a collision. Each batch of 1.5 million simulations withτ = −1 had on average 0.07 unsafe simulations. The maximum ownship velocity v own in the unsafe cases had a mean of 175.4 with a standard deviation of 77.9. The greatest value of v own over the unsafe cases found in all 150 million simulations was 343.0, whereas our approach found a case with v own =964.1, as shown before in Figure 4(c).
Overall, while simulation analysis may find some unsafe cases, it would be difficult to find the extreme velocity cases discovered with the proposed approach. Further, simulation analysis is incomplete and cannot prove safety for the system under subsets of operating conditions as was done in Section 4.2.

Related Work
Simulation-based Safety Analysis. The ACSX Xu system was originally evaluated using 1.5 million simulations [21] based on Bayesian statistical encounter models. This uses relaxed assumptions compared with our work, such as allowing for changes in acceleration. The output of such analysis is not a yes/no assessment of safety, as the system can clearly be unsafe if the intruder is faster than the ownship and maneuvers adversarially, but rather a risk score assessment of the change in safety compared to without using the system. Via simulation, given a bounded uncertainty in sensing and control, the probability of near-mid-air-collision was about 10 −4 [17]. Although simulations show that the system may be unsafe, we do not know if the collision occurs due to the uncertainty or the system itself. In this work, we showed that the closed-loop ACAS Xu system is actually unsafe even if we have perfect sensing and control. Verification of NNCS. The Verisig approach [13] verifies a NNCS by transforming a network with a sigmoidal neural network controller to an equivalent hybrid system that can be analyzed with Flow* [5], a well-known tool for verifying nonlinear hybrid systems. Another method [12,8] combines polynomial approximation of the neural network controller with the plant's physical dynamics to construct a tight overapproximation of the system's reachable set. The star set approach [28] shows that the exact reachable set of an NNCS with a linear plant model and a ReLU neural network controller can be computed, although this is expensive when initial states are large. These methods build upon open-loop neural network verification algorithms [22,29], which can be difficult to scale to large complex networks [3] and can sometimes lose soundness due to floating-point numeric issues [32]. The proposed quantization analysis only needs to execute neural networks, and so does not suffer from these problems. Verification of the Closed-loop ACAS Xu System. Existing works have verified NNCS with a single neural network controller on a small set of initial states [15]. The closed-loop ACAS Xu system involves switching between multiple neural networks and has a large set of initial states, creating a unique challenge for verification. The simplified Horizontal CAS system was analyzed using fast symbolic interval analysis for neural network controllers [31] to construct a discrete abstraction [16]. This method can consider sensor uncertainty, inexact turn commands, and pilot delay, although simplified assumptions are made, as discussed in Section 4.3. Recently, the original closed-loop ACAS Xu system has been verified with the extension of the symbolic interval method [6] and the star-based reachability [23] in nnv [30] and nnenum [1]. These approaches use forward reachability analysis and provide sound but not complete verification results. Further, verification has only been demonstrated for specific scenarios with small sets of initial states, not the full operating conditions considered here.

Conclusion
In this work, we set out to prove the safety of the closed-loop ACAS Xu NNCS using a new algorithm based on state quantization and backreachability. In principle, the approach could verify the safety of a quantized approximation to the closed-loop ACAS Xu NNCS system under all valid initial states and aircraft velocities. In the process, we found many unsafe scenarios where the original, unquantized system results in near mid-air collisions, despite ideal assumptions on sensors and maneuvering. Compared with random simulation-based analysis, we could find counterexamples at more extreme velocities, as well as provide proofs of safety of the quantized closed-loop system in more limited scenarios.
The approach is could be attractive for certification. A system with a quantization layer behaves like a large lookup table, and the method is therefore effective on any size network with any layer type, and may even be applicable to other machine learning approaches. The trade-off of quantization is usually a small degradation in performance of the controller, with a significant benefit of reducing analysis complexity and allowing for the possibility of verification. The AH-Polytope representation is informally an affine trasnformation of a halfspace polytope, where the affine transformation and polytope are kept explicitly separate. This representation is extremely useful for reachability of continuous and hybrid systems with linear dynamics. The name was introduced fairly recently [26], although it has been regularly used for hybrid systems reachability analysis as well as neural network verification. Here, we provide a formal definition and list key set operations for the representations used in our approach.
Definition 4 (AH-Polytope). An AH-Polytope is a tuple Θ = V, c, C, d that represents a set of states as follows: We generally refer to both the tuple Θ and the set of states Θ as Θ as it is clear from context which one we are referring to.

Proposition 1 (Affine Mapping
). An affine mapping of an AH-Polytope Θ = V, c, C, d with a mapping matrix W and an offset vector b is a new AH-

Proposition 2 (Linear Transformation). A linear transformation of an AH-
Polytope with a matrix W is an affine mapping using mapping matrix W and an offset vector of b = 0. Proposition 4 (Linear Optimization). Linear optimization in given a direction w ∈ R n over a star set Θ = V, c, C, d can be solved with linear programming as follows: min(w T x), s.t. x ∈ Θ = w T c + min(w T V α), s.t. Cα ≤ d.

B Unsafe Counterexample Details
Here, we provide detailed traces on the unsafe counterexamples found in the original ACAS Xu NNCS shown previously in Figure 4.

B.1 Counterexample Outside Range
Fig. 5: The network advises the ownship to turn immediately once the intruder is in range, when ρ becomes less than 60760 ft, but a collision still occurs.
When doing a full proof of safety of the system, counterexamples were generated for the original, nonquantized ACAS Xu NNCS. In this scenario, the planes were at the same altitude,τ = 0, and the system commanded a turn as soon as the intruder was in range. Nonetheless a collision occurred. This indicates perhaps a larger range for ρ should be considered, which would require retraining the network with more data in this range. A visualization of the counterexample is shown in Figure 5. A video of the simulation is online: https://youtu.be/aeh_9GVHNzE. The full trace is provided in Table 2. Row 3 of the table show the system issuing a turn command as soon as the distance between aircraft ρ becomes less than 60760 ft.  In this scenario, the planes are at the same altitude,τ = 0, and the ownship has cleared the path of the intruder. Nonetheless, the system advises the ownship to turn, which eventually leads it back into the path of the intruder, causing a near mid-air collision. A visualization of the unsafe scenario is shown in Figure 6. A video of the simulation is online: https://youtu.be/s-ZXqMdg2GA. The full trace is provided in Table 3. The unrounded initial state is ρ = 61462.16874158125 ft, θ = 2.8797448888478536 rad, ψ = −0.2973898012094359 rad, with velocities v own = 114.27575493691512 ft/sec, and v int = 1100.31313 ft/sec.  Using the described quantized backreachability approach, we found an unsafe situation with v own > 950 ft/sec. In this case, the system was safe for in-plane flight, whenτ = 0, but unsafe when there was a difference in vertical velocity,τ = −1. A visualization of the counterexample is shown in Figure 7. A video of the simulation is online: https://youtu.be/nLd5XSrS-CA. From the visualization, it looks like the collision was avoidable if the system did not continue to advise a right turn for the final few seconds. The full trace is provided in Table 4.  Using the described quantized backreachability approach, we found an unsafe situation with v int < 400 ft/sec. A video of the simulation is online, https: //youtu.be/1uoSOgAl54Q, and a visualization of the counterexample is shown in Figure 8.
The 159 second trace is provided in Table 5. Examining the trace, an interesting observation is that the command switch from weak-left to strong right at step 142 corresponds to the relative position angle θ wrapping from −π to π. This discontinuity in the network input between successive steps is likely the cause of the eventual near mid air collision. Table 5: Unsafe case with slow intruder with velocity v int = 390.1 ft/sec and in-plane flight (τ = 0 andτ = 0). The unrounded initial state is ρ = 60959.597800102 ft, θ = -0.7461997148243538 rad, ψ = 2.1997877266124295 rad, v own = 110.84814862335269 ft/sec, and v int = 390.10329256 ft/sec.