This repository contains code for generating safeable boundaries for collision avoidance neural networks and finding counter-examples via Reluplex.
The neural networks are generated by solving a discrete MDP and training a neural network to represent the Q-values. More information and code to generate the neural networks can be found here. The trained networks are located in the networks directory in this repository.
The neural networks represent a collision avoidance policy for a single-intruder encounter. The networks have four inputs:
- h (ft): Altitude of intruder aircraft relative to ownship
- v_own (ft/s): Climbrate of ownship
- v_int (ft/s): Climbrate of intruder
- tau (s): Time to loss of horizontal separation
Each network has nine outputs, representing the value of each collision avoidance advisory that could be given to the pilot. The advisory associated with the highest scoring advisory is given to the pilot. Furthermore, there are nine neural networks, one for each previous advisory given to the pilot, which allows the system to be consistent in giving alerts.
A near midair collision (NMAC) is said to occur if the intruder aicraft is within 100 ft vertically at tau=0. The networks are trained to prevent NMACs from occuring.
The safeable region for an advisory is defined as the region where the advisory can be given such that a future advisory exists that ensures no NMAC occurs. Therefore, it is unsafe to give an advisory in the region outside its safeable region. If the network always issues a safeable advisory whenever possible, than an NMAC will never occur if the intruder begins in the safeable region.
However, if an advisory is given in a state where a safeable advisory could be given, than the system is not safe. We want to verify that the networks never give an unsafe advisory when a safeable one exists. To do this, the region where all advisories are unsafe is computed, and the region outside this unsafe region but still outside an advisory's safeable region is created, which we call the advisory's unsafeable region.
After constucting the unsafeable region, we want to verify that the advisory is never given in its unsafeable region. We use Reluplex, a neural network verification tool that uses an algorithm based on the simplex method to verify if the advisory is ever given in the region. However, Reluplex requires linear bounds, so the region must be linearized. The region can be either over or under approximated and split into small regions with linear boundaries, which are fed to Reluplex as queries.
There are two Jupyter notebooks provided to demonstrate how the regions are created and verified with Reluplex.
The file reluplex.cfg specifies settings to check all queries related to a previous advisory and advisory. After setting up reluplexpy and ensuring that Reluplex is on the PYTHONPATH, run the config file as
python3 runReluplex.py reluplex.cfg