计算机应用研究

作者：张杰,刘耕阳,关永,

单位：1.北京化工大学信息科学与技术学院,北京100029；2.首都师范大学信息工程学院,北京100048；

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

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

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

来源：2019年第2期

《计算机应用研究》期刊编辑部

查看计算机应用研究杂志2019年第2期