Verifying Aircraft Collision Avoidance Neural Networks Through Linear Approximations of Safe Regions

Understand

The next generation of aircraft collision avoidance systems frame the problem as a Markov decision process and use dynamic programming to optimize the alerting logic.

• The resulting system uses a large lookup table to determine advisories given to pilots, but these tables can grow very large.
• To enable the system to operate on limited hardware, prior work investigated compressing the table using a deep neural network.
• However, ensuring that the neural network reliably issues safe advisories is important for certification.