This paper presents a novel approach to safety verification based on neural barrier certificates synthesis for continuous dynamical systems. We construct the synthesis framework as an inductive loop between a Learner and a Verifier based on barrier certificate learning and counterexample guidance. Compared with the counterexample-guided verification method based on the SMT solver, we design and learn neural barrier functions with special structure, and use the special form to convert the counterexample generation into a polynomial optimization problem for obtaining the optimal counterexample. In the verification phase, the task of identifying the real barrier certificate can be tackled by solving the Linear Matrix Inequalities (LMI) feasibility problem, which is efficient and makes the proposed method formally sound. The experimental results demonstrate that our approach is more effective and practical than the traditional SOS-based barrier certificates synthesis and the state-of-the-art neural barrier certificates learning approach.

This paper investigates the controllability and synchronization of a newly designed three-dimensional chaotic system using active and adaptive control strategies. Although both controllers were designed with the help of a positive definite function using Lyapunov theory, for adaptive controllers, we estimated an unknown parameter of the system in real time and adjusted the control signal accordingly to maintain stability. Moreover, numerical simulations demonstrated that the active control approach achieved stability for both equilibrium points ($p_1$ and $p_2$) approximately at time t = $0.5$ s, demonstrating its rapid convergence and robust performance. In contrast, the adaptive control method stabilized $p_1$ at approximately $t\approx 0.5$ and $p_2$ at $t\approx 1$ s, illustrating reaching their desired conditions. Furthermore, the considered methods could effectively synchronize two identical chaotic systems, where the slave system overlapped the master system at approximately $t=5$ s. Apart from this, a detailed comparative analysis of the two techniques in terms of controllability and synchronization is presented. Moreover, the complementary strengths of these methods provide valuable perspectives for broader applications in chaotic system management and security-critical systems.

This article presents a novel approach to the safety verification of hybrid systems by synthesizing neural barrier certificates (BCs) via counterexample-guided neural network (NN) learning combined with sum-of-square (SOS)-based verification. We learn more easily verifiable BCs with NN polynomial expansions in a high-accuracy counterexamples guided framework. By leveraging the polynomial candidates yielded from the learning phase, we reformulate the identification of real BCs as convex linear matrix inequality (LMI) feasibility testing problems, instead of directly solving the inherently NP-hard nonconvex bilinear matrix inequality (BMI) problems associated with SOS-based BC generation. Furthermore, we decompose the large SOS verification programming into several manageable subprogrammings. Benefiting from the efficiency and scalability advantages, our approach can synthesize BCs not amenable to existing methods and handle more general hybrid systems.

Polynomial inequality proving is fundamental to many mathematical disciplines and finds wide applications in diverse fields. Current traditional algebraic methods are based on searching for a polynomial positive definite representation over a set of basis. However, these methods are limited by truncation degree. To address this issue, this paper proposes an approach based on reinforcement learning to find a {Krivine-basis} representation for proving polynomial inequalities. Specifically, we formulate the inequality proving problem as a linear programming (LP) problem and encode it as a basis selection problem using reinforcement learning (RL), achieving a non-negative {Krivine basis}. Moreover, a fast multivariate polynomial multiplication method based on Fast Fourier Transform (FFT) is employed to enhance the efficiency of action space search. Furthermore, we have implemented a tool called {APPIRL} (Automated Proof of Polynomial Inequalities via Reinforcement Learning). Experimental evaluation on benchmark problems demonstrates the feasibility and effectiveness of our approach. In addition, {APPIRL} has been successfully applied to solve the maximum stable set problem.