Barrier certificates play an important role in verifying the safety of continuous-time systems, including autonomous driving, robotic manipulators and other critical applications. Recently, ReLU neural barrier certificates---barrier certificates represented by the ReLU neural networks---have attracted significant attention in the safe control community due to their promising performance. However, because of the approximate nature of neural networks, rigorous verification methods are required to ensure the correctness of these certificates. This paper presents a necessary and sufficient condition for verifying the correctness of ReLU neural barrier certificates. The proposed condition can be encoded as either an Satisfiability Modulo Theories (SMT) or optimization problem, enabling both verification and falsification. To the best of our knowledge, this is the first approach capable of falsifying ReLU neural barrier certificates. Numerical experiments demonstrate the validity and effectiveness of the proposed method in both verifying and falsifying such certificates.

We present PyBDR, a Python toolkit for reachability analysis based on set-boundary techniques, which centralizes on widely-adopted set propagation techniques for formal verification, controller synthesis, and state estimation. By analyzing the boundaries of initial sets, PyBDR mitigates the wrapping effect in computations, thereby enhancing the efficiency of reachability algorithms without incurring substantial computational overhead. Its modular architecture provides a collection of building blocks that streamline the prototyping of new reachability analysis methods. Illustrative examples highlight PyBDR’s key features and demonstrate its advantages in computing reachable sets for large initial conditions and long time horizons.

Recently, formal verification of deep neural networks (DNNs) has garnered considerable attention, and over-approximation based methods have become popular due to their effectiveness and efficiency. However, these strategies face challenges in addressing the "unknown dilemma" concerning whether the exact output region or the introduced approximation error violates the property in question. To address this, this paper introduces theUR4NNVverification framework, which utilizes under-approximation reachability analysis for DNN verification for the first timeUR4NNV focuses on DNNs with Rectified Linear Unit (ReLU) activations and employs a binary tree branch-based under-approximation algorithm. In each epoch, UR4NNVunder-approximates a sub-polytope of the reachable set and verifies this polytope against the given property. Through a trial-and-error approach,UR4NNVeffectively falsifies DNN properties while providing confidence levels when reaching verification epoch bounds and failing falsifying properties. Experimental comparisons with existing verification methods demonstrate the effectiveness and efficiency ofUR4NNVsignificantly reducing the impact of the "unknown dilemma".

Train platoons are a really innovative application for future railways, in which trains are virtually-coupled via Train-Train communication, so drastically reducing their headways and increasing line capacity. However, as the spacing between trains becomes closer, the influence of disturbances from preceding trains becomes more significant and cannot be ignored. This influence can have a substantial impact on the operational behavior of the following trains, leading to fluctuating spacing within the platoon and potentially compromising the safety and stability of the train spacing. This paper introduces a formalized modeling framework and a controller synthesis method for train platoons, aiming to achieve absolute safety and stable operation in train platoon operations. The framework utilizes Hybrid Priced Two-player Timed Game Automaton (HPTTGA) to describe train platoon dynamics and synthesizes controllers that satisfy safety requirements using an On-the-fly Controller Synthesis (OCS) algorithm, where the effectiveness of the algorithm is demonstrated through a two-train tracking example, and Q-learning is applied to select controller which satisfy local and string stability. Owing to model-based feature, the proposed method is compared to classical Model Predictive Control (MPC) in terms of safety, local stability, and string stability. Experimental results demonstrate that the proposed method consistently ensures train platoon safety and achieves similar control performance to MPC in extreme operating scenarios. Moreover, under velocity limit scenarios, the proposed method successfully achieves the desired following behavior of the trailing train according to the control objectives.

