Research On Data-Driven Learning Method For Safe Dynamic Systems

A cyber-physical system(CPS)is a complex system that integrates computing,communication,control and sensing technologies,and is widely used in intelligent transportation,industrial manufacturing,aerospace,smart home and other fields.Dynamic system theory provides a mathematical modeling method,which can be used to describe the motion state and change trend of CPS or its subsystems,and realize control and optimization.Through dynamic system modeling,researchers can understand the behavior and characteristics of the system more clearly,explore the internal laws and mechanisms of the system,so as to provide reference and guidance for the design and control of the system,and improve the reliability,safety and efficiency of the system.However,due to the complexity and uncertainty of dynamic system behavior,traditional modeling methods face challenges in accuracy,efficiency,and scalability.Deep learning techniques provide simple and flexible modeling schemes for dynamic systems,but their inexplicability limits their application in safety-critical domains.Formal methods can make up for the shortcomings of deep learning technology to a certain extent.This method analyzes the design of the system and detects potential errors and defects through mathematical calculation and logical reasoning,providing a strict guarantee for the correctness of computer software systems.In this paper,we propose a formal learning method for dynamic systems with safety and reachability,which combines the powerful modeling capabilities of deep learning and the rigorous logic of formal methods to automatically learn and verify dynamic system models to ensure that they conform to the predefined specification--safety and reachability.Among them,safety means that for a given initial state of the system,the system will not enter the unsafe state set during the evolution of time;reachability means that the system state can always enter the target state set over time.The research content of this paper is as follows:· Research on formal learning methods for discrete systems.The neural network Lyapunov barrier certificate(LBC)and its training method for discrete systems are designed.LBC is a general certificate that indicates the safety and reachability of the system.The trained neural network certificates are validated by mixed integer linear programming techniques,an optimization technique that can be used to solve mathematical optimization problems involving continuous and discrete variables.By formulating the verification problem of the neural network as an optimization problem with binary variables and solving it,it is possible to determine whether the model and the neural network certificate meet the specification.Experimental results show that this method can successfully synthesize LBC of discrete systems,and has better long-term prediction effect than DDPG(Deep Deterministic Policy Gradient).· Research on formal learning methods for continuous systems.Due to the different forms of continuous systems and discrete systems,the forms of Lyapunov barrier certificates are also different,so the loss function needs to be designed in a targeted manner.To verify the Lie derivative condition in LBC in continuous form,mixed integer quadratic programming is employed,a programming technique used to solve optimization problems involving linear and quadratic constraints.In experiments,applying this formal learning method successfully synthesized neural network certificates and accurately reconstructed the vector field of the system.· Implemented a formal learning framework FLMSR for the above two methods.The framework consists of three interactive parts: Learner,Seeker and Verifier.Among them,the Learner is used to jointly learn the dynamic system model and the neural network certificate.The Seeker samples the system state space and finds counterexamples through simulation.The counterexamples will be used to update the model and certificate in the next iteration.Seeker’s way of finding counterexamples is computing power-saving.If this method fails to find counterexamples,Verifier will verify the model and certificate to provide a formal guarantee for the safety and reachability of the model.