Quantitative verification of learning-enabled systems using ProbStar reachability

DOI10.1016/J.NAHS.2025.101623MaRDI QIDQ6885129zbMATH OpenFDO

Authors Yuntao Li, Sung Woo Choi, Bardh Hoxha, Georgios E. Fainekos, Hoang-Dung Tran

Publication date 12 December 2025

Published in Nonlinear Analysis. Hybrid Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/J.NAHS.2025.101623

zbMATH Keywords

reachability analysiscyber-physical systemsquantitative verificationdeep neural networklearning-enabled CPS

Mathematics Subject Classification ID

Artificial neural networks and deep learning (68T07) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Specification and verification (program logics, model checking, etc.) (68Q60) Attainable sets, reachability (93B03) Application models in control theory (93C95)

Cites work

• Case study
• Computation of multivariate normal and t probabilities
• Formal verification of neural network controlled autonomous systems
• Generating probabilistic safety guarantees for neural network controllers
• Improved geometric path enumeration for verifying ReLU neural networks
• JuliaReach
• Numerical computation of multivariate normal probabilities using bivariate conditioning
• Numerical verification of affine systems with up to a billion dimensions
• Parsimonious, Simulation Based Verification of Linear Systems
• Probabilistic reach-avoid for Bayesian neural networks
• Quantitative Verification for Neural Networks using ProbStars
• Reachability analysis for neural feedback systems using regressive polynomial rule inference
• Reachability analysis of deep ReLU neural networks using facet-vertex incidence
• Reluplex: an efficient SMT solver for verifying deep neural networks
• Rigorous simulation-based analysis of linear hybrid systems
• Robustness verification of semantic segmentation neural networks using relaxed reachability
• Safety Verification and Robustness Analysis of Neural Networks via Quadratic Constraints and Semidefinite Programming
• Simulation-equivalent reachability of large linear systems with inputs
• Star-based reachability analysis of deep neural networks
• The normal law under linear restrictions: simulation and estimation via minimax tilting
• Verification of Recurrent Neural Networks with Star Reachability
• Verification of deep convolutional neural networks using ImageStars
• Verifying binarized neural networks by Angluin-style learning
• Verifying low-dimensional input neural networks via input quantization
• Verisig
• \textsf{BDD4BNN}: a BDD-based quantitative analysis framework for binarized neural networks

This page was built for publication: Quantitative verification of learning-enabled systems using ProbStar reachability

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6885129)