多机器人路径规划的安全性验证

• 作者: 刘涛 王淑灵 詹乃军
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 人工智能 机器人 混成通信顺序进程 混成系统 形式化验证 定理证明
• 年，卷（期）: 2017,（5）
• 所属期刊栏目: 形式化方法与应用专题
• 页码范围: 1118-1127
• 页数: 10页
• 分类号: TP311
• 字数: 7408字
• 语种: 中文
• DOI: 10.13328/j.cnki.jos.005207

摘要

近年来,伴随着人工智能领域的浪潮,机器人越来越多地出现在我们的日常生活中,例如足球机器人、无人机、无人车等,如何保证这些自治机器人尤其是多个机器人在移动过程中的安全,成为人们一直很关心的问题,混成通信顺序进程(hybrid communicating sequential process,简称HCSP)是一种针对混成系统的形式化建模语言,在通信顺序进程(communicating sequential process,简称CSP)的基础上引入了微分方程以描述混成系统中的连续行为和控制逻辑,可以方便而高效地对大型控制系统,尤其是在有通信事件发生时的情形进行形式化建模.用HCSP建模多机器人的路径控制算法,并用定理证明工具HProver进行形式化验证,结果表明,在满足一定的初始条件下,机器人团队在整个运行途中不会发生碰撞.