面向CPS时空规则验证制导的安全强化学习  

Formal Verification of Spatio-Temporal Rules Guided Safe Reinforcement Learning for CPS

作　　者：印婵 祝义[1] 王金永 陈小颖 郝国生[1] YIN Chan;ZHU Yi;WANG Jinyong;CHEN Xiaoying;HAO Guosheng(College of Computer Science and Technology,Jiangsu Normal University,Xuzhou,Jiangsu 221116,China;School of Information Engineering,Xuzhou Institute of Technology,Xuzhou,Jiangsu 221018,China;Department of Computer Science and Technology,Nanjing University,Nanjing 210023,China)

机构地区：[1]江苏师范大学计算机科学与技术学院,江苏徐州221116 [2]徐州工程学院信息工程学院,江苏徐州221018 [3]南京大学计算机科学与技术系,南京210023

出　　处：《计算机科学与探索》2025年第2期513-527,共15页Journal of Frontiers of Computer Science and Technology

基　　金：国家自然科学基金(62077029,62277030);CCF-华为胡杨林基金(CCF-HuaweiFM202209);高安全系统的软件开发与验证技术工业和信息化部重点实验室开放项目基金(NJ2020022);江苏省研究生科研与实践创新项目(SJCX22_1261)。

摘　　要：深度强化学习是目前信息物理融合系统(CPS)决策中常用的一种方法。然而,当面对未知环境和复杂任务时,基于黑盒的深度强化学习方法在系统的安全性和奖励函数设置的可解释性方面存在不足。针对上述问题,提出了一种形式化时空规则验证制导的安全强化学习方法。提出了时空规则通信顺序进程(CSR-TCSP)对系统进行建模,并结合时空规约语言(STSL)和模型检测工具FDR对进程代数模型进行验证。利用系统环境模型形式化奖励状态机的结构,提出了时空规则奖励状态机(STR-RM)以指导强化学习中奖励函数的设置。此外,为了监测系统的运行并确保输出决策的安全性,设计了一个监控器及安全动作决策算法以获得更安全的状态行为策略。通过一个自动驾驶系统中的避障与变道超车实例,证明所提方法的有效性。ing the system environment model to propose the spatio-temporal rule reward machine(STR-RM)which can guide the setting of reward functions in reinforcement learning.In addition,to monitor system operation and ensure the safety of output decisions,a monitor and a safe action decision-making algorithm are designed to obtain a more secure state-action strategy.Finally,the effectiveness of the proposed method is demonstrated through an example of obstacle avoidance and lane-changing overtaking in the autonomous driving system.

关 键 词：信息物理融合系统 形式化方法 进程代数 安全强化学习 自动驾驶 

分 类 号：TP181[自动化与计算机技术—控制理论与控制工程]