Constraint-solving-based program invariant synthesis takes a parametric invariant template and encodes the (inductive) invariant conditions into constraints. The problem of characterizing the set of all valid parameter assignments is referred to as the strong invariant synthesis problem , while the problem of finding a concrete valid parameter assignment is called the weak invariant synthesis problem . For both problems, the challenge lies in solving or reducing the encoded constraints, which are generally non-convex and lack efficient solvers. In this article, we propose two novel algorithms for synthesizing invariants of polynomial programs using semidefinite programming (SDP): (1) The Cluster algorithm targets the strong invariant synthesis problem for polynomial invariant templates. Leveraging robust optimization techniques, it solves a series of SDP relaxations and yields a sequence of increasingly precise under-approximations of the set of valid parameter assignments. We prove the algorithm’s soundness, convergence, and weak completeness under a specific robustness assumption on templates. Moreover, the outputs can simplify the weak invariant synthesis problem. (2) The Mask algorithm addresses the weak invariant synthesis problem in scenarios where the aforementioned robustness assumption does not hold, rendering the Cluster algorithm ineffective. It identifies a specific subclass of invariant templates, termed masked templates, involving parameterized polynomial equalities and known inequalities. By applying variable substitution, the algorithm transforms constraints into an equivalent form amenable to SDP relaxations. Both algorithms have been implemented and demonstrated superior performance compared to state-of-the-art methods in our empirical evaluation.

Abstract Inner-approximate reachability analysis involves calculating subsets of reachable sets, known as inner-approximations. This analysis is crucial in the fields of dynamic systems analysis and control theory as it provides a reliable estimation of the set of states that a system can reach from given initial states at a specific time instant. In this paper, we study the inner-approximate reachability analysis problem based on the set-boundary reachability method for systems modelled by ordinary differential equations, in which the computed inner-approximations are represented with zonotopes. The set-boundary reachability method computes an inner-approximation by excluding states reached from the initial set’s boundary. The effectiveness of this method is highly dependent on the efficient extraction of the exact boundary of the initial set. To address this, we propose methods leveraging boundary and tiling matrices that can efficiently extract and refine the exact boundary of the initial set represented by zonotopes. Additionally, we enhance the exclusion strategy by contracting the outer-approximations in a flexible way, which allows for the computation of less conservative inner-approximations. To evaluate the proposed method, we compare it with state-of-the-art methods against a series of benchmarks. The numerical results demonstrate that our method is not only efficient but also accurate in computing inner-approximations.

Abstract We present PyBDR, a Python reachability analysis toolkit based on set-boundary analysis, which centralizes on widely-adopted set propagation techniques for formal verification, controller synthesis, state estimation, etc. It employs boundary analysis of initial sets to mitigate the wrapping effect during computations, thus improving the performance of reachability analysis algorithms without significantly increasing computational costs. Beyond offering various set representations such as polytopes and zonotopes, our toolkit particularly excels in interval arithmetic by extending operations to the tensor level, enabling efficient parallel interval arithmetic computation and unifying vector and matrix intervals into a single framework. Furthermore, it features symbolic computation of derivatives of arbitrary order and evaluates them as real or interval-valued functions, which is essential for approximating behaviours of nonlinear systems at specific time instants. Its modular architecture design offers a series of building blocks that facilitate the prototype development of reachability analysis algorithms. Comparative studies showcase its strengths in handling verification tasks with large initial sets or long time horizons. The toolkit is available at https://github.com/ASAG-ISCAS/PyBDR .

Recently, the interpretability and verification of deep learning have attracted enormous attention from both academic and industrial communities, aiming to gain users’ trust and ease their concerns. To guide learning procedures or data operations carried out in a more interpretable way, in this paper, we put a similar perspective on image datasets, the inputs of deep learning. Based on manifold learning, we work out an interpretable geometrical characterization on the curvity of manifolds to depict the feature density of datasets, which is represented with the ratio of the Euclidean distance and the geodesic distance. It is a noteworthy characteristic of image datasets and we take the dataset compression and enhancement problems as application instances via sample credit assignment with the geometrical information. Experiments on typical image datasets have justified the effectiveness and enormous prospect of the presented geometrical characteristic.

