The paper presents a barrier certificate based approach to verifying safety properties of closed-loop systems using neural networks as controllers. It deals with the verification problem in the infinite time horizon and exploits the approximated system of the original one to synthesize the candidate barrier certificates, where the behavior of a neural network controller is approximated by a polynomial with a bounded error. Satisfiability Modulo Theories solvers are then utilized to identify real barrier certificates from those candidates. As a barrier certificate can separate the over-approximation of the reachable set from the unsafe region, once it is constructed, the safety property gets proved. We show the advantage of our approach in barrier certificates synthesis by comparing it with the state-of-the-art work on a set of benchmarks.

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 agent-based simulation, emergent equilibrium describes the macroscopic steady states of agents' interactions. While the state of individual agents might be changing, the collective behavior pattern remains the same in macroscopic equilibrium states. Traditionally, these emergent equilibriums are calculated using Monte Carlo methods. However, these methods require thousands of repeated simulation runs, which are extremely time-consuming. In this paper, we propose a novel three-layer framework to efficiently compute emergent equilibriums. The framework consists of a macro-level pseudo-arclength equilibrium solver (PAES), a micro-level simulator (MLS) and a macro-micro bridge (MMB). It can adaptively explore parameter space and recursively compute equilibrium states using the predictor-corrector scheme. We apply the framework to the popular opinion dynamics and labour market models. The experimental results show that our framework outperformed Monte Carlo experiments in terms of computation efficiency while maintaining the accuracy.