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

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

1 引 言

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

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

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

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

本文的主要貢獻(xiàn)如下：

1)群機(jī)器人響應(yīng)閾值模型的形式化建模；

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

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

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

2 預(yù)備知識

2.1 HOL-Light

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

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

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

2.2 概率論高階邏輯表達(dá)

在數(shù)學(xué)上，令(Ω，F(xiàn))為可測空間，μ為可測空間上的測度，則稱三元組(Ω，F(xiàn)，μ)為測度空間.μ(Ω)=1的測度空間稱為概率空間，記為(Ω，F(xiàn)，P).其中Ω是一個(gè)集合，稱為樣本空間，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.隨機(jī)變量

|-?X p.

real_random_variable X p<=>

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

在定義5中，X表示隨機(jī)變量，p表示給定的概率空間，real_borel_measurable表示一個(gè)包含所有開集的最小σ代數(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ū)域覆蓋算法

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

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

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

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

1.%初始化

當(dāng)前時(shí)間步pt=0；群機(jī)器人隨機(jī)分布在區(qū)域內(nèi)；

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

repeat

loop i=1…nr

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

檢測鄰近單元格刺激量

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

end loop

pt=pt+1

until pt>t

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

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

3 群機(jī)器人工作場景形式化描述

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

機(jī)器人移動區(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.機(jī)器人移動區(qū)域

|-?m n.

move_area m n=

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

圖1給出了機(jī)器人移動區(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.柵欄邊界非頂點(diǎn)的單元格

|-?m n.

move_area_bound_nonvertex m n=

{x，y |(x=1∧1

(x=m∧1

(y=1∧1

(y=n∧1

2

定義10.柵欄頂點(diǎn)處單元格

|-?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，柵欄邊界非頂點(diǎn)的單元格數(shù)量為(2×(m+n)-4)，柵欄頂點(diǎn)單元格數(shù)量為4，分別形式化描述為定理1、定理2、定理3.

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

|-?m n.

2

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

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

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

|-?m n.

2

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

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

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

|-?m n.

2

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

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

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

(1)

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

定義11.機(jī)器人可移動區(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中的第一個(gè)值x′，SND表示為數(shù)對h中的第二個(gè)值y′.

根據(jù)機(jī)器人所在位置情況不同，執(zhí)行移動操作后，機(jī)器人到達(dá)相鄰單元格分別形式化描述為定義12、定義13、定義14，即柵欄非邊界區(qū)域相鄰的單元格、柵欄邊界非頂點(diǎn)區(qū)域相鄰的單元格、柵欄頂點(diǎn)區(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.柵欄邊界非頂點(diǎn)區(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.柵欄頂點(diǎn)區(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ū)域相鄰的單元格是機(jī)器人在原位置為C區(qū)域上執(zhí)行移動操作之后到達(dá)的位置在HOL-Light中的表示形式.同樣，定義13中的柵欄邊界非頂點(diǎn)區(qū)域相鄰的單元格、定義14中的柵欄頂點(diǎn)區(qū)域相鄰的單元格分別是機(jī)器人在原位置為B區(qū)域、A區(qū)域上執(zhí)行移動操作之后到達(dá)的位置在HOL-Light中的表示形式.

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

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

|-?x y m n.

1

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

定理5.柵欄邊界非頂點(diǎn)區(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.柵欄頂點(diǎn)區(qū)域相鄰的單元格數(shù)量

|-?x y m n.

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

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

4 機(jī)器人移動概率平均方法形式化

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

(2)

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

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

(3)

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

基于以上描述，可實(shí)現(xiàn)對機(jī)器人移動行為的高階邏輯建模.由式(3)可知，描述機(jī)器人移動到相鄰單元格的概率涉及到的變量有機(jī)器人原位置(x，y)、機(jī)器人移動后到達(dá)的位置(x′，y′)、刺激量s以及響應(yīng)閾值θ等.結(jié)合概率論的高階邏輯表達(dá)、機(jī)器人移動區(qū)域及可移動區(qū)域定義，機(jī)器人移動到相鄰單元格的概率形式化模型可用隨機(jī)變量X、樣本空間p、刺激量s、響應(yīng)閾值theta、移動區(qū)域大小m和n表示，見定義16.

定義16.機(jī)器人移動到相鄰單元格的移動概率形

|-?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為定義實(shí)隨機(jī)變量X的概率空間.CHOICEs表示任取集合s中的一個(gè)元素.機(jī)器人執(zhí)行移動操作，從原位置到達(dá)某一個(gè)相鄰的單元格.由于機(jī)器人相鄰的單元格并不唯一，所以用CHOICE任取一相鄰單元格作為機(jī)器人移動后到達(dá)的位置.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ù).

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

(4)

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

(5)

為方便研究，本文設(shè)單元格刺激量為常數(shù)，用c表示，并且機(jī)器人覆蓋區(qū)域內(nèi)無障礙物，不考慮機(jī)器人避障問題.當(dāng)機(jī)器人原位置為柵欄非邊界((1

定理7.機(jī)器人原位置在柵欄非邊界處的移動概率形式化

|-?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證明過程中，首先重寫機(jī)器人移動模型(move_prob_rv)定義，然后結(jié)合假設(shè)列表中的條件引入子目標(biāo)1——事件“當(dāng)機(jī)器人原位置在柵欄非邊界單元格內(nèi)，執(zhí)行移動操作后下一步位置在可移動區(qū)域”在事件集里，在該子目標(biāo)證明成立后，就可以在假設(shè)列表里直接應(yīng)用該條件.然后，引入子目標(biāo)2——當(dāng)前條件下的響應(yīng)函數(shù)值為c2/(8×c2+θ2)，并結(jié)合實(shí)數(shù)庫、集合庫、定理4相關(guān)內(nèi)容實(shí)現(xiàn)子目標(biāo)2的證明.最后，采用策略ASM_SIMP_TAC將假設(shè)列表中的子目標(biāo)2寫入當(dāng)前目標(biāo)并實(shí)現(xiàn)化簡，結(jié)合sum相關(guān)定理完成該目標(biāo)的證明.即實(shí)現(xiàn)機(jī)器人原位置在柵欄非邊界處的移動概率的證明.

機(jī)器人原位置分別為柵欄邊界非頂點(diǎn)處、柵欄邊界頂點(diǎn)處，移動概率的形式化描述如定理8、定理9所示，其證明過程與定理7證明過程相似.

定理8.驗(yàn)證機(jī)器人原位置在柵欄邊界非頂點(diǎn)處的移動概率

|-?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.機(jī)器人原位置在柵欄頂點(diǎn)處的移動概率形式化

|-?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)，機(jī)器人的平均移動概率可形式化描述為定理10.

定理10.機(jī)器人的平均移動概率形式化

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

(6)

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

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

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

(7)

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

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

(8)

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

(9)

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

(10)

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

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

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

定義18.機(jī)器人區(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)))

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

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

6 總 結(jié)

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