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

尹晓娜，王国辉，施智平，关 永，张倩颖，张景芝

(高可靠嵌入式系统技术北京市工程研究中心，首都师范大学信息工程学院，北京100048)

1 引 言

群机器人系统是一个多机器人系统，每个机器人个体按照一定的行为规则，实现个体之间的交互，从而使整体达到预期的任务目标.在群机器人系统中，每个机器人个体感知搜索区域中的信息能力是有限的，完成任务目标是大量简单个体机器人交互的结果，是一种整体行为的实现，并不依赖于某一个体的主控作用[1，2].因此群机器人系统具有鲁棒性、灵活性以及规模可伸缩性等特点[3]，可广泛用于区域覆盖的相关应用如资源勘查[4]、目标搜救[5]以及地形测绘[6]等领域.

群机器人区域覆盖是指群机器人系统中的个体通过具有一定感知能力的传感器探索访问一定的区域，利用多个机器人的相互协作，完成相应任务的过程[7].例如，当地震等自然灾害发生后，可利用群机器人进行探索并对幸存人员进行搜救[8]；当有易燃易爆物品存在、爆炸性或窒息性气体泄露时，可利用群机器人在事故发生现场对危险源追踪检测[9]；当陆地或海底发现新资源时，可利用群机器人进行地形测绘.上述任务均具有目标区域内的每个点曾经被机器人覆盖过，但并不需要机器人在目标区域内持续性覆盖的特点[10]，因此，通常用非持续性区域覆盖方法[11]来解决.目前，学者主要对非持续性区域覆盖算法和覆盖率进行研究，如2013年兰州理工大学的张国有等人[12]采用三元组定义了区域覆盖问题.2018年上海海事大学的孙冰等人[14]研究了基于网格图和神经网络的多AUV(水下自主机器人)完整覆盖问题.2020年四川大学的石海云[13]分析了现实条件下的多目标检索问题.上述研究成果主要集中在用传统计算机仿真和数值计算方法解决实际问题，其提出的数学模型尚未得到系统的形式化验证.

基于传统计算机仿真技术的系统分析，是在仿真软件上对系统设计模型进行测试.这种方法虽然高效，但在涉及伪随机数时，仿真平台不能保证仿真结果的准确性[15].基于计算机代数系统方法在边界条件的处理上存在短板，可能因其自身的不完整性而不能给出精确的结果[16，17].和以上传统方法不同，形式化验证根据系统形式规范或属性，使用数学方法证明系统的正确性，对所验证的性质而言是精确和完备的[18].基于定理证明的形式化方法能够进行精确的系统分析，克服上述仿真方法带来的局限性.

在区域覆盖任务过程中，机器人移动方向的随机性会影响给定时间内的区域覆盖率.因此本文基于离散概率分析[19]的方法，在高阶逻辑定理证明器HOL-Light中对机器人区域覆盖率进行形式化验证.

本文的主要贡献如下：

1)群机器人响应阈值模型的形式化建模；

2)群机器人移动概率的形式化描述；

3)机器人区域覆盖算法的形式化建模与验证.

论文组织结构如下：第2节对高阶逻辑定理证明器HOL-Light、概率论高阶逻辑表达以及区域覆盖算法相关知识进行简要介绍；第3节对机器人移动区域进行形式化描述；第4节对群机器人响应阈值模型进行形式化建模，进而实现机器人移动概率和平均移动概率的建模与验证；第5节对群机器人区域覆盖算法进行形式化建模与验证；最后总结全文.

2 预备知识

2.1 HOL-Light

HOL-Light是一种高阶逻辑定理证明器.高阶逻辑可以形式化描述任何具有逻辑性的系统模型或具有封闭性的数学表达式.在HOL-Light中，系统验证过程一般分为3个步骤：1)将系统进行形式化建模；2)将所需验证的系统属性形式化为目标任务；3)运用合适的策略和定理验证目标任务.

