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

High-order-logical Modeling and Verification of Region Coverage Algorithm with Swarm Robots

作　　者：尹晓娜 王国辉[1] 施智平[1] 关永[1] 张倩颖[1] 张景芝 YIN Xiao-na;WANG Guo-hui;SHI Zhi-ping;GUAN Yong;ZHANG Qian-ying;ZHANG Jing-zhi(Beijing Engineering Research Center of High Reliable Embedded System,Capital Normal University,Beijing 100048,China)

机构地区：[1]高可靠嵌入式系统技术北京市工程研究中心,首都师范大学信息工程学院,北京100048

出　　处：《小型微型计算机系统》2022年第3期475-482,共8页Journal of Chinese Computer Systems

基　　金：国家重点研发计划项目(2019YFB1309900)资助;国家自然科学基金项目(61876111,61877040,62002246)资助;特区项目(18-163-11-ZT-005-038-05)资助;北京市教委科技计划一般项目(KM20190028005)资助;科技创新服务能力建设-基本科研业务费(科研费)项目(00621530290000)资助。

摘　　要：区域覆盖算法广泛用于群机器人解决资源勘查、目标搜救、地形测绘等问题.目前,对区域覆盖算法的研究主要是用传统计算机仿真和数值计算方法对算法模型进行测试,然而,软件系统缺陷可能会使测试结果出现偏差,导致任务失败.因此,本文采用定理证明的形式化方法,基于交互定理证明器HOL-Light中集合库、实分析库等定理证明库,实现了群机器人工作场景的高阶逻辑表达;完成了机器人移动概率和平均移动概率的建模与验证;最终验证了一定时间步长内群机器人在特定区域内的覆盖率的正确性.为实现多种复杂场景下群机器人区域覆盖算法的高阶逻辑定理证明形式化分析奠定基础.Region coverage algorithm is widely used in swarm robots on resource exploration,target searching and rescuing,terrain mapping and others.At present,the research on region coverage algorithm mainly test the algorithm model using the traditional computer simulation and numerical calculation methods.However,the software defects may lead to the deviation of the test results and the failure of the task.Therefore,it is highly necessary to be verified in the formal method of theorem proving.For this purpose,the high-order logic expression of scenarios,the swarm robots work on,are formalized based on the library of screw theory such as set library and real analysis library on the interactive theorem prover named HOL-Light.The probability of robot movement and the probability of average movement are formalized.And then,the coverage rate of swarm robots in a specific area within a certain time is verified.It lays a foundation for the formal analysis using the higher order logic theorem proving of the region coverage algorithm with swarm robots in a variety of complex scenarios.

关 键 词：群机器人 区域覆盖 高阶逻辑 定理证明 形式化验证 

分 类 号：TP302[自动化与计算机技术—计算机系统结构]