Reachability Analysis of Neural Network Control Systems

TY - GEN

T1 - Reachability Analysis of Neural Network Control Systems

AU - Zhang, Chi

AU - Ruan, Wenjie

AU - Xu, Peipei

N1 - © 2023, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved

PY - 2023/6/26

Y1 - 2023/6/26

N2 - Neural network controllers (NNCs) have shown great promise in autonomous and cyber-physical systems. Despite the various verification approaches for neural networks, the safety analysis of NNCs remains an open problem. Existing verification approaches for neural network control systems (NNCSs) either can only work on a limited type of activation functions, or result in non-trivial over-approximation errors with time evolving. This paper proposes a verification framework for NNCS based on Lipschitzian optimisation, called DeepNNC. We first prove the Lipschitz continuity of closed-loop NNCSs by unrolling and eliminating the loops. We then reveal the working principles of applying Lipschitzian optimisation on NNCS verification and illustrate it by verifying an adaptive cruise control model. Compared to state-of-the-art verification approaches, DeepNNC shows superior performance in terms of efficiency and accuracy over a wide range of NNCs. We also provide a case study to demonstrate the capability of DeepNNC to handle a real-world, practical, and complex system. Our tool DeepNNC is available at https://github.com/TrustAI/DeepNNC.

AB - Neural network controllers (NNCs) have shown great promise in autonomous and cyber-physical systems. Despite the various verification approaches for neural networks, the safety analysis of NNCs remains an open problem. Existing verification approaches for neural network control systems (NNCSs) either can only work on a limited type of activation functions, or result in non-trivial over-approximation errors with time evolving. This paper proposes a verification framework for NNCS based on Lipschitzian optimisation, called DeepNNC. We first prove the Lipschitz continuity of closed-loop NNCSs by unrolling and eliminating the loops. We then reveal the working principles of applying Lipschitzian optimisation on NNCS verification and illustrate it by verifying an adaptive cruise control model. Compared to state-of-the-art verification approaches, DeepNNC shows superior performance in terms of efficiency and accuracy over a wide range of NNCs. We also provide a case study to demonstrate the capability of DeepNNC to handle a real-world, practical, and complex system. Our tool DeepNNC is available at https://github.com/TrustAI/DeepNNC.

U2 - 10.1609/aaai.v37i12.26783

DO - 10.1609/aaai.v37i12.26783

M3 - Conference contribution

VL - 37

T3 - Proceedings of the AAAI Conference on Artificial Intelligence

BT - Proceedings of the AAAI Conference on Artificial Intelligence

PB - AAAI Press

T2 - 37th AAAI Conference on Artificial Intelligence

Y2 - 7 February 2023 through 14 February 2023

ER -