Reachability Analysis For Neural Network Aircraft Collision Avoidance Systems

Sequential decision-making problems can be modeled as Markov decision processes and solved with value iteration to produce a table of values. However, the numeric table can be too large to deploy in systems using limited or legacy hardware with memory constraints. Neural networks have been suggested as a way to significantly compress the data while still preserving performance. Because simulations evaluate only a finite number of inputs, simulations are not sufficient to guarantee that a continuous neural network function will perform safely for all possible inputs. This paper presents a methodology for providing safety guarantees when using neural network representations of decision-making systems. This methodology uses the neural network verification tool ReluVal to determine the actions available in regions of the state space. With the action space restricted, a conservative overapproximation of the system dynamics is used to ensure that unsafe regions of the state space are unreachable. Experiments with example systems inspired by the ACAS X family of aircraft collision avoidance systems show that neural networks giving either horizontal or vertical maneuvers can be proven safe. In addition, constraints on aircraft dynamics are relaxed to compute the uncertainty tolerated before safety is compromised. The reachability method is flexible and can incorporate uncertainties such as pilot delay and sensor error. These results suggest that the method could be used in the future to certify neural network collision avoidance systems for use in real aircraft.