Deep Neural Network Compression for Aircraft Collision Avoidance Systems

Abstract

One approach to designing decision making logic for an aircraft collision avoidance system frames the problem as a Markov decision process and optimizes the system using dynamic programming. The resulting collision avoidance strategy can be represented as a numeric table. This methodology has been used in the development of the Airborne Collision Avoidance System X (ACAS X) family of collision avoidance systems for manned and unmanned aircraft, but the high dimensionality of the state space leads to very large tables. To improve storage efficiency, a deep neural network is used to approximate the table. With the use of an asymmetric loss function and a gradient descent algorithm, the parameters for this network can be trained to provide accurate estimates of table values while preserving the relative preferences of the possible advisories for each state. By training multiple networks to represent subtables, the network also decreases the required runtime for computing the collision avoidance advisory. Simulation studies show that the network improves the safety and efficiency of the collision avoidance system. Because only the network parameters need to be stored, the required storage space is reduced by a factor of 1000, enabling the collision avoidance system to operate using current avionics systems.

References in corpus (3)

• Scikit-learn: Machine Learning in Python
• ADADELTA: An Adaptive Learning Rate Method
• On the Number of Linear Regions of Deep Neural Networks

Cited by in corpus (27)

• Formal Certification Methods for Automated Vehicle Safety Assessment
• Security and Privacy in the Emerging Cyber-Physical World: A Survey
• Guaranteeing Safety for Neural Network-Based Aircraft Collision Avoidance Systems
• Algorithms for Verifying Deep Neural Networks
• Parallelization Techniques for Verifying Neural Networks
• Neural Network Compression of ACAS Xu Early Prototype is Unsafe: Closed-Loop Verification through Quantized State Backreachability
• Toward Certification of Machine-Learning Systems for Low Criticality Airborne Applications
• Incremental Verification of Neural Networks
• Formally Verified Next-Generation Airborne Collision Avoidance Games in ACAS X
• Architecture-Preserving Provable Repair of Deep Neural Networks
• The Black-Box Simplex Architecture for Runtime Assurance of Autonomous CPS
• Long Short-Term Memory for Spatial Encoding in Multi-Agent Path Planning
• Safe-visor Architecture for Sandboxing (AI-based) Unverified Controllers in Stochastic Cyber-Physical Systems
• Multi-Agent Safe Planning with Gaussian Processes
• Generating Probabilistic Safety Guarantees for Neural Network Controllers
• Sound and Complete Neural Network Repair with Minimality and Locality Guarantees
• Formal Methods for Autonomous Systems
• dtControl: Decision Tree Learning Algorithms for Controller Representation
• Adversarial Examples for Electrocardiograms
• NeuroDiff: Scalable Differential Verification of Neural Networks using Fine-Grained Approximation
• Extending Neural Network Verification to a Larger Family of Piece-wise Linear Activation Functions
• Computing Linear Restrictions of Neural Networks
• Overestimation learning with guarantees
• Simplifying Neural Networks using Formal Verification
• Using Quantifier Elimination to Enhance the Safety Assurance of Deep Neural Networks
• Scaling up Memory-Efficient Formal Verification Tools for Tree Ensembles
• On Scalable Testing of Samplers