A proposed set of benchmarks for the VNN21 competition. This is a network which consists of (i) a conditional generative adversarial network (cGAN) with two latent inputs and two conditioned inputs concatenated with (ii) an image-based state estimator. The cGAN is used to model images from a camera mounted on the wing of an aircraft and taken at different locations along a runway. The first two inputs to this network are latent variables which can vary from -0.85 to 0.85 and allow the cGAN to produce a variety of different images for each position on the runway. The third input is the cross-track position (distance from the centerline) for the aircraft, while the fourth input is the heading of the aircraft. The output of the concatenated network is an estimated cross-track position and heading. The control effort for the taxiing aircraft is then given by a linear combination of the outputs of the network. We would like to be be able to ask questions about the possible control effort assuming the state estimation network will be passed images from the image model represented by the cGAN. For additional context and justification of this network please see the paper Verification of Image-based Neural Network Controllers Using Generative Models. As a result, we created a series of queries .vnnlib format for different rectangular regions in the input space that ask about how large or small the control effort can be in that region.
The network can be found under networks/GANControl/full_mlp_best_conv.onnx. The queries can be found in queries/.