目前，HOL-Light中存在较为完整的证明策略和定理库，例如集合库、实分析库、实数库等，为本文的工作提供了保证.因此，本文选择使用定理证明器HOL-Light对机器人区域覆盖算法进行形式化建模与验证.为了更好的理解本文内容，表1对定理证明器HOL-Light 中一些常用的符号与函数进行解释.

表1 HOL-Light 符号与函数Table 1 HOL-Light symbols and functions

2.2 概率论高阶逻辑表达

在数学上，令(Ω，F)为可测空间，μ为可测空间上的测度，则称三元组(Ω，F，μ)为测度空间.μ(Ω)=1的测度空间称为概率空间，记为(Ω，F，P).其中Ω是一个集合，称为样本空间，F是Ω的子集族，称为事件集，P的值为1，是样本空间的测度，称为概率测度.它们在HOL-Light中的形式化定义如下：

定义1.样本空间

|-p_space=m_space_s

在定义1中，m_space_s表示空间Ω.

定义2.事件

|-events=measurable_sets

在定义2中，measurable_sets表示可测集.

定义3.概率

|-prob=measure_s

在定义3中，measure_s表示测度.

定义4.概率空间

|-∀p.prob_space p<=>

measure_space p/measure_s p(p_space p)=&1

在定义4中，measure_spacep表示测度空间p.

定义5.随机变量

|-∀X p.

real_random_variable X p<=>

prob_space p∧X IN real_borel_measurable(p_space p，events p)

在定义5中，X表示随机变量，p表示给定的概率空间，real_borel_measurable表示一个包含所有开集的最小σ代数.

定义6.期望

|-∀X p.

expectation p X=

sum(IMAGE X(p_space p))

(λr.r*prob p(PREIMAGE X{r}INTER p_space p))

在定义6中，(IMAGEX(p_spacep))表示样本空间p在映射X下的像，PREIMAGEX{r}表示{r}关于映射X的原像.

2.3 区域覆盖算法

在群机器人执行覆盖任务时，首先，nr个机器人进入给定的区域，在单位时间pt内每个机器人ri(i=1…nr)检测自身所在位置和该位置邻近单元格的刺激量，进而计算响应阈值.然后，机器人根据响应阈值的结果确定移动方向并执行移动操作.最后，在给定的时间步长t内，根据统计的群机器人覆盖单元格数和给定区域单元格数量的比值，计算出区域覆盖率.算法1给出了区域覆盖算法的具体步骤.

算法1.群机器人区域覆盖算法

输入：区域栅格化后单元格数量m×n，单元格刺激量s机器人数量nr，响应阈值θ，时间步t

输出：区域覆盖率

1.%初始化

当前时间步pt=0；群机器人随机分布在区域内；

2.%群机器人执行移动操作

repeat

loop i=1…nr

检测机器人ri所在单元格(x，y)

检测邻近单元格刺激量

根据响应函数确定移动到的单元格位置(x′，y′)

end loop

pt=pt+1

until pt>t

3.%计算区域覆盖率

统计群机器人覆盖单元格数，计算区域覆盖率

3 群机器人工作场景形式化描述

