# A Reachability Method for Verifying Dynamical Systems with Deep Neural Network Controllers

## TL;DR

This paper introduces a reachability-based verification method for neural network controllers in dynamical systems, ensuring safety over multiple steps by over-approximating reachable states using verification tools.

## Contribution

It combines reachability analysis with neural network verification to provide formal safety guarantees for neural network controllers in dynamical systems.

## Key findings

- Successfully verified neural network controllers for mountain car and aircraft collision avoidance.
- Provided formal guarantees that the system states remain within safe bounds.
- Demonstrated the method's effectiveness in complex, real-world scenarios.

## Abstract

Deep neural networks can be trained to be efficient and effective controllers for dynamical systems; however, the mechanics of deep neural networks are complex and difficult to guarantee. This work presents a general approach for providing guarantees for deep neural network controllers over multiple time steps using a combination of reachability methods and open source neural network verification tools. By bounding the system dynamics and neural network outputs, the set of reachable states can be over-approximated to provide a guarantee that the system will never reach states outside the set. The method is demonstrated on the mountain car problem as well as an aircraft collision avoidance problem. Results show that this approach can provide neural network guarantees given a bounded dynamic model.