计算机科学与探索

作者：印婵, 祝义, 王金永, 陈小颖, 郝国生

单位：1. 江苏师范大学 计算机科学与技术学院，江苏 徐州 2211162. 徐州工程学院 信息工程学院，江苏 徐州 2210183. 南京大学 计算机科学与技术系，南京 210023

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

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

深度强化学习是目前信息物理融合系统（CPS）决策中常用的一种方法。然而，当面对未知环境和复杂任务时，基于黑盒的深度强化学习方法在系统的安全性和奖励函数设置的可解释性方面存在不足。针对上述问题，提出了一种形式化时空规则验证制导的安全强化学习方法。提出了时空规则通信顺序进程（CSR-TCSP）对系统进行建模，并结合时空规约语言（STSL）和模型检测工具FDR对进程代数模型进行验证。利用系统环境模型形式化奖励状态机的结构，提出了时空规则奖励状态机（STR-RM）以指导强化学习中奖励函数的设置。此外，为了监测系统的运行并确保输出决策的安全性，设计了一个监控器及安全动作决策算法以获得更安全的状态行为策略。通过一个自动驾驶系统中的避障与变道超车实例，证明所提方法的有效性。

来源：2025年第2期

《计算机科学与探索》期刊编辑部

查看计算机科学与探索杂志2025年第2期