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

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