群机器人区域覆盖算法高阶逻辑建模与验证

区域覆盖算法广泛用于群机器人解决资源勘查、目标搜救、地形测绘等问题.目前,对区域覆盖算法的研究主要是用传统计算机仿真和数值计算方法对算法模型进行测试,然而,软件系统缺陷可能会使测试结果出现偏差,导致任务失败.因此,本文采用定理证明的形式化方法,基于交互定理证明器HOL-Light中集合库、实分析库等定理证明库,实现了群机器人工作场景的高阶逻辑表达;完成了机器人移动概率和平均移动概率的建模与验证;最终验证了一定时间步长内群机器人在特定区域内的覆盖率的正确性.为实现多种复杂场景下群机器人区域覆盖算法的高阶逻辑定理证明形式化分析奠定基础.