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

来源：软件学报杂志2017年第5期北京时间：

作者：刘涛,王淑灵,詹乃军

单位：刘涛，计算机科学国家重点实验室(中国科学院 软件研究所), 北京 10019011,王淑灵，计算机科学国家重点实验室(中国科学院 软件研究所), 北京 10019002,詹乃军，计算机科学国家重点实验室(中国科学院 软件研究所), 北京 10019003

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

关键词：人工智能;机器人;混成通信顺序进程;混成系统;形式化验证;定理证明

基金资助：国家自然科学基金（91118007，6110006，61304185）