In this paper we investigate the optimal controller synthesis problem, so that the system under the controller can reach a specified target set while satisfying given constraints. Existing model predictive control (MPC) methods learn from a set of discrete states visited by previous (sub-)optimized trajectories and thus result in computationally expensive mixed-integer nonlinear optimization. In this paper a novel MPC method is proposed based on reach-avoid analysis to solve the controller synthesis problem iteratively. The reach-avoid analysis is concerned with computing a reach-avoid set which is a set of initial states such that the system can reach the target set successfully. It not only provides terminal constraints, which ensure feasibility of MPC, but also expands discrete states in existing methods into a continuous set (i.e., reach-avoid sets) and thus leads to nonlinear optimization which is more computationally tractable online due to the absence of integer variables. Finally, we evaluate the proposed method and make comparisons with state-of-the-art ones based on several examples.

Robustness of deep neural networks (DNNs) has caused great concerns in the academic and industrial communities, especially in safety-critical domains. Instead of verifying whether the robustness property holds or not in certain neural networks, this paper focuses on training robust neural networks with respect to given perturbations. State-of-the-art training methods, interval bound propagation (IBP) and CROWN-IBP, perform well with respect to small perturbations, but their performance declines significantly in large perturbation cases, which is termed “drawdown risk” in this paper. Specifically, drawdown risk refers to the phenomenon that IBP-family training methods cannot provide expected robust neural networks in larger perturbation cases, as in smaller perturbation cases. To alleviate the unexpected drawdown risk, we propose a global and monotonically decreasing robustness training strategy that takes multiple perturbations into account during each training epoch (global robustness training), and the corresponding robustness losses are combined with monotonically decreasing weights (monotonically decreasing robustness training). With experimental demonstrations, our presented strategy maintains performance on small perturbations and the drawdown risk on large perturbations is alleviated to a great extent. It is also noteworthy that our training method achieves higher model accuracy than the original training methods, which means that our presented training strategy gives more balanced consideration to robustness and accuracy.

To analyse local robustness properties of deep neural networks (DNNs), we present a practical framework from a model learning perspective. Based on black-box model learning with scenario optimisation, we abstract the local behaviour of a DNN via an affine model with the probably approximately correct (PAC) guarantee. From the learned model, we can infer the corresponding PAC-model robustness property. The innovation of our work is the integration of model learning into PAC robustness analysis: that is, we construct a PAC guarantee on the model level instead of sample distribution, which induces a more faithful and accurate robustness evaluation. This is in contrast to existing statistical methods without model learning. We implement our method in a prototypical tool named DeepPAC. As a black-box method, DeepPAC is scalable and efficient, especially when DNNs have complex structures or high-dimensional inputs. We extensively evaluate DeepPAC, with 4 baselines (using formal verification, statistical methods, testing and adversarial attack) and 20 DNN models across 3 datasets, including MNIST, CIFAR-10, and ImageNet. It is shown that DeepPAC outperforms the state-of-the-art statistical method PROVERO, and it achieves more practical robustness analysis than the formal verification tool ERAN. Also, its results are consistent with existing DNN testing work like DeepGini.

Abstract A barrier certificate often serves as an inductive invariant that isolates an unsafe region from the reachable set of states, and hence is widely used in proving safety of hybrid systems possibly over the infinite time horizon. We present a novel condition on barrier certificates, termed theinvariant barrier-certificate condition, that witnesses unbounded-time safety of differential dynamical systems. The proposed condition is by far the least conservative one on barrier certificates, and can be shown as the weakest possible one to attain inductive invariance. We show that discharging the invariant barrier-certificate condition—thereby synthesizing invariant barrier certificates—can be encoded as solving anoptimization problem subject to bilinear matrix inequalities(BMIs). We further propose a synthesis algorithm based on difference-of-convex programming, which approaches a local optimum of the BMI problem via solvinga series of convex optimization problems. This algorithm is incorporated in a branch-and-bound framework that searches for the global optimum in a divide-and-conquer fashion. We present a weak completeness result of our method, in the sense that a barrier certificate is guaranteed to be found (under some mild assumptions) whenever there exists an inductive invariant (in the form of a given template) that suffices to certify safety of the system. Experimental results on benchmark examples demonstrate the effectiveness and efficiency of our approach.

Delays are ubiquitous in modern hybrid systems, which exhibit both continuous and discrete dynamical behaviors. Induced by signal transmission, conversion, the nature of plants, and so on, delays may appear either in the continuous evolution of a hybrid system such that the evolution depends not only on the present state but also on its execution history, or in the discrete switching between its different control modes. In this paper we come up with a new model of hybrid systems, called delay hybrid automata, to capture the dynamics of systems with the aforementioned two kinds of delays. Furthermore, based upon this model we study the robust switching controller synthesis problem such that the controlled delay system is able to satisfy the specified safety properties regardless of perturbations. To the end, a novel method is proposed to synthesize switching controllers based on the computation of differential invariants for continuous evolution and backward reachable sets of discrete jumps with delays. Finally, we implement a prototypical tool of our approach and demonstrate it on some case studies.

We give an introduction to the MARS toolchain for formal modeling and verification of hybrid systems. It consists of translators from Simulink/Stateflow models to Hybrid Communicating Sequential Processes (HCSP), and tools for simulation, code generation, and deductive verification of an HCSP model. We apply the toolchain to model the descent guidance control phase of the recently launched Tianwen I mars lander, and verify that it correctly controls the velocity of the lander.

Abstract We propose a spurious region guided refinement approach for robustness verification of deep neural networks. Our method starts with applying the DeepPoly abstract domain to analyze the network. If the robustness property cannot be verified, the result is inconclusive. Due to the over-approximation, the computed region in the abstraction may be spurious in the sense that it does not contain any true counterexample. Our goal is to identify such spurious regions and use them to guide the abstraction refinement. The core idea is to make use of the obtained constraints of the abstraction to infer new bounds for the neurons. This is achieved by linear programming techniques. With the new bounds, we iteratively apply DeepPoly, aiming to eliminate spurious regions. We have implemented our approach in a prototypical tool DeepSRGR. Experimental results show that a large amount of regions can be identified as spurious, and as a result, the precision of DeepPoly can be significantly improved. As a side contribution, we show that our approach can be applied to verify quantitative robustness properties.

This article investigates the consensus tracking problem of the heterogeneous multivehicle systems (MVSs) under a repeatable control environment. First, a unified iterative learning control (ILC) algorithm is presented for all autonomous vehicles, each of which is governed by both discrete- and continuous-time nonlinear dynamics. Then, several consensus criteria for MVSs with switching topology and external disturbances are established based on our proposed distributed ILC protocols. For discrete-time systems, all vehicles can perfectly track to the common reference trajectory over a specified finite time interval, and the corresponding digraphs may not have spanning trees. Existing approaches dealing with the continuous-time systems generally require that all vehicles have strictly identical initial conditions, being too ideal in practice. We relax this unpractical assumption and propose an extra distributed initial state learning protocol such that vehicles can take different initial states, leading to the fact that the finite time tracking is achieved ultimately regardless of the initial errors. Finally, a numerical example demonstrates the effectiveness of our theoretical results.

In this paper, we propose a method for bounding the probability that a stochastic differential equation (SDE) system violates a safety specification over the infinite time horizon. SDEs are mathematical models of stochastic processes that capture how states evolve continuously in time. They are widely used in numerous applications such as engineered systems (e.g., modeling how pedestrians move in an intersection), computational finance (e.g., modeling stock option prices), and ecological processes (e.g., population change over time). Previously the safety verification problem has been tackled over finite and infinite time horizons using a diverse set of approaches. The approach in this paper attempts to connect the two views by first identifying a finite time bound, beyond which the probability of a safety violation can be bounded by a negligibly small number. This is achieved by discovering an exponential barrier certificate that proves exponentially converging bounds on the probability of safety violations over time. Once the finite time interval is found, a finite-time verification approach is used to bound the probability of violation over this interval. We demonstrate our approach over a collection of interesting examples from the literature, wherein our approach can be used to find tight bounds on the violation probability of safety properties over the infinite time horizon.

Craig interpolant generation for non-linear theory and its combination with other theories are still in infancy, although interpolation-based techniques have become popular in the verification of programs and hybrid systems where non-linear expressions are very common. In this paper, we first prove that a polynomial interpolant of the form $$h(\mathbf {x})>0$$ exists for two mutually contradictory polynomial formulas $$\phi (\mathbf {x},\mathbf {y})$$ and $$\psi (\mathbf {x},\mathbf {z})$$ , with the form $$f_1\ge 0\wedge \cdots \wedge f_n\ge 0$$ , where $$f_i$$ are polynomials in $$\mathbf {x},\mathbf {y}$$ or $$\mathbf {x},\mathbf {z}$$ , and the quadratic module generated by $$f_i$$ is Archimedean. Then, we show that synthesizing such interpolant can be reduced to solving a semi-definite programming problem ( $$\mathrm{SDP}$$ ). In addition, we propose a verification approach to assure the validity of the synthesized interpolant and consequently avoid the unsoundness caused by numerical error in $$\mathrm{SDP}$$ solving. Besides, we discuss how to generalize our approach to general semi-algebraic formulas. Finally, as an application, we demonstrate how to apply our approach to invariant generation in program verification.

Deep neural networks (DNNs) have been applied in safety-critical domains such as self driving cars, aircraft collision avoidance systems, malware detection, etc. In such scenarios, it is important to give a safety guarantee to the robustness property, namely that outputs are invariant under small perturbations on the inputs. For this purpose, several algorithms and tools have been developed recently. In this paper, we present PRODeep, a platform for robustness verification of DNNs. PRODeep incorporates constraint-based, abstraction-based, and optimisation-based robustness checking algorithms. It has a modular architecture, enabling easy comparison of different algorithms. With experimental results, we illustrate the use of the tool, and easy combination of those techniques.

Random ordinary differential equations (RODEs) are ordinary differential equations (ODEs) that contain a stochastic process in their vector field functions. They have been used for many years in a wide range of applications, but have been a shadow existence to stochastic differential equations (SDEs) despite being able to model a wider and often physically more adequate range of disturbances. In this article, we study the safety verification problem over both finite time horizons and the infinite time horizon for RODEs incorporating Wiener processes. Concretely, we investigate the p-safety problem, where we identify the set of initial states from which the probability to satisfy safety specifications is at least p. Based on identifying a set of sample paths whose probability measure is larger than p, we propose a method of reducing stochastic reachability to adversary reachability of ODEs for solving the p-safety problem over finite time horizons. This method permits an efficient lifting of reach-set computation methods for perturbed ODEs to RODEs. In this method, the p-safety problem over finite time horizons is reduced to the problem of inner-approximating robust backward reachable sets for ODEs with time-varying perturbation inputs. We then extend the method to the p-safety problem over the infinite time horizon. Finally, we demonstrate our method on several examples.

In this article, we present a novel model checking approach to finite-time safety verification of black-box continuous-time dynamical systems within the framework of probably approximately correct (PAC) learning. The black-box dynamical systems are the ones, for which no model is given but whose states changing continuously through time within a finite-time interval can be observed at some discrete-time instants for a given input. The new model checking approach is termed as the PAC model checking due to the incorporation of learned models with correctness guarantees expressed using the terms error probability and confidence. Based on the error probability and confidence level, our approach provides statistically formal guarantees that the time-evolving trajectories of the black-box dynamical system over finite-time horizons fall within the range of the learned model plus a bounded interval, contributing to insights on the reachability of the black-box system and thus on the satisfiability of its safety requirements. The learned model together with the bounded interval is obtained by scenario optimization, which boils down to a linear programming problem. Three examples demonstrate the performance of our approach.

Delayed coupling between state variables occurs regularly in technical dynamical systems, especially embedded control. As it consequently is omnipresent in safety-critical domains, there is an increasing interest in the safety verification of systems modelled by Delay Differential Equations (DDEs). In this paper, we leverage qualitative guarantees for the existence of an exponentially decreasing estimation on the solutions to DDEs as established in classical stability theory, and present a quantitative method for constructing such delay-dependent estimations, thereby facilitating a reduction of the verification problem over an unbounded temporal horizon to a bounded one. Our technique builds on the linearization technique of nonlinear dynamics and spectral analysis of the linearized counterparts. We show experimentally on a set of representative benchmarks from the literature that our technique indeed extends the scope of bounded verification techniques to unbounded verification tasks. Moreover, our technique is easy to implement and can be combined with any automatic tool dedicated to bounded verification of DDEs.

In this paper we study the problem of computing robust invariant sets for state-constrained perturbed polynomial systems within the Hamilton-Jacobi reachability framework. A robust invariant set is a set of states such that every possible trajectory starting from it never violates the given state constraint, irrespective of the actual perturbation. The main contribution of this work is to describe the maximal robust invariant set as the zero level set of the unique Lipschitz-continuous viscosity solution to a Hamilton-Jacobi-Bellman (HJB) equation. The continuity and uniqueness property of the viscosity solution facilitates the use of existing numerical methods to solve the HJB equation for an appropriate number of state variables in order to obtain an approximation of the maximal robust invariant set. We furthermore propose a method based on semi-definite programming to synthesize robust invariant sets. Some illustrative examples demonstrate the performance of our methods.

In this paper we suggest a method based on convex programming for computing semi-algebraic under-approximations of reach sets for polynomial continuous systems with initial sets being the zero sub-level set of a polynomial function. It is well-known that the reachable set can be formulated as the zero sub-level set of a value function to a Hamilton-Jacobi partial differential equation (HJE), and our approach in this paper consequently focuses on searching for approximate analytical polynomial solutions to associated HJEs, of which the zero sub-level sets converge to the exact reachable set from inside in measure, without discretizing the state space. Such approximate solutions can be computed via a classical hierarchy of convex programs consisting of linear matrix inequalities, which are constructed by sum-of-squares decomposition techniques. In contrast to traditional numerical methods approximately solving HJEs, such as level-set methods, our method reduces HJE solving to convex optimization, avoiding the complexity associated to gridding the state space. Compared to existing approaches computing under-approximations, the approach described in this paper is structurally simpler as the under-approximations are the outcome of a single semi-definite program. Furthermore, an over-approximation of the reach set, shedding light on the quality of the constructed under-approximation, can be constructed via solving the same semi-definite program. Several illustrative examples and comparisons with existing methods demonstrate the merits of our approach.

In this paper we propose a mechanisable approach for discovering multiple Lyapunov functions for switched hybrid systems. We start with the classical definition on asymptotic stability, which can be assured by the existence of multiple Lyapunov functions. Then, we derive an algebraizable sufficient condition on multiple Lyapunov functions in quadratic form for asymptotic stability analysis. Since different modes are considered, in addition to real root classification, we further apply a projection operator step by step to under-approximate this sufficient condition and obtain a set of semi-algebraic sets which only involve the coefficients of the multiple Lyapunov function. Moreover, for each step, we use the information on modes to optimize our intermediate computation results. Finally, we compute a sample point in the resulting semi-algebraic sets for coefficients. We tested our approach on five examples using prototypical implementation. The computation and comparison results demonstrate the applicability and efficiency of our approach.

In this paper we propose a mechanisable technique for asymptotic stability analysis of continuous dynamical systems. We start from linearizing a continuous dynamical system, solving the Lyapunov matrix equation and then check whether the solution is positive definite. For the cases that the Jacobian matrix is not a Hurwitz matrix, we first derive an algebraizable sufficient condition for the existence of a Lyapunov function in quadratic form without linearization. Then, we apply a real root classification based method step by step to formulate this derived condition as a semi-algebraic set such that the semi-algebraic set only involves the coefficients of the pre-assumed quadratic form. Finally, we compute a sample point in the resulting semi-algebraic set for the coefficients resulting in a Lyapunov function. In this way, we avoid the use of generic quantifier elimination techniques for efficient computation. We prototypically implemented our algorithm based on DISCOVERER. The experimental results and comparisons demonstrate the feasibility and promise of our approach.