Abstract This paper presents StarV, a new tool for verifying deep neural networks (DNNs) and learning-enabled Cyber-Physical Systems (Le-CPS) using the well-known star reachability. Distinguished from existing star-based verification tools such as NNV and NNENUM and others, StarV not only offers qualitative verification techniques using Star and ImageStar reachability analysis but is also the first tool to propose using ProbStar reachability for quantitative verification of DNNs with piecewise linear activation functions and Le-CPS. Notably, it introduces a novel ProbStar Temporal Logic formalism and associated algorithms, enabling the quantitative verification of DNNs and Le-CPS’s temporal behaviors. Additionally, StarV presents a novel SparseImageStar set representation and associated reachability algorithm that allows users to verify deep convolutional neural networks and semantic segmentation networks with more memory efficiency. StarV is evaluated in comparison with state-of-the-art in many challenging benchmarks. The experiments show that StarV outperforms existing tools in many aspects, such as timing performance, scalability, and memory consumption.

This paper introduces a novel quantitative verification framework for analyzing the temporal behaviors of learning-enabled systems (LES). Our approach employs ProbStar Temporal Logic (ProbStarTL) to specify LES temporal behaviors alongside advanced reachability and verification algorithms. Unlike existing qualitative methods focusing primarily on reach-avoid properties, our framework enables quantitative analysis of temporal properties. ProbStarTL, distinct from Signal Temporal Logic, operates on sequences of timed probabilistic star reachable sets, known as ProbStar signals. It features a clear syntax and dual qualitative and quantitative semantics. Our framework includes depth-first search algorithms for generating ProbStar traces and novel verification algorithms that transform ProbStarTL specifications into a computable disjunctive normal form for analysis. Our verification algorithms allow for both exact and approximate analyses. The exact scheme guarantees sound and complete results with precise satisfaction probabilities, while the approximate scheme offers sound results with maximum and minimum satisfaction probabilities at a reduced computational cost. The new verification framework is implemented using StarV, and its effectiveness is demonstrated through case studies on a learning-based adaptive cruise control system and an advanced emergency braking system.

This article extends the star set reachability approach to verify the robustness of feed-forward neural networks (FNNs) with sigmoidal activation functions such as Sigmoid and TanH. The main drawbacks of the star set approach in Sigmoid/TanH FNN verification are scalability, feasibility, and optimality issues, in some cases due to the linear programming solver usage. We overcome this challenge by proposing a relaxed star (RStar) with symbolic intervals, which allows the usage of the back-substitution technique in DeepPoly to find bounds when overapproximating activation functions while maintaining the valuable features of a star set. RStar can overapproximate a sigmoidal activation function using four linear constraints (RStar4) or two linear constraints (RStar2), or only the output bounds (RStar0). We implement our RStar reachability algorithms in NNV and compare them to DeepPoly via robustness verification of image classification DNNs benchmarks. The experimental results show that the original star approach (i.e., no relaxation) is the least conservative of all methods yet the slowest. RStar4 is computationally much faster than the original star method and is the second least conservative approach. It certifies up to 40% more images against adversarial attacks than DeepPoly and on average 51 times faster than the star set. Last, RStar0 is the most conservative method, which could only verify two cases for the CIFAR10 small Sigmoid network, δ = 0.014. However, it is the fastest method that can verify neural networks up to 3,528 times faster than the star set and up to 46 times faster than DeepPoly in our evaluation.

The rising use of robots in construction aims to ease labor-intensive and hazardous tasks. Ensuring safety in human-robot collaboration at construction sites is crucial, necessitating robust safety protocols and smooth interaction. This work aims to develop an open-source framework for monitoring and verifying safety in construction scenarios involving humans and robots. Our proposed framework includes the co-design of two modules: runtime monitoring against Signal Temporal Logic (STL) requirements and real-time reachability analysis using ProbStar. The runtime monitoring module effectively detects, localizes, and predicts human movements within the robot’s operational field. By employing a Kalman filter, we accurately estimate the future paths of workers, which facilitates proactive monitoring of worker safety. This approach enables dynamic adjustments to the robot’s trajectory, guided by quantitatively calculating robustness values of STL specifications in real-time. Our approach leverages real-time data from an RGB-D camera to promptly identify any deviations from expected behavior, further enhancing safety measures. To address uncertainties in localization that make the monitoring results inconclusive for safety judgments, the verification module employs real-time probabilistic reachability analysis to evaluate the likelihood of collisions between robots and obstacles within the robot’s local view. We evaluate the proposed framework across various human-robot interaction scenarios at construction sites.