在给定区域内，群机器人通过协作完成区域覆盖任务.将机器人所需覆盖的区域表示为二维栅格化区域，区域大小为m×n(2

机器人移动区域形式化描述如定义7所示.定义7中 x IN 1…m 表示x在1到m的范围内，即(x I N 1…m)⟺1≤x∧x≤m，y IN 1…n 表示y在1到n的范围内.

定义7.机器人移动区域

|-∀m n.

move_area m n=

{x，y | x IN 1…m∧y IN 1…n∧2

图1给出了机器人移动区域可以划分的3种情况.栅栏非边界的单元格((1

图1 移动区域栅格图Fig.1 Grid diagram of the move area

定义8.栅栏非边界的单元格

|-∀m n.

move_area_inner m n=

{x，y | 1

定义9.栅栏边界非顶点的单元格

|-∀m n.

move_area_bound_nonvertex m n=

{x，y |(x=1∧1

(x=m∧1

(y=1∧1

(y=n∧1

2

定义10.栅栏顶点处单元格

|-∀m n.

move_area_vertex m n=

{x，y |(x=1∧y=1)∨(x=1∧y=n)∨

(x=m∧y=1)∨(x=m∧y=n)∧2

区域覆盖率可以用已覆盖单元格数量和单元格总数量的比值表示.因此，区域覆盖率的形式化需要用到区域单元格数量相关定理.结合图1可知，栅栏非边界的单元格数量为(m×n-2(m+n)+4，栅栏边界非顶点的单元格数量为(2×(m+n)-4)，栅栏顶点单元格数量为4，分别形式化描述为定理1、定理2、定理3.

定理1.栅栏非边界的单元格数量

|-∀m n.

2

==> &(CARD(move_area_inner m n))

=&m*&n-&2*(&m+&n)+&4

定理2.栅栏边界非顶点的单元格数量

|-∀m n.

2

==> &(CARD(move_area_bound_nonvertex m n))

=&2*((&m+&n)-&4)

定理3.栅栏顶点数量

|-∀m n.

2

==>&(CARD(move_area_vertex m n))=&4

定理1-定理3中，CARDs表示集合s中元素的数量.上述定理的证明思路相似，但复杂度不一.因此，以较为复杂的定理2为例进行介绍.首先，重写栅栏边界非顶点的单元格定义将目标展开.然后，采用化简策略SIMP_TAC以及处理集合运算的相关定理(如结合律、分配对偶律等)对目标化简，并将目标改写成笛卡尔积的表达形式.最后，利用CARD库中如CARD_CROSS(表示笛卡尔积表达形式下集合元素的数量)、CARD_SING(表示单个集合元素的数量)等相关定理对目标进行验证.

机器人执行移动操作后所抵达位置情况的数学表达式如式(1)所示：

(1)

其形式化描述如定义11所示.

定义11.机器人可移动区域

|-∀m n h.

movable_area h m n=

(if FST h IN 1…m∧SND h IN 1…n∧2

then if 1

then {a，b |(abs(&a-&(FST h))=&1∨a=FST h)∧

(abs(&b-&(SND h))=&1∨b=SND h)∧

～(a=FST h∧b=SND h)}

else if FST h=1

then if SND h=1

then {(1，2)，(2，1)，(2，2)}

else if SND h=n

then {(1，n-1)，(2，n-1)，(2，n)}

else {a，b |(&a-&(FST h)=&1∨a=FST h)∧

(abs(&b-&(SND h))=&1∨

b=SND h)∧～(a=FST h∧b=SND h)}

else if FST h=m

then if SND h=1

then {(m-1，1)，(m-1，2)，(m，2)}

else if SND h=n

then {(m-1，n-1)，(m-1，n)，(m，n-1)}

else {a，b |(&a-&(FST h)=--&1∨a=FST h)∧

(abs(&b-&(SND h))=&1∨b=SND h)∧

～(a=FST h∧b=SND h)}

else if SND h=1

then {a，b |(abs(&a-&(FST h))=&1∨

a=FST h)∧

(&b-&(SND h)=&1∨b=SND h)∧

～(a=FST h∧b=SND h)}

else {a，b |(abs(&a-&(FST h))=&1∨

a=FST h)∧(&b-&(SND h)=--&1∨

b=SND h)∧～(a=FST h∧b=SND h)}

else {})

定义11中嵌套了if…else…语句用于选择判断，可根据不同条件执行不同操作，if P then Q else R表示P成立则Q成立，反之R成立，即(P⟹Q)∧(P⟹R).其中，h表示数对(x′，y′)，FST表示为数对h中的第一个值x′，SND表示为数对h中的第二个值y′.

根据机器人所在位置情况不同，执行移动操作后，机器人到达相邻单元格分别形式化描述为定义12、定义13、定义14，即栅栏非边界区域相邻的单元格、栅栏边界非顶点区域相邻的单元格、栅栏顶点区域相邻的单元格.

定义12.栅栏非边界区域相邻的单元格

|-∀m n h.

movable_area_inner h m n=

{a，b | 1

1

(abs(&a-&(FST h))=&1∨a=FST h)∧

(abs(&b-&(SND h))=&1∨b=SND h)∧

～(a=FST h∧b=SND h)}

定义13.栅栏边界非顶点区域相邻的单元格

|-∀m n h.

movable_area_bound_nonvertex h m n=

{a，b |(FST h=1∧1

2

(&a-&(FST h)=&1∨a=FST h)∧

(abs(&b-&(SND h))=&1∨b=SND h)∧

～(a=FST h∧b=SND h))∨

(FST h=m∧1

2

(&a-&(FST h)=--&1∨a=FST h)∧

(abs(&b-&(SND h))=&1∨b=SND h)∧

～(a=FST h∧b=SND h))∨

(SND h=1∧1

2

(abs(&a-&(FST h))=&1∨a=FST h)∧

(&b-&(SND h)=&1∨b=SND h)∧

～(a=FST h∧b=SND h))∨

(SND h=n∧1

2

(abs(&a-&(FST h))=&1∨a=FST h)∧

(&b-&(SND h)=--&1∨b=SND h)∧

～(a=FST h∧b=SND h))}

定义14.栅栏顶点区域相邻的单元格

|-∀hm n.

movable_area_vertex h m n=

{a，b|FST h=1∧SND h=1∧

2

(a，b=1，2∨a，b=2，1∨a，b=2，2)∨

FST h=1∧SND h=n∧

2

(a，b=1，n-1∨a，b=2，n-1∨a，b=2，n)∨

FST x=m∧SND x=1∧

2

(a，b=m，2∨a，b=m-1，1∨a，b=m-1，2)∨

FST h=m∧SND h=n∧

2

(a，b=m，n-1∨a，b=m-1，n∨a，b=m-1，n-1)}

定义12中的栅栏非边界区域相邻的单元格是机器人在原位置为C区域上执行移动操作之后到达的位置在HOL-Light中的表示形式.同样，定义13中的栅栏边界非顶点区域相邻的单元格、定义14中的栅栏顶点区域相邻的单元格分别是机器人在原位置为B区域、A区域上执行移动操作之后到达的位置在HOL-Light中的表示形式.

群机器人的移动概率与机器人执行移动操作之后可能到达位置的个数有关，因此将栅栏非边界区域、边界非顶点区域、顶点区域相邻的单元格数量分别形式化描述为定理4、定理5、定理6.

定理4.栅栏非边界区域相邻的单元格数量

|-∀x y m n.

1

==> CARD(movable_area(x，y)m n)=8

定理5.栅栏边界非顶点区域相邻的单元格数

|-∀x y m n.

((x=1∨x=m)∧1

(y=1∨y=n)∧1

2

==> CARD(movable_area(x，y)m n)=5

定理6.栅栏顶点区域相邻的单元格数量

|-∀x y m n.

(x=1∨x=m)∧(y=1∨y=n)∧2

==> CARD(movable_area(x，y)m n)=3

4 机器人移动概率平均方法形式化

机器人具有一定的感知能力.在区域移动过程中，机器人将感知的周围环境的信息作为输入信号，这些输入信号称为刺激量，影响机器人执行移动操作的决策.机器人具有独立的响应阈值θ，每个单元格具有一个刺激量s，机器人选择下一单元格的概率由响应函数决定，响应函数如式(2)所示:

(2)

其形式化描述如定义15所示:

定义15.响应函数

|-∀a x m n s theta

response_fun x a s theta m n=

(if x，a IN move_area m n CROSS

movable_area x m n

then if x，a IN

move_area_inner m n CROSS

movable_area x m n UNION

move_area_bound_nonvertex m n CROSS

movable_area x m n UNION

move_area_vertex m n CROSS

movable_area x m n

then s a pow 2*

inv(sum(movable_area3 x m n)(λi.s i pow 2)+theta pow 2)

else &0

else &0)

定义15中的response_fun是响应函数在HOL-Light中的表示.根据对机器人移动操作分析，机器人从t时刻的位置到达t+1时刻的位置，到达位置并不能确定.依据区域覆盖算法，在给定区域内，机器人执行移动操作，移动到相邻单元格具有一定的概率，如式(3)所示:

(3)

其中，(x，y)∈A∩B∩C(A、B、C为图1给定区域).

基于以上描述，可实现对机器人移动行为的高阶逻辑建模.由式(3)可知，描述机器人移动到相邻单元格的概率涉及到的变量有机器人原位置(x，y)、机器人移动后到达的位置(x′，y′)、刺激量s以及响应阈值θ等.结合概率论的高阶逻辑表达、机器人移动区域及可移动区域定义，机器人移动到相邻单元格的概率形式化模型可用随机变量X、样本空间p、刺激量s、响应阈值theta、移动区域大小m和n表示，见定义16.

定义16.机器人移动到相邻单元格的移动概率形

|-∀X p s theta m n.

move_prob_rv X p s theta m n<=>

real_random_variable X p∧

events p=

POW

(IMAGE(λ(x，y).(x，y)，CHOICE(movable_area(x，y)m n))

(move_area m n))∧

p_space p=

IMAGE(λ(x，y).(x，y)，CHOICE(movable_area(x，y)m n))

(move_area m n)∧

(∀z.z IN events p

==> prob p z=

sum z(λ((x，y)，a，b).response_fun(x，y)(a，b)s theta m n))

定义16中p为定义实随机变量X的概率空间.CHOICEs表示任取集合s中的一个元素.机器人执行移动操作，从原位置到达某一个相邻的单元格.由于机器人相邻的单元格并不唯一，所以用CHOICE任取一相邻单元格作为机器人移动后到达的位置.POWset表示set的幂集，即POWset={s|s⊂set}.IMAGE(λ(x，y).(x，y)，CHOICE(movable_area(x，y)mn))(move_areamn)表示所有可能事件.((λ(x，y)，a，b).response_fun(x，y)(a，b)sthetamn))为概率函数.

机器人从不同位置移动到相邻单元格的概率的数学表达式如式(4)所示：

(4)

基于上式，在给定区域内机器人移动到某一邻近单元格的平均概率为：

(5)

为方便研究，本文设单元格刺激量为常数，用c表示，并且机器人覆盖区域内无障碍物，不考虑机器人避障问题.当机器人原位置为栅栏非边界((1

定理7.机器人原位置在栅栏非边界处的移动概率形式化

|-∀x y m n a b s theta X p.

move_prob_rv X p(λs.c)theta m n∧2

==> prob p

(IMAGE(λ(x，y).(x，y)，CHOICE(movable_area(x，y)m n))

(move_area_inner m n))=

(&m*&n-&2*(&m+&n)+&4)*c pow 2*

inv(&8*c pow 2+theta pow 2)

在定理7证明过程中，首先重写机器人移动模型(move_prob_rv)定义，然后结合假设列表中的条件引入子目标1——事件“当机器人原位置在栅栏非边界单元格内，执行移动操作后下一步位置在可移动区域”在事件集里，在该子目标证明成立后，就可以在假设列表里直接应用该条件.然后，引入子目标2——当前条件下的响应函数值为c2/(8×c2+θ2)，并结合实数库、集合库、定理4相关内容实现子目标2的证明.最后，采用策略ASM_SIMP_TAC将假设列表中的子目标2写入当前目标并实现化简，结合sum相关定理完成该目标的证明.即实现机器人原位置在栅栏非边界处的移动概率的证明.

机器人原位置分别为栅栏边界非顶点处、栅栏边界顶点处，移动概率的形式化描述如定理8、定理9所示，其证明过程与定理7证明过程相似.

定理8.验证机器人原位置在栅栏边界非顶点处的移动概率

|-∀x y m n a b s theta X p.

move_prob_rv X p(λs.c)theta m n∧2

==> prob p

(IMAGE(λ(x，y).(x，y)，CHOICE(movable_area(x，y)m n))

(move_area_bound_nonvertex m n))=

(&2*((&m+&n)-&4))*c pow 2*

inv(&5*c pow 2+theta pow 2)

定理9.机器人原位置在栅栏顶点处的移动概率形式化

|-∀x y m n a b s theta X p.

move_prob_rv X p(λs.c)theta m n∧2

==> prob p

(IMAGE(λ(x，y).(x，y)，CHOICE(movable_area(x，y)m n))

(move_area_vertex m n))=

&4*c pow 2*inv(&3*c pow 2+theta pow 2)

根据式(2)和式(3)，机器人的平均移动概率可形式化描述为定理10.

定理10.机器人的平均移动概率形式化

|-∀x y m n a b s theta p X.

X=(λ((x，y)，a，b).if x，y IN move_area m n∧

a，b=CHOICE(movable_area(x，y)m n)

then inv(&m*&n)

else &0)∧

move_prob_rv X p(λs.c)theta m n∧

2

==> expectation p X=

inv(&m*&n)*c pow 2*

((&m*&n-&2*(&m+&n)+&4)*

inv(&8*c pow 2+theta pow 2)+

(&2*((&m+&n)-&4))*

inv(&5*c pow 2+theta pow 2)+

&4*inv(&3*c pow 2+theta pow 2))

在定理10证明过程中，首先重写期望(expectation)的定义，结合重写策略REWRITE_TAC化简目标.然后引入3个子目标分别验证机器人原位置在栅栏非边界处、在栅栏边界非顶点处、顶点处的移动概率.最后结合集合库、实分析库相关定理和策略完成定理10的证明，验证了机器人的平均移动概率如式(6)所示:

(6)

5 机器人区域覆盖率形式化建模与验证

区域覆盖任务的完成与刺激量、响应阈值、机器人移动区域大小、机器人数量等变量相关.机器人覆盖率如式(7)所示：

Cover(t)=f(θ/s，Na，nr，t)

(7)

Cover表示覆盖率，θ表示响应阈值，s表示刺激量，Na表示单元格数量，t表示为时间.

事实上机器人移动概率包含两种可能性，一种是移动到未覆盖单元格，另一种是移动到已覆盖单元格.机器人移动到未覆盖单元格概率Pu(t)数学表示形式为：

(8)

在式(8)中，k(t)表示为机器人邻近单元格未覆盖数量，其数学表示为：

(9)

机器人在t时间步内区域覆盖率为：

(10)

根据上述描述可知，机器人邻近单元格未覆盖数量、机器人移动到未覆盖单元格概率、区域覆盖率3个变量之间存在较为复杂的耦合关系，在HOL-Light中无法对这3个变量进行解耦并给出相应的直接表示.因此，本文对涵盖这3个变量的完整区域覆盖算法模型形式化为定义17.

定义17.机器人的区域覆盖模型定义

|-∀expec c theta nr m n.

move_cover nr m n c expec theta<=>

(?k mtoup covp.

k 1=&8*(&1-nr*inv(&m*&n))∧

k 2=&8*(&1-nr*inv(&m*&n))-expec∧

k 3=k 2-k 2*&4*inv(&7)*c pow 2*

inv(&8*c pow 2+theta pow 2)-

&8*nr*inv(&m*&n)∧

(!t.3

==> k t=k(t-1)-inv(&8)*

(k(t-1)*c pow 2*

inv(&8*c pow 2+theta pow 2))*

nr*inv(&m*&n)*sum(1…t-1)

( j.k j*c pow 2*inv(&8*c pow 2+theta pow 2)))∧

(!a.mtoup a=

k a*c pow 2*inv(&8*c pow 2+theta pow 2))∧

(!b.covp nr b=

nr*inv(&m*&n)*sum(1…b)(x.mtoup x)))

定义17中，k(t)表示为机器人邻近的单元格未覆盖数量，mtoup表示移动到未覆盖单元格概率，covp表示区域覆盖率.

为确保机器人完成覆盖任务的相关变量符合机器人区域覆盖模型，需建立由未完成覆盖单元格数、移动到未覆盖单元格概率、机器人区域覆盖率3个变量组成的三元组集合，其形式化表达为定义18.未覆盖单元格数形式化描述为定义19.移动到未覆盖单元格概率形式化描述为定义20.机器人区域覆盖率形式化描述为定义21.

定义18.机器人区域覆盖三元组

|-∀expec c theta nr m n.

move_cover1 nr m n c expec theta=

{k，mtoup，covp | k 1=&8*(&1-nr*inv(&m*&n))∧

k2=&8*(&1-nr*inv(&m*&n))-expec∧

k3=k 2-k 2*&4*inv(&7)*c pow 2*

inv(&8*c pow 2+theta pow 2)-

&8*nr*inv(&m*&n)∧

(!t.3 k t=k(t-1)-inv(&8)*

(k(t-1)*c pow 2*

inv(&8*c pow 2+theta pow 2))*

nr*inv(&m*&n)*sum(1…t-1)

(λj.k j*c pow 2*

inv(&8*c pow 2+theta pow 2)))∧

(!t.mtoup t=k t*c pow 2*

inv(&8*c pow 2+theta pow 2))∧

(!t.covp nr t=

nr*inv(&m*&n)*sum(1…t)(λx.mtoup x))}

定义19.未覆盖单元格数形式化定义

|-∀nr m n c expec theta.

uncover_num nr m n c expec theta=

FST(CHOICE(move_cover1 nr m n c expec theta))

定义20.移动到未覆盖单元格概率形式化定义

|-∀t nr m n c expec theta.

mtoup nr m n c expec t theta=

FST(SND(CHOICE(move_cover1 nr m n c expec theta)))

定义21.区域覆盖率形式化定义

|-∀nr m n c expec theta.

covp nr m n c expec theta=

SND(SND(CHOICE(move_cover1 nr m n c expec theta)))

本文实现了对3时间步长(t=3)内nr个机器人在m×n区域内的覆盖率形式化，如定理11所示.

定理11.区域覆盖率形式化

|-∀nr m n c expec theta.

move_cover nr m n c expec theta

==> covp nr m n c expec theta nr 3=

nr*inv(&m*&n)*

(&24-&32*nr*inv(&m*&n)-

&2*expec-

(&8*(&1-nr*inv(&m*&n))-expec)*

&4*inv(&7)*c pow 2*

inv(&8*c pow 2+theta pow 2))*c pow 2*

inv(&8*c pow 2+theta pow 2)

通过式(8)-式(10)求得3时间步长内nr个机器人在m×n区域内的覆盖率.在定理11的证明过程中，首先重写机器人区域覆盖模型(move_cover)和区域覆盖率(covp)的定义，其次重写CHOICE并结合化简策略SIMP_TAC将目标简化.然后采用策略SELECT_ELIM_TAC消除目标中的任何选择项，结合策略DISCH_THEN(MP_TACoSPECL)将目标前件中条件特殊化；为化简目标，结合策略ANTS_TAC将目标前件的前件拆分成子目标并进行证明，最终实现区域覆盖率形式化，验证了3时间步长(t=3)内nr个机器人在m×n区域内的覆盖率为：

本文对群机器人工作场景、机器人移动概率平均方法、机器人区域覆盖三元组进行了详细的形式化描述并实现了相应的性质验证，证明了整个群机器人区域覆盖模型具有可靠性、完备性，保障了区域覆盖率验证的正确性.

6 总 结

本文以集合库和概率库为基础，对机器人的移动概率和平均移动概率进行了高阶逻辑表达，进一步实现了对机器人区域覆盖算法的建模与验证.本工作难点在于机器人移动概率平均方法形式化和区域覆盖模型的建立.机器人移动概率平均方法形式化关键在于随机变量、事件以及机器人移动概率的表示，构建区域覆盖模型的关键在于机器人邻近的单元格未覆盖数量、机器人移动到未覆盖单元格概率、区域覆盖率3个变量之间复杂的耦合关系的表达.通过建立机器人区域覆盖模型，验证了特定情境下的机器人区域覆盖率，为未来在有障碍物环境下群机器人区域覆盖算法的形式化分析奠定了基础.