An iterative scheme of hybrid controller synthesis for nonlinear systems subject to safety constraints

For many safety-critical systems, there is a pressing need for learning the controllers to endow systems with properties of safety. Reinforcement learning (RL) has emerged as a promising approach to synthesizing controllers that satisfy safety requirements by leveraging user-defined reward functions to encode desired system behavior. However, it remains a significant challenge in synthesizing provably correct controllers with safety requirements. To address this issue, we try to design a special hybrid polynomial-NN controller that is easy to verify without losing its expressiveness and flexibility. This paper proposes an iterative framework to synthesize a hybrid controller based on RL, low-degree polynomial fitting and knowledge distillation. By formulating and solving a constrained optimization problem in which the verification conditions produce the barrier certificates, a computational method is given to ensure that every trajectory starting from the initial set of the system with the resulting controller satisfies the given safety requirement. In addition, we have implemented a tool named SynHC and evaluated its performance over a set of benchmark examples. The experimental results demonstrate that our approach efficiently synthesizes safe DNN controllers.