Verification of Neural Network Control Systems in Continuous Time

TL;DR

This work tackles the challenge of formally verifying neural network controllers operating with continuous actuation, where verification becomes intractable as actuation frequency increases. It proposes a sound abstraction that replaces the NN controller with a set of locally valid linear models plus bounded uncertainty, enabling reachability analysis in continuous time and handling the limit $\delta \to 0$. The method is demonstrated on an image‑based NN controller for autonomous aircraft taxiing (AATS) using a cGAN perception surrogate, and its infinite‑frequency verification is compared to fixed‑frequency baselines, revealing a larger verifiable region under certain conditions. The results also expose current verification tool bottlenecks for closed‑loop, high‑frequency queries and highlight the need for benchmarks and further development to support continuous‑actuation analysis in practice.

Abstract

Neural network controllers are currently being proposed for use in many safety-critical tasks. Most analysis methods for neural network control systems assume a fixed control period. In control theory, higher frequency usually improves performance. However, for current analysis methods, increasing the frequency complicates verification. In the limit, when actuation is performed continuously, no existing neural network control systems verification methods are able to analyze the system. In this work, we develop the first verification method for continuously-actuated neural network control systems. We accomplish this by adding a level of abstraction to model the neural network controller. The abstraction is a piecewise linear model with added noise to account for local linearization error. The soundness of the abstraction can be checked using open-loop neural network verification tools, although we demonstrate bottlenecks in existing tools when handling the required specifications. We demonstrate the approach's efficacy by applying it to a vision-based autonomous airplane taxiing system and compare with a fixed frequency analysis baseline.

Figures (7)

• Figure 1: Autonomous Aircraft Taxiing System closed-loop diagram. In this work, we verify the performance of the infinite frequency version of this system, whereas prior work assumed a fixed frequency (1Hz).
• Figure 2: The nominal model assumes an ideal, predictable system, whereas the real model includes disturbances from the environment. Conformant synthesis uses the nominal model and adds disturbances to tackle the real model's uncertainties.
• Figure 3: Abstraction region for one cell and fitted linear models on all cells.
• Figure 4: Example image of the runway taken from an aircraft wing-mounted camera (left) and its corresponding downsampled image (right). Images from katz2021verifiGAN.
• Figure 5: Convergence of reachable sets over time. Comparison of the prior fixed frequency method and our modified approach at fixed 1Hz frequency setting using same initial states. Although the results are qualitatively similar, small differences are apparent due to the way physics are handled (the prior work uses a 20Hz time discretization), as well as how NN output bounds are obtained.