# A Neurosymbolic Approach to the Verification of Temporal Logic Properties of Learning enabled Control Systems

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

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 30 of its 51 references that are in the map.
- First posted on arXiv 7 Mar 2023.

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

- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Deep Reinforcement Learning in a Handful of Trials using Probabilistic Dynamics Models](https://mlsanity.com/paper/1805.12114/) (2018)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Efficient and Accurate Estimation of Lipschitz Constants for Deep Neural Networks](https://mlsanity.com/paper/1906.04893/) (2019)
- [Safety Verification of Deep Neural Networks](https://mlsanity.com/paper/1610.06940/) (2016)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [Formal Security Analysis of Neural Networks using Symbolic Intervals](https://mlsanity.com/paper/1804.10829/) (2018)
- [Semidefinite relaxations for certifying robustness to adversarial examples](https://mlsanity.com/paper/1811.01057/) (2018)
- [Efficient Formal Safety Analysis of Neural Networks](https://mlsanity.com/paper/1809.08098/) (2018)
- [NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems](https://mlsanity.com/paper/2004.05519/) (2020)
- [An approach to reachability analysis for feed-forward ReLU neural networks](https://mlsanity.com/paper/1706.07351/) (2017)
- [Exactly Computing the Local Lipschitz Constant of ReLU Networks](https://mlsanity.com/paper/2003.01219/) (2020)
- [Gaussian Processes for Data-Efficient Learning in Robotics and Control](https://mlsanity.com/paper/1502.02860/) (2015)
- [Lipschitz constant estimation of Neural Networks via sparse polynomial optimization](https://mlsanity.com/paper/2004.08688/) (2020)
- [Verisig: verifying safety properties of hybrid systems with neural network controllers](https://mlsanity.com/paper/1811.01828/) (2018)
- [Output Reachable Set Estimation and Verification for Multi-Layer Neural Networks](https://mlsanity.com/paper/1708.03322/) (2017)
- [Formal Verification of Neural Network Controlled Autonomous Systems](https://mlsanity.com/paper/1810.13072/) (2018)
- [Optimization and Abstraction: A Synergistic Approach for Analyzing Neural Network Robustness](https://mlsanity.com/paper/1904.09959/) (2019)
- [POLAR: A Polynomial Arithmetic Framework for Verifying Neural-Network Controlled Systems](https://mlsanity.com/paper/2106.13867/) (2021)
- [Compositional Falsification of Cyber-Physical Systems with Machine Learning Components](https://mlsanity.com/paper/1703.00978/) (2017)
- [Output Range Analysis for Deep Neural Networks](https://mlsanity.com/paper/1709.09130/) (2017)
- [Simulation-based Adversarial Test Generation for Autonomous Vehicles with Machine Learning Components](https://mlsanity.com/paper/1804.06760/) (2018)
- [Analyzing Deep Neural Networks with Symbolic Propagation: Towards Higher Precision and Faster Verification](https://mlsanity.com/paper/1902.09866/) (2019)
- [ReachNN: Reachability Analysis of Neural-Network Controlled Systems](https://mlsanity.com/paper/1906.10654/) (2019)
- [Certifying Incremental Quadratic Constraints for Neural Networks via Convex Optimization](https://mlsanity.com/paper/2012.05981/) (2020)
- [Formal Verification of CNN-based Perception Systems](https://mlsanity.com/paper/1811.11373/) (2018)
- [Time Robustness in MTL and Expressivity in Hybrid System Falsification (Extended Version)](https://mlsanity.com/paper/1505.06307/) (2015)
- [Analytical bounds on the local Lipschitz constants of affine-ReLU functions](https://mlsanity.com/paper/2008.06141/) (2020)

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

- [RT-NeuS: Towards Real-Time Neuro-Symbolic Video Understanding via Adaptive Temporal Verification](https://mlsanity.com/paper/2602.23553/) (2026)
- [Formal Verification of Long Short-Term Memory based Audio Classifiers: A Star based Approach](https://mlsanity.com/paper/2311.12130/) (2023)
- [Scaling Learning based Policy Optimization for Temporal Logic Tasks by Controller Network Dropout](https://mlsanity.com/paper/2403.15826/) (2024)

## Abstract (arXiv)

Signal Temporal Logic (STL) has become a popular tool for expressing formal requirements of Cyber-Physical Systems (CPS). The problem of verifying STL properties of neural network-controlled CPS remains a largely unexplored problem. In this paper, we present a model for the verification of Neural Network (NN) controllers for general STL specifications using a custom neural architecture where we map an STL formula into a feed-forward neural network with ReLU activation. In the case where both our plant model and the controller are ReLU-activated neural networks, we reduce the STL verification problem to reachability in ReLU neural networks. We also propose a new approach for neural network controllers with general activation functions; this approach is a sound and complete verification approach based on computing the Lipschitz constant of the closed-loop control system. We demonstrate the practical efficacy of our techniques on a number of examples of learning-enabled control systems.