一种水下群机器人路径规划算法的形式化研究

摘要：

为了增强基于遗传算法的水下群机器人路径规划算法正确性的说服力,使用定理证明对其进行形式化研究,给出算法在定理证明器HOL4中的形式化模型.基于算法形式化的一般步骤,对算法的设计进行了详细的分析,指出算法设计的核心步骤和建模难点.在此基础上建立了总体形式化建模框架,然后对其进行化简,得到种群初始化、选择、交叉三个核心模块.给出了模型中要用到的基本数据类型的形式化描述,并分别对三个模块进行形式化描述,最终得到算法的形式化模型.通过证明与模型相关的97条性质,说明了模型的合理性及有效性,在此模型的基础上,可以完成对算法的形式化验证,同时还能拓展HOL4的应用范围.

关键词：遗传算法、群机器人、路径规划、定理证明、形式化建模、HOL4

所属期刊栏目：36

分类号：TP311.5(计算技术、计算机技术)

资助基金：国家自然科学基金资助项目61572331

在线出版日期：2019-05-31（万方平台首次上网日期，不代表论文的发表时间）

页数：共5页

页码：490-494