Verification of Neural Network Control Systems in Continuous Time

TL;DR

This paper introduces the first verification method for neural network control systems with continuous actuation, enabling safety analysis at higher control frequencies by abstracting neural controllers into a piecewise linear model.

Contribution

It develops a novel abstraction-based verification approach for continuous-time neural network control systems, addressing limitations of existing methods at high actuation frequencies.

Findings

Effective verification of continuous-time neural control systems demonstrated on autonomous airplane taxiing.

The abstraction approach enables analysis with existing neural network verification tools.

Comparison shows advantages over fixed frequency analysis baseline.

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.