群機器人區(qū)域覆蓋算法高階邏輯建模與驗證

尹曉娜，王國輝，施智平，關(guān) 永，張倩穎，張景芝

(高可靠嵌入式系統(tǒng)技術(shù)北京市工程研究中心，首都師范大學信息工程學院，北京100048)

1 引 言

群機器人系統(tǒng)是一個多機器人系統(tǒng)，每個機器人個體按照一定的行為規(guī)則，實現(xiàn)個體之間的交互，從而使整體達到預期的任務目標.在群機器人系統(tǒng)中，每個機器人個體感知搜索區(qū)域中的信息能力是有限的，完成任務目標是大量簡單個體機器人交互的結(jié)果，是一種整體行為的實現(xiàn)，并不依賴于某一個體的主控作用[1，2].因此群機器人系統(tǒng)具有魯棒性、靈活性以及規(guī)?？缮炜s性等特點[3]，可廣泛用于區(qū)域覆蓋的相關(guān)應用如資源勘查[4]、目標搜救[5]以及地形測繪[6]等領(lǐng)域.

群機器人區(qū)域覆蓋是指群機器人系統(tǒng)中的個體通過具有一定感知能力的傳感器探索訪問一定的區(qū)域，利用多個機器人的相互協(xié)作，完成相應任務的過程[7].例如，當?shù)卣鸬茸匀粸暮Πl(fā)生后，可利用群機器人進行探索并對幸存人員進行搜救[8]；當有易燃易爆物品存在、爆炸性或窒息性氣體泄露時，可利用群機器人在事故發(fā)生現(xiàn)場對危險源追蹤檢測[9]；當陸地或海底發(fā)現(xiàn)新資源時，可利用群機器人進行地形測繪.上述任務均具有目標區(qū)域內(nèi)的每個點曾經(jīng)被機器人覆蓋過，但并不需要機器人在目標區(qū)域內(nèi)持續(xù)性覆蓋的特點[10]，因此，通常用非持續(xù)性區(qū)域覆蓋方法[11]來解決.目前，學者主要對非持續(xù)性區(qū)域覆蓋算法和覆蓋率進行研究，如2013年蘭州理工大學的張國有等人[12]采用三元組定義了區(qū)域覆蓋問題.2018年上海海事大學的孫冰等人[14]研究了基于網(wǎng)格圖和神經(jīng)網(wǎng)絡的多AUV(水下自主機器人)完整覆蓋問題.2020年四川大學的石海云[13]分析了現(xiàn)實條件下的多目標檢索問題.上述研究成果主要集中在用傳統(tǒng)計算機仿真和數(shù)值計算方法解決實際問題，其提出的數(shù)學模型尚未得到系統(tǒng)的形式化驗證.

基于傳統(tǒng)計算機仿真技術(shù)的系統(tǒng)分析，是在仿真軟件上對系統(tǒng)設(shè)計模型進行測試.這種方法雖然高效，但在涉及偽隨機數(shù)時，仿真平臺不能保證仿真結(jié)果的準確性[15].基于計算機代數(shù)系統(tǒng)方法在邊界條件的處理上存在短板，可能因其自身的不完整性而不能給出精確的結(jié)果[16，17].和以上傳統(tǒng)方法不同，形式化驗證根據(jù)系統(tǒng)形式規(guī)范或?qū)傩?，使用?shù)學方法證明系統(tǒng)的正確性，對所驗證的性質(zhì)而言是精確和完備的[18].基于定理證明的形式化方法能夠進行精確的系統(tǒng)分析，克服上述仿真方法帶來的局限性.

在區(qū)域覆蓋任務過程中，機器人移動方向的隨機性會影響給定時間內(nèi)的區(qū)域覆蓋率.因此本文基于離散概率分析[19]的方法，在高階邏輯定理證明器HOL-Light中對機器人區(qū)域覆蓋率進行形式化驗證.

本文的主要貢獻如下：

1)群機器人響應閾值模型的形式化建模；

2)群機器人移動概率的形式化描述；

3)機器人區(qū)域覆蓋算法的形式化建模與驗證.

