IoT Thrust Seminar | Reachability Analysis of Neural Network Control Systems using Polynomial Approximation

Safety verification of Cyber-Physical Systems (CPSs) has been a significant research topic due to the increasing use of computer controllers in safety-critical systems such as medical devices and autonomous vehicles. However, verifying the safety of a CPS is often difficult due to its complex behavior. In this talk, we present a series of techniques to computing accurate reachable set overapproximations for Neural Network Control Systems (NNCSs) which are a typical model of learning-enabled CPSs. We point out that directly combining the existing range overapproximation methods for neural network outputs and CPS reachable sets cannot well handle the reachable sets of NNCSs. Therefore, our methods compute an accurate polynomial abstraction for the input-output relation of a neural network and integrate the result into a reachability analysis framework. The developed techniques are implemented in the tool POLAR whose performance is evaluated on various challenging benchmarks.