mlsanityData to 14 Oct 2026

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

arXiv 2303.05394 ↗First posted 7 Mar 2023eess.SY cs.LG cs.ROcited by 3

Not on the map. Why?

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.

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

30 of 51 references.

References · 30

  1. 2013Intriguing properties of neural networkscited by 5,155
  2. 2018Deep Reinforcement Learning in a Handful of Trials using Probabilistic Dynamics Modelscited by 774
  3. 2017Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networkscited by 744
  4. 2018Efficient Neural Network Robustness Certification with General Activation Functionscited by 445
  5. 2019Efficient and Accurate Estimation of Lipschitz Constants for Deep Neural Networkscited by 293
  6. 2016Safety Verification of Deep Neural Networkscited by 263
  7. 2017Formal Verification of Piece-Wise Linear Feed-Forward Neural Networkscited by 242
  8. 2019Algorithms for Verifying Deep Neural Networkscited by 221
  9. 2018Formal Security Analysis of Neural Networks using Symbolic Intervalscited by 185
  10. 2018Semidefinite relaxations for certifying robustness to adversarial examplescited by 179
  11. 2018Efficient Formal Safety Analysis of Neural Networkscited by 165
  12. 2020NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systemscited by 128
18 more
  1. 2017An approach to reachability analysis for feed-forward ReLU neural networkscited by 127
  2. 2020Exactly Computing the Local Lipschitz Constant of ReLU Networkscited by 102
  3. 2015Gaussian Processes for Data-Efficient Learning in Robotics and Controlcited by 98
  4. 2020Lipschitz constant estimation of Neural Networks via sparse polynomial optimizationcited by 87
  5. 2018Verisig: verifying safety properties of hybrid systems with neural network controllerscited by 84
  6. 2017Output Reachable Set Estimation and Verification for Multi-Layer Neural Networkscited by 80
  7. 2018Formal Verification of Neural Network Controlled Autonomous Systemscited by 41
  8. 2019Optimization and Abstraction: A Synergistic Approach for Analyzing Neural Network Robustnesscited by 40
  9. 2021POLAR: A Polynomial Arithmetic Framework for Verifying Neural-Network Controlled Systemscited by 39
  10. 2017Compositional Falsification of Cyber-Physical Systems with Machine Learning Componentscited by 32
  11. 2017Output Range Analysis for Deep Neural Networkscited by 30
  12. 2018Simulation-based Adversarial Test Generation for Autonomous Vehicles with Machine Learning Componentscited by 29
  13. 2019Analyzing Deep Neural Networks with Symbolic Propagation: Towards Higher Precision and Faster Verificationcited by 28
  14. 2019ReachNN: Reachability Analysis of Neural-Network Controlled Systemscited by 26
  15. 2020Certifying Incremental Quadratic Constraints for Neural Networks via Convex Optimizationcited by 18
  16. 2018Formal Verification of CNN-based Perception Systemscited by 13
  17. 2015Time Robustness in MTL and Expressivity in Hybrid System Falsification (Extended Version)cited by 8
  18. 2020Analytical bounds on the local Lipschitz constants of affine-ReLU functionscited by 2

Built on by

Cited by year (2026 to 14 Oct)

Citing papers per year: 2023: 1; 2024: 1; 2025: 0; 2026: 1.

3 papers.

  1. 2026RT-NeuS: Towards Real-Time Neuro-Symbolic Video Understanding via Adaptive Temporal Verificationcited by 2
  2. 2023Formal Verification of Long Short-Term Memory based Audio Classifiers: A Star based Approachcited by 0
  3. 2024Scaling Learning based Policy Optimization for Temporal Logic Tasks by Controller Network Dropoutcited by 0