Safety verification is an essential requirement of neural network controlled systems when they are adopted in safety-critical fields. This paper proposes a novel approach to synthesizing neural networks as barrier certificates, which can provide safety guarantees for neural network controlled systems. We first propose the construction conditions of neural network barrier certificates, followed by an iterative framework to synthesize them. Each iteration trains a neural network as the candidate barrier certificate using the training datasets sampled from the neural network controlled system. After training, identifying whether the candidate barrier certificate is a real one for the neural network controlled system is transformed into a group of mixed-integer programming problems, which the numerical optimization solver solves with guaranteed results. We implement the tool NetBC and evaluate its performance over 6 practical benchmark examples. The experimental results show that NetBC is more effective and scalable than the existing polynomial barrier certificate-based method.

Barrier certificates provide safety guarantees for hybrid systems. In this paper, we propose a novel approach to synthesizing neural networks as barrier certificates. Candidate networks are trained from a special structure: ReLU neural networks consisting of two hidden layers. Then, the problem of identifying real barrier certificates from candidates is transformed into a group of mixed integer linear programming problems and a mixed integer quadratically constrained problem. Taking full advantage of the recent advance in optimization, barrier certificates validation can be performed effectively. We implement the tool SyntheBC and evaluate its performance over 3 hybrid systems and 8 continuous systems up to 12-dimensional state space. The experimental results show that our method is more scalable and effective than the classical polynomial barrier certificate method and the existing neural network based method.

In safety verification of hybrid systems, barrier certificates are generated by solving the verification conditions derived from non-negative representations of different types. This paper presents a new computational method, sequential linear programming projection, for directly solving the set of verification conditions represented by the Krivine-Vasilescu-Handelman's positivstellensatz. The key idea is to decompose it into two successive optimization problems that refine the desired barrier certificate and those undetermined multipliers, respectively, and solve it in an iterative scheme. The most important benefit of the proposed approach lies in that it is much more effective than the LP relaxation method in producing real barrier certificates, and possesses a much lower computational complexity than the popular sum of square relaxation methods, which is demonstrated by the theoretical analysis on complexity and the experiment on a set of examples gathered from the literature.

Multi-robot navigation control in the absence of reference trajectory is rather challenging as it is expected to ensure stability and feasibility while still offer fast computation on control decisions. The intrinsic high complexity of switched linear dynamical robots makes the problem even more challenging. In this paper, we propose a novel HMPC based method to address the navigation problem of multiple robots with switched linear dynamics. We develop a new technique to compute the reachable sets of switched linear systems and use them to enable the parallel computation of control parameters. We present theoretical results on stability, feasibility and complexity of the proposed approach, and demonstrate its empirical advance in performance against other approaches.