論文組織結(jié)構(gòu)如下：第2節(jié)對高階邏輯定理證明器HOL-Light、概率論高階邏輯表達以及區(qū)域覆蓋算法相關(guān)知識進行簡要介紹；第3節(jié)對機器人移動區(qū)域進行形式化描述；第4節(jié)對群機器人響應閾值模型進行形式化建模，進而實現(xiàn)機器人移動概率和平均移動概率的建模與驗證；第5節(jié)對群機器人區(qū)域覆蓋算法進行形式化建模與驗證；最后總結(jié)全文.

2 預備知識

2.1 HOL-Light

HOL-Light是一種高階邏輯定理證明器.高階邏輯可以形式化描述任何具有邏輯性的系統(tǒng)模型或具有封閉性的數(shù)學表達式.在HOL-Light中，系統(tǒng)驗證過程一般分為3個步驟：1)將系統(tǒng)進行形式化建模；2)將所需驗證的系統(tǒng)屬性形式化為目標任務；3)運用合適的策略和定理驗證目標任務.

目前，HOL-Light中存在較為完整的證明策略和定理庫，例如集合庫、實分析庫、實數(shù)庫等，為本文的工作提供了保證.因此，本文選擇使用定理證明器HOL-Light對機器人區(qū)域覆蓋算法進行形式化建模與驗證.為了更好的理解本文內(nèi)容，表1對定理證明器HOL-Light 中一些常用的符號與函數(shù)進行解釋.

表1 HOL-Light 符號與函數(shù)Table 1 HOL-Light symbols and functions

2.2 概率論高階邏輯表達

在數(shù)學上，令(Ω，F(xiàn))為可測空間，μ為可測空間上的測度，則稱三元組(Ω，F(xiàn)，μ)為測度空間.μ(Ω)=1的測度空間稱為概率空間，記為(Ω，F(xiàn)，P).其中Ω是一個集合，稱為樣本空間，F(xiàn)是Ω的子集族，稱為事件集，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表示一個包含所有開集的最小σ代數(shù).

定義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}關(guān)于映射X的原像.

2.3 區(qū)域覆蓋算法

在群機器人執(zhí)行覆蓋任務時，首先，nr個機器人進入給定的區(qū)域，在單位時間pt內(nèi)每個機器人ri(i=1…nr)檢測自身所在位置和該位置鄰近單元格的刺激量，進而計算響應閾值.然后，機器人根據(jù)響應閾值的結(jié)果確定移動方向并執(zhí)行移動操作.最后，在給定的時間步長t內(nèi)，根據(jù)統(tǒng)計的群機器人覆蓋單元格數(shù)和給定區(qū)域單元格數(shù)量的比值，計算出區(qū)域覆蓋率.算法1給出了區(qū)域覆蓋算法的具體步驟.

算法1.群機器人區(qū)域覆蓋算法

輸入：區(qū)域柵格化后單元格數(shù)量m×n，單元格刺激量s機器人數(shù)量nr，響應閾值θ，時間步t

輸出：區(qū)域覆蓋率

1.%初始化

當前時間步pt=0；群機器人隨機分布在區(qū)域內(nèi)；

2.%群機器人執(zhí)行移動操作

repeat

loop i=1…nr

檢測機器人ri所在單元格(x，y)

檢測鄰近單元格刺激量

根據(jù)響應函數(shù)確定移動到的單元格位置(x′，y′)

end loop

pt=pt+1

until pt>t

3.%計算區(qū)域覆蓋率

統(tǒng)計群機器人覆蓋單元格數(shù)，計算區(qū)域覆蓋率

3 群機器人工作場景形式化描述

