一种面向概率深度强化学习系统的形式化验证方法、系统及应用

本发明公开了一种面向概率深度强化学习系统的形式化验证方法，主要用于验证由非确定性深度强化学习算法训练获得的系统的安全问题，具体步骤包括：(1)抽象训练：基于现有的抽象训练技术离散化抽象并进行抽象训练；(2)概率模型建模：依据原系统动力学设计抽象状态空间上的状态迁移规则，构建离散马尔科夫链模型；(3)验证分析：给出描述系统安全性质的PCTL时序逻辑规范，利用STORM概率模型检查器验证系统安全。本发明能够自动完成对概率深度强化学习系统的概率安全性质的检查，提供深度强化学习应用中的安全性。本发明还公开了一种实现所属概率系统形式化验证方法的工具。