典型文献
群机器人区域覆盖算法高阶逻辑建模与验证
文献摘要：
区域覆盖算法广泛用于群机器人解决资源勘查、目标搜救、地形测绘等问题.目前,对区域覆盖算法的研究主要是用传统计算机仿真和数值计算方法对算法模型进行测试,然而,软件系统缺陷可能会使测试结果出现偏差,导致任务失败.因此,本文采用定理证明的形式化方法,基于交互定理证明器HOL-Light中集合库、实分析库等定理证明库,实现了群机器人工作场景的高阶逻辑表达;完成了机器人移动概率和平均移动概率的建模与验证;最终验证了一定时间步长内群机器人在特定区域内的覆盖率的正确性.为实现多种复杂场景下群机器人区域覆盖算法的高阶逻辑定理证明形式化分析奠定基础.
文献关键词：
群机器人;区域覆盖;高阶逻辑;定理证明;形式化验证
中图分类号：
作者姓名：
尹晓娜;王国辉;施智平;关永;张倩颖;张景芝
作者机构：
高可靠嵌入式系统技术北京市工程研究中心,首都师范大学信息工程学院,北京100048
文献出处：
引用格式：
[1]尹晓娜;王国辉;施智平;关永;张倩颖;张景芝-.群机器人区域覆盖算法高阶逻辑建模与验证)[J].小型微型计算机系统,2022(03):475-482
A类：
B类：
群机器人,区域覆盖,覆盖算法,高阶逻辑,资源勘查,搜救,地形测绘,计算机仿真,数值计算方法,算法模型,软件系统,系统缺陷,定理证明,形式化方法,互定,明器,HOL,Light,中集,工作场景,逻辑表达,平均移动,时间步长,特定区域,复杂场景,形式化分析,形式化验证
AB值：
0.382294
机标中图分类号，由域田数据科技根据网络公开资料自动分析生成，仅供学习研究参考。