Abstract This manuscript presents the updated version of the Neural Network Verification (NNV) tool. NNV is a formal verification software tool for deep learning models and cyber-physical systems with neural network components. NNV was first introduced as a verification framework for feedforward and convolutional neural networks, as well as for neural network control systems. Since then, numerous works have made significant improvements in the verification of new deep learning models, as well as tackling some of the scalability issues that may arise when verifying complex models. In this new version of NNV, we introduce verification support for multiple deep learning models, including neural ordinary differential equations, semantic segmentation networks and recurrent neural networks, as well as a collection of reachability methods that aim to reduce the computation cost of reachability analysis of complex neural networks. We have also added direct support for standard input verification formats in the community such as VNNLIB (verification properties), and ONNX (neural networks) formats. We present a collection of experiments in which NNV verifies safety and robustness properties of feedforward, convolutional, semantic segmentation and recurrent neural networks, as well as neural ordinary differential equations and neural network control systems. Furthermore, we demonstrate the capabilities of NNV against a commercially available product in a collection of benchmarks from control systems, semantic segmentation, image classification, and time-series data.

The paper extends the recent star reachability method to verify the robustness of recurrent neural networks (RNNs) for use in safety-critical applications. RNNs are a popular machine learning method for various applications, but they are vulnerable to adversarial attacks, where slightly perturbing the input sequence can lead to an unexpected result. Recent notable techniques for verifying RNNs include unrolling, and invariant inference approaches. The first method has scaling issues since unrolling an RNN creates a large feedforward neural network. The second method, using invariant sets, has better scalability but can produce unknown results due to the accumulation of overapproximation errors over time. This paper introduces a complementary verification method for RNNs that is both sound and complete. A relaxation parameter can be used to convert the method into a fast overapproximation method that still provides soundness guarantees. The method is designed to be used with NNV, a tool for verifying deep neural networks and learning-enabled cyber-physical systems. Compared to state-of-the-art methods, the extended exact reachability method is 10 × faster, and the overapproximation method is 100 × to 5000 × faster.

Given a real function f(X,Y), a box region B and ε>0, we want to compute an ε-isotopic polygonal approximation to the curve C: f(X,Y)=0 within B. We focus on subdivision algorithms because of their adaptive complexity. Plantinga & Vegter (2004) gave a numerical subdivision algorithm that is exact when the curve C is non-singular. They used a computational model that relies only on function evaluation and interval arithmetic.

An open question in Exact Geometric Computation is whether there re transcendental computations that can be made "geometrically exact".Perhaps the simplest such problem in computational geometry is that of computing the shortest obstacle-avoiding path between two points p, q in the plane, where the obstacles re collection of n discs.This problem can be solved in O (n 2 log n)time in the Real RAM model, but nothing was known about its computability in the standard (Turing) model of computation. We first show the Turing-computability of this problem,provided the radii of the discs are rationally related. We make the usual assumption that the numerical input data are real algebraic numbers. By appealing to effective bounds from transcendental number theory, we further show single-exponential time upper bound when the input numbers are rational.Our result ppears to be the first example of non-algebraic combinatorial problem which is shown computable. It is also rare example of transcendental number theory yielding positive computational results.

Medial axis transform (MAT) is a basic tool for shape analysis. However, in spite of its usefulness, it has some drawbacks, one of which is its instability under the boundary perturbation. We show that, although medial axis transform is unstable with respect to standard measures such as the Hausdorff distance, it is stable in a measure called relative Hausdorff distance for some "smoothed out" injective domains. In fact, we obtain an upper bound of the relative Hausdorff distance of the MAT of an injective domain with respect to the MAT of an arbitrary domain which is in small Hausdorff distance from the original injective domain. One consequence of the above result is that, by approximating a given domain with injective domains, we can extract the most "essential part" of the MAT within the prescribed error bound in Hausdorff distance. This introduces a new pruning strategy with precise error estimation. We illustrate our results with an example.

In order to process video data efficiently, a video segmentation technique through scene change detection must be employed. Many of advanced video applications require manipulations of compressed video signals. So, the scene change detection process is achieved by analyzing the video directly in the compressed domain, thereby avoiding the overhead of decompressing video into individual frames in the pixel domain. In this paper, we propose a fast scene change detection algorithm using direct feature extraction from MPEG compressed videos, and evaluate this technique using sample video data. This process was made possible by a new mathematical formulation for deriving the edge information directly from the discrete cosine transform coefficients.

In order to process video data efficiently, a video segmentation technique through scene change detection must be required. This is a fundamental operation used in many digital video applications such as digital libraries, video on demand (VOD), etc. Many of these advanced video applications require manipulations of compressed video signals. So, the scene change detection process is achieved by analyzing the video directly in the compressed domain, thereby avoiding the overhead of decompressing video into individual frames in the pixel domain. In this paper, we propose a fast scene change detection algorithm using direct feature extraction from MPEG compressed videos, and evaluate this technique using sample video data, First, we derive binary edge maps from the AC coefficients in blocks which were discrete cosine transformed. Second, we measure edge orientation, strength and offset using correlation between the AC coefficients in the derived binary edge maps. Finally, we match two consecutive frames using these two features (edge orientation and strength). This process was made possible by a new mathematical formulation for deriving the edge information directly from the discrete cosine transform (DCT) coefficients. We have shown that the proposed algorithm is faster or more accurate than the previously known scene change detection algorithms.