Interval Reachability of Nonlinear Dynamical Systems with Neural Network Controllers

Saber Jafarpour, Akash Harapanahalli, Samuel Coogan
Proceedings of The 5th Annual Learning for Dynamics and Control Conference, PMLR 211:12-25, 2023.

Abstract

This paper proposes a computationally efficient framework, based on interval analysis, for rigorous verification of nonlinear continuous-time dynamical systems with neural network controllers. Given a neural network, we use an existing verification algorithm to construct inclusion functions for its input-output behavior. Inspired by mixed monotone theory, we embed the closed-loop dynamics into a larger system using an inclusion function of the neural network and a decomposition function of the open-loop system. This embedding provides a scalable approach for safety analysis of the neural control loop while preserving the nonlinear structure of the system. We show that one can efficiently compute hyper-rectangular over-approximations of the reachable sets using a single trajectory of the embedding system. We design an algorithm to leverage this computational advantage through partitioning strategies, improving our reachable set estimates while balancing its runtime with tunable parameters. We demonstrate the performance of this algorithm through two case studies. First, we demonstrate this method’s strength in complex nonlinear environments. Then, we show that our approach matches the performance of the state-of-the-art verification algorithm for linear discretized systems.

Cite this Paper

BibTeX
@InProceedings{pmlr-v211-jafarpour23a, title = {Interval Reachability of Nonlinear Dynamical Systems with Neural Network Controllers}, author = {Jafarpour, Saber and Harapanahalli, Akash and Coogan, Samuel}, booktitle = {Proceedings of The 5th Annual Learning for Dynamics and Control Conference}, pages = {12--25}, year = {2023}, editor = {Matni, Nikolai and Morari, Manfred and Pappas, George J.}, volume = {211}, series = {Proceedings of Machine Learning Research}, month = {15--16 Jun}, publisher = {PMLR}, pdf = {https://proceedings.mlr.press/v211/jafarpour23a/jafarpour23a.pdf}, url = {https://proceedings.mlr.press/v211/jafarpour23a.html}, abstract = {This paper proposes a computationally efficient framework, based on interval analysis, for rigorous verification of nonlinear continuous-time dynamical systems with neural network controllers. Given a neural network, we use an existing verification algorithm to construct inclusion functions for its input-output behavior. Inspired by mixed monotone theory, we embed the closed-loop dynamics into a larger system using an inclusion function of the neural network and a decomposition function of the open-loop system. This embedding provides a scalable approach for safety analysis of the neural control loop while preserving the nonlinear structure of the system. We show that one can efficiently compute hyper-rectangular over-approximations of the reachable sets using a single trajectory of the embedding system. We design an algorithm to leverage this computational advantage through partitioning strategies, improving our reachable set estimates while balancing its runtime with tunable parameters. We demonstrate the performance of this algorithm through two case studies. First, we demonstrate this method’s strength in complex nonlinear environments. Then, we show that our approach matches the performance of the state-of-the-art verification algorithm for linear discretized systems. } }
Endnote
%0 Conference Paper %T Interval Reachability of Nonlinear Dynamical Systems with Neural Network Controllers %A Saber Jafarpour %A Akash Harapanahalli %A Samuel Coogan %B Proceedings of The 5th Annual Learning for Dynamics and Control Conference %C Proceedings of Machine Learning Research %D 2023 %E Nikolai Matni %E Manfred Morari %E George J. Pappas %F pmlr-v211-jafarpour23a %I PMLR %P 12--25 %U https://proceedings.mlr.press/v211/jafarpour23a.html %V 211 %X This paper proposes a computationally efficient framework, based on interval analysis, for rigorous verification of nonlinear continuous-time dynamical systems with neural network controllers. Given a neural network, we use an existing verification algorithm to construct inclusion functions for its input-output behavior. Inspired by mixed monotone theory, we embed the closed-loop dynamics into a larger system using an inclusion function of the neural network and a decomposition function of the open-loop system. This embedding provides a scalable approach for safety analysis of the neural control loop while preserving the nonlinear structure of the system. We show that one can efficiently compute hyper-rectangular over-approximations of the reachable sets using a single trajectory of the embedding system. We design an algorithm to leverage this computational advantage through partitioning strategies, improving our reachable set estimates while balancing its runtime with tunable parameters. We demonstrate the performance of this algorithm through two case studies. First, we demonstrate this method’s strength in complex nonlinear environments. Then, we show that our approach matches the performance of the state-of-the-art verification algorithm for linear discretized systems.
APA
Jafarpour, S., Harapanahalli, A. & Coogan, S.. (2023). Interval Reachability of Nonlinear Dynamical Systems with Neural Network Controllers. Proceedings of The 5th Annual Learning for Dynamics and Control Conference, in Proceedings of Machine Learning Research 211:12-25 Available from https://proceedings.mlr.press/v211/jafarpour23a.html.

Related Material