# Verification of Neural Network Control Systems in Continuous Time

arXiv: https://arxiv.org/abs/2406.00157 · HTML: https://mlsanity.com/paper/2406.00157/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 9 of its 39 references that are in the map.
- First posted on arXiv 31 May 2024.

## Builds on (most cited first, 9 of 9)

- [Explaining and Harnessing Adversarial Examples](https://mlsanity.com/paper/1412.6572/) (2014)
- [Conditional Generative Adversarial Nets](https://mlsanity.com/paper/1411.1784/) (2014)
- [Provable defenses against adversarial examples via the convex outer adversarial polytope](https://mlsanity.com/paper/1711.00851/) (2017)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers](https://mlsanity.com/paper/2011.13824/) (2020)
- [ReachNN: Reachability Analysis of Neural-Network Controlled Systems](https://mlsanity.com/paper/1906.10654/) (2019)
- [Evaluating Robustness of Neural Networks with Mixed Integer Programming](https://mlsanity.com/paper/1711.07356/) (2017)
- [Automatic Perturbation Analysis for Scalable Certified Robustness and Beyond](https://mlsanity.com/paper/2002.12920/) (2020)
- [Scalable Synthesis of Verified Controllers in Deep Reinforcement Learning](https://mlsanity.com/paper/2104.10219/) (2021)

## Built on by (most cited first, 2 of 2)

- [Scenario-based Compositional Verification of Autonomous Systems with Neural Perception](https://mlsanity.com/paper/2504.20942/) (2025)
- [Robust Verification of Controllers under State Uncertainty via Hamilton-Jacobi Reachability Analysis](https://mlsanity.com/paper/2511.14755/) (2025)

## Abstract (arXiv)

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.