在給定區(qū)域內(nèi)，群機器人通過協(xié)作完成區(qū)域覆蓋任務.將機器人所需覆蓋的區(qū)域表示為二維柵格化區(qū)域，區(qū)域大小為m×n(2

機器人移動區(qū)域形式化描述如定義7所示.定義7中 x IN 1…m 表示x在1到m的范圍內(nèi)，即(x I N 1…m)?1≤x∧x≤m，y IN 1…n 表示y在1到n的范圍內(nèi).

定義7.機器人移動區(qū)域

|-?m n.

move_area m n=

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

圖1給出了機器人移動區(qū)域可以劃分的3種情況.柵欄非邊界的單元格((1

圖1 移動區(qū)域柵格圖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

區(qū)域覆蓋率可以用已覆蓋單元格數(shù)量和單元格總數(shù)量的比值表示.因此，區(qū)域覆蓋率的形式化需要用到區(qū)域單元格數(shù)量相關(guān)定理.結(jié)合圖1可知，柵欄非邊界的單元格數(shù)量為(m×n-2(m+n)+4，柵欄邊界非頂點的單元格數(shù)量為(2×(m+n)-4)，柵欄頂點單元格數(shù)量為4，分別形式化描述為定理1、定理2、定理3.

定理1.柵欄非邊界的單元格數(shù)量

|-?m n.

2

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

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

定理2.柵欄邊界非頂點的單元格數(shù)量

|-?m n.

2

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

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

定理3.柵欄頂點數(shù)量

|-?m n.

2

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

定理1-定理3中，CARDs表示集合s中元素的數(shù)量.上述定理的證明思路相似，但復雜度不一.因此，以較為復雜的定理2為例進行介紹.首先，重寫柵欄邊界非頂點的單元格定義將目標展開.然后，采用化簡策略SIMP_TAC以及處理集合運算的相關(guān)定理(如結(jié)合律、分配對偶律等)對目標化簡，并將目標改寫成笛卡爾積的表達形式.最后，利用CARD庫中如CARD_CROSS(表示笛卡爾積表達形式下集合元素的數(shù)量)、CARD_SING(表示單個集合元素的數(shù)量)等相關(guān)定理對目標進行驗證.

機器人執(zhí)行移動操作后所抵達位置情況的數(shù)學表達式如式(1)所示：

(1)

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

定義11.機器人可移動區(qū)域

|-?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…語句用于選擇判斷，可根據(jù)不同條件執(zhí)行不同操作，if P then Q else R表示P成立則Q成立，反之R成立，即(P?Q)∧(P?R).其中，h表示數(shù)對(x′，y′)，F(xiàn)ST表示為數(shù)對h中的第一個值x′，SND表示為數(shù)對h中的第二個值y′.

根據(jù)機器人所在位置情況不同，執(zhí)行移動操作后，機器人到達相鄰單元格分別形式化描述為定義12、定義13、定義14，即柵欄非邊界區(qū)域相鄰的單元格、柵欄邊界非頂點區(qū)域相鄰的單元格、柵欄頂點區(qū)域相鄰的單元格.

定義12.柵欄非邊界區(qū)域相鄰的單元格

|-?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.柵欄邊界非頂點區(qū)域相鄰的單元格

|-?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.柵欄頂點區(qū)域相鄰的單元格

|-?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中的柵欄非邊界區(qū)域相鄰的單元格是機器人在原位置為C區(qū)域上執(zhí)行移動操作之后到達的位置在HOL-Light中的表示形式.同樣，定義13中的柵欄邊界非頂點區(qū)域相鄰的單元格、定義14中的柵欄頂點區(qū)域相鄰的單元格分別是機器人在原位置為B區(qū)域、A區(qū)域上執(zhí)行移動操作之后到達的位置在HOL-Light中的表示形式.

群機器人的移動概率與機器人執(zhí)行移動操作之后可能到達位置的個數(shù)有關(guān)，因此將柵欄非邊界區(qū)域、邊界非頂點區(qū)域、頂點區(qū)域相鄰的單元格數(shù)量分別形式化描述為定理4、定理5、定理6.

定理4.柵欄非邊界區(qū)域相鄰的單元格數(shù)量

|-?x y m n.

1

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

定理5.柵欄邊界非頂點區(qū)域相鄰的單元格數(shù)

|-?x y m n.

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

(y=1∨y=n)∧1

2

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

定理6.柵欄頂點區(qū)域相鄰的單元格數(shù)量

|-?x y m n.

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

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

4 機器人移動概率平均方法形式化

機器人具有一定的感知能力.在區(qū)域移動過程中，機器人將感知的周圍環(huán)境的信息作為輸入信號，這些輸入信號稱為刺激量，影響機器人執(zhí)行移動操作的決策.機器人具有獨立的響應閾值θ，每個單元格具有一個刺激量s，機器人選擇下一單元格的概率由響應函數(shù)決定，響應函數(shù)如式(2)所示:

(2)

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

定義15.響應函數(shù)

|-?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是響應函數(shù)在HOL-Light中的表示.根據(jù)對機器人移動操作分析，機器人從t時刻的位置到達t+1時刻的位置，到達位置并不能確定.依據(jù)區(qū)域覆蓋算法，在給定區(qū)域內(nèi)，機器人執(zhí)行移動操作，移動到相鄰單元格具有一定的概率，如式(3)所示:

(3)

其中，(x，y)∈A∩B∩C(A、B、C為圖1給定區(qū)域).

基于以上描述，可實現(xiàn)對機器人移動行為的高階邏輯建模.由式(3)可知，描述機器人移動到相鄰單元格的概率涉及到的變量有機器人原位置(x，y)、機器人移動后到達的位置(x′，y′)、刺激量s以及響應閾值θ等.結(jié)合概率論的高階邏輯表達、機器人移動區(qū)域及可移動區(qū)域定義，機器人移動到相鄰單元格的概率形式化模型可用隨機變量X、樣本空間p、刺激量s、響應閾值theta、移動區(qū)域大小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中的一個元素.機器人執(zhí)行移動操作，從原位置到達某一個相鄰的單元格.由于機器人相鄰的單元格并不唯一，所以用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))為概率函數(shù).

機器人從不同位置移動到相鄰單元格的概率的數(shù)學表達式如式(4)所示：

(4)

基于上式，在給定區(qū)域內(nèi)機器人移動到某一鄰近單元格的平均概率為：

(5)

為方便研究，本文設(shè)單元格刺激量為常數(shù)，用c表示，并且機器人覆蓋區(qū)域內(nèi)無障礙物，不考慮機器人避障問題.當機器人原位置為柵欄非邊界((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)定義，然后結(jié)合假設(shè)列表中的條件引入子目標1——事件“當機器人原位置在柵欄非邊界單元格內(nèi)，執(zhí)行移動操作后下一步位置在可移動區(qū)域”在事件集里，在該子目標證明成立后，就可以在假設(shè)列表里直接應用該條件.然后，引入子目標2——當前條件下的響應函數(shù)值為c2/(8×c2+θ2)，并結(jié)合實數(shù)庫、集合庫、定理4相關(guān)內(nèi)容實現(xiàn)子目標2的證明.最后，采用策略ASM_SIMP_TAC將假設(shè)列表中的子目標2寫入當前目標并實現(xiàn)化簡，結(jié)合sum相關(guān)定理完成該目標的證明.即實現(xiàn)機器人原位置在柵欄非邊界處的移動概率的證明.

機器人原位置分別為柵欄邊界非頂點處、柵欄邊界頂點處，移動概率的形式化描述如定理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)

根據(jù)式(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)的定義，結(jié)合重寫策略REWRITE_TAC化簡目標.然后引入3個子目標分別驗證機器人原位置在柵欄非邊界處、在柵欄邊界非頂點處、頂點處的移動概率.最后結(jié)合集合庫、實分析庫相關(guān)定理和策略完成定理10的證明，驗證了機器人的平均移動概率如式(6)所示:

(6)

5 機器人區(qū)域覆蓋率形式化建模與驗證

區(qū)域覆蓋任務的完成與刺激量、響應閾值、機器人移動區(qū)域大小、機器人數(shù)量等變量相關(guān).機器人覆蓋率如式(7)所示：

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

(7)

Cover表示覆蓋率，θ表示響應閾值，s表示刺激量，Na表示單元格數(shù)量，t表示為時間.

事實上機器人移動概率包含兩種可能性，一種是移動到未覆蓋單元格，另一種是移動到已覆蓋單元格.機器人移動到未覆蓋單元格概率Pu(t)數(shù)學表示形式為：

(8)

在式(8)中，k(t)表示為機器人鄰近單元格未覆蓋數(shù)量，其數(shù)學表示為：

(9)

機器人在t時間步內(nèi)區(qū)域覆蓋率為：

(10)

根據(jù)上述描述可知，機器人鄰近單元格未覆蓋數(shù)量、機器人移動到未覆蓋單元格概率、區(qū)域覆蓋率3個變量之間存在較為復雜的耦合關(guān)系，在HOL-Light中無法對這3個變量進行解耦并給出相應的直接表示.因此，本文對涵蓋這3個變量的完整區(qū)域覆蓋算法模型形式化為定義17.

定義17.機器人的區(qū)域覆蓋模型定義

|-?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)表示為機器人鄰近的單元格未覆蓋數(shù)量，mtoup表示移動到未覆蓋單元格概率，covp表示區(qū)域覆蓋率.

為確保機器人完成覆蓋任務的相關(guān)變量符合機器人區(qū)域覆蓋模型，需建立由未完成覆蓋單元格數(shù)、移動到未覆蓋單元格概率、機器人區(qū)域覆蓋率3個變量組成的三元組集合，其形式化表達為定義18.未覆蓋單元格數(shù)形式化描述為定義19.移動到未覆蓋單元格概率形式化描述為定義20.機器人區(qū)域覆蓋率形式化描述為定義21.

定義18.機器人區(qū)域覆蓋三元組

|-?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.未覆蓋單元格數(shù)形式化定義

|-?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.區(qū)域覆蓋率形式化定義

|-?nr m n c expec theta.

covp nr m n c expec theta=

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

本文實現(xiàn)了對3時間步長(t=3)內(nèi)nr個機器人在m×n區(qū)域內(nèi)的覆蓋率形式化，如定理11所示.

定理11.區(qū)域覆蓋率形式化

|-?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時間步長內(nèi)nr個機器人在m×n區(qū)域內(nèi)的覆蓋率.在定理11的證明過程中，首先重寫機器人區(qū)域覆蓋模型(move_cover)和區(qū)域覆蓋率(covp)的定義，其次重寫CHOICE并結(jié)合化簡策略SIMP_TAC將目標簡化.然后采用策略SELECT_ELIM_TAC消除目標中的任何選擇項，結(jié)合策略DISCH_THEN(MP_TACoSPECL)將目標前件中條件特殊化；為化簡目標，結(jié)合策略ANTS_TAC將目標前件的前件拆分成子目標并進行證明，最終實現(xiàn)區(qū)域覆蓋率形式化，驗證了3時間步長(t=3)內(nèi)nr個機器人在m×n區(qū)域內(nèi)的覆蓋率為：

本文對群機器人工作場景、機器人移動概率平均方法、機器人區(qū)域覆蓋三元組進行了詳細的形式化描述并實現(xiàn)了相應的性質(zhì)驗證，證明了整個群機器人區(qū)域覆蓋模型具有可靠性、完備性，保障了區(qū)域覆蓋率驗證的正確性.

6 總 結(jié)

本文以集合庫和概率庫為基礎(chǔ)，對機器人的移動概率和平均移動概率進行了高階邏輯表達，進一步實現(xiàn)了對機器人區(qū)域覆蓋算法的建模與驗證.本工作難點在于機器人移動概率平均方法形式化和區(qū)域覆蓋模型的建立.機器人移動概率平均方法形式化關(guān)鍵在于隨機變量、事件以及機器人移動概率的表示，構(gòu)建區(qū)域覆蓋模型的關(guān)鍵在于機器人鄰近的單元格未覆蓋數(shù)量、機器人移動到未覆蓋單元格概率、區(qū)域覆蓋率3個變量之間復雜的耦合關(guān)系的表達.通過建立機器人區(qū)域覆蓋模型，驗證了特定情境下的機器人區(qū)域覆蓋率，為未來在有障礙物環(huán)境下群機器人區(qū)域覆蓋算法的形式化分析奠定了基礎(chǔ).