一种针对安全可达动态系统的形式化学习方法

Formal learning approach for safe and reachable dynamical systems

在动态系统建模问题中,深度学习为建模提供了更便捷和灵活的方法,但其难以解释的特点降低了模型的可靠性。针对具有安全性和可达性的动态系统,提出了一种形式化模型学习方法,将安全性和可达性引入到对目标系统的学习过程中,使模型满足这两个性质。为保证所学系统在定义域上严格满足这两个性质,该方法基于现代控制理论中的Lyapunov方法和Barrier函数设计了可验证的Lyapunov Barrier函数(LBF),通过将其与动态系统联合学习,使得LBF能够为所学系统提供安全性和可达性保障。最后通过求解混合整数线性规划问题验证了模型确实满足相关性质,与DDPG的对比实验展示了这一方法的有效性。

In the problem of dynamic system modeling,deep learning based techniques make modeling more convenient and flexible,but it reduces the reliability of the learned model because of the difficulty in explanation.For dynamic systems with safety and reachability,this paper proposed a formal learning approach that introduced safety and reachability into the learning process of the target system,making the model satisfy these two properties.In order to ensure that the learned system strictly satisfies these two properties in the entire state space,this approach combined the Lyapunov method with Barrier function in modern control theory,and designed a verifiable Lyapunov Barrier function(LBF),which was jointly learned with the dynamic system and guarantee security and reachability for the learned system.In addition,this paper employed the mixed integer linear programming in the verification about that the model satisfied the relevant properties.It makes a comparison with DDPG based method and the experimental results demonstrate the effectiveness and efficiency of the proposed approach.