Safe Neural Network Controller Synthesis and Verification for Hybrid Systems

Controller synthesis is a fundamental problem in hybrid system control. The synthesis of safe controllers is related to the use of hybrid systems in safety-critical fields. This paper proposes a novel approach to synthesizing neural network controllers with safety guarantees for hybrid systems. The safety of neural network controllers is guaranteed by barrier certificates, which are simultaneously synthesized with the controllers. To learn safe neural network controllers, first, the network structures of the controllers are determined, and the training datasets are constructed based on the hybrid system. Then, the loss function of network training is encoded based on the barrier certificate conditions guaranteeing the safety of the controllers. When the training process completes, the learned controllers are safe on training datasets but may not be safe on the whole hybrid system. To verify the safety of the learned controllers on the whole system, this paper transforms the certification of safety conditions into a group of mixed-integer programming problems and adopts the numerical optimization solver to get formally guaranteed results. We implement the safe neural network controller synthesis tool SafeNC and evaluate its performance on 8 benchmark systems. SafeNC successfully synthesizes large controllers with up to 6 hidden layers and 1804 neurons. The experimental results show that SafeNC can deal with more complex systems, and is more effective and scalable than the existing methods. © 2023 Chinese Academy of Sciences. All rights reserved.