IIn this paper we propose a convex programming based method to address a long-standing problem of innerapproximating backward reachable sets of state-constrained polynomial systems subject to time-varying uncertainties. The backward reachable set is a set of states, from which all trajectories starting will surely enter a target region at the end of a given time horizon without violating a set of state constraints in spite of the actions of uncertainties. It is equal to the zero sub-level set of the unique Lipschitz viscosity solution to a Hamilton-Jacobi partial differential equation (HJE). We show that inner-approximations of the backward reachable set can be formed by zero sub-level sets of its viscosity super-solutions. Consequently, we reduce the innerapproximation problem to a problem of synthesizing polynomial viscosity super-solutions to this HJE. Such a polynomial solution in our method is synthesized by solving a single semi-definite program. We also prove that polynomial solutions to the formulated semi-definite program exist and can produce a convergent sequence of inner-approximations to the interior of the backward reachable set in measure under appropriate assumptions. This is the main contribution of this work. Several illustrative examples demonstrate the merits of our approach.

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 novel semi-definite programming approach that solves reach-avoid problems over open (i.e., not bounded a priori) time horizons for dynamical systems modeled by polynomial stochastic differential equations. The reach-avoid problem in this paper is a probabilistic guarantee: we approximate from the inner a $p$ -reach-avoid set, i.e., the set of initial states guaranteeing with probability larger than $p$ that the system eventually enters a given target set while remaining inside a specified safe set till the target hit. Our approach begins with the construction of a bounded value function, whose strict $p$ super-level set is equal to the $p$ -reach-avoid set. This value function is then reduced to a twice continuously differentiable solution to a system of equations. The system of equations facilitates the construction of a semi-definite program using sum-of-squares decomposition for multivariate polynomials and thus the transformation of nonconvex reach-avoid problems into a convex optimization problem. We would like to point out that our approach can straightforwardly be specialized to address classical safety verification by, a.o., stochastic barrier certificate methods and reach-avoid analysis for ordinary differential equations. In addition, several examples are provided to demonstrate theoretical and algorithmic developments of the proposed method.

In this paper we propose novel sufficient conditions for verifying reach-avoid properties of continuous-time systems modelled by ordinary differential equations (ODEs). Given a system, an initial set, a safe set and a target set of states, we say that the reach-avoid property holds, if for all initial conditions in the initial set, any trajectory of the system starting at them will eventually, i.e. in unbounded yet finite time, enter the target set while remaining inside the safe set until that first target hit (that is, if the system starting from the initial set can reach the target set safely). Based on a discount value function, two sets of quantified constraints are derived for verifying the reach-avoid property via the computation of exponential/asymptotic guidance-barrier functions (they form a barrier escorting the system to the target set safely at an exponential or asymptotic rate). It is interesting to find that one set of constraints whose solution is termed exponential guidance-barrier functions is just a simplified version of the existing one derived from the moment based method, while the other one whose solution is termed asymptotic guidance-barrier functions is completely new. Furthermore, built upon this new set of constraints, we derive a set of more expressive constraints, which includes the aforementioned two sets of constraints as special instances, providing more chances for verifying the reach-avoid property successfully. Finally, several examples demonstrate the theoretical developments and performance of proposed sufficient conditions using semi-definite programming methods.