多自主機(jī)器人協(xié)作及群體行為分析

一直以來(lái)，多自主機(jī)器人協(xié)作都是機(jī)器人學(xué)中的一個(gè)研究熱點(diǎn)，以往的方法在優(yōu)化效率和自適應(yīng)性方面存在著很多亟待解決的問(wèn)題。最近，費(fèi)耶特維爾州立大學(xué)數(shù)學(xué)與計(jì)算機(jī)科學(xué)系，華沙理工大學(xué)計(jì)算機(jī)科學(xué)研究所的科學(xué)家們，對(duì)多自主機(jī)器人協(xié)作及群體行為進(jìn)行了研究，提出了使用機(jī)器人行為劃分的全新方法，在室內(nèi)環(huán)境下對(duì)機(jī)器人的行為進(jìn)行研究，并提出了驗(yàn)證和分析組合機(jī)器人行為的技術(shù)。

在本文中，我們對(duì)以往有關(guān)協(xié)作自主機(jī)器人的研究進(jìn)行了擴(kuò)展，將環(huán)境變化和群體中機(jī)器人數(shù)量的變化會(huì)影響分配給機(jī)器人群體的任務(wù)執(zhí)行效率的情況，納入了研究之中。我們提出了一種全新的基于機(jī)器人行為劃分的方法，描述子路徑的子圖使得我們能夠使用有限數(shù)量的狀態(tài)組合對(duì)自主機(jī)器人之間的高級(jí)交互進(jìn)行建模，避免可達(dá)性組合爆炸（combinatorial explosion）。我們對(duì)可以確保機(jī)器人交互正確性的系統(tǒng)進(jìn)行了確認(rèn)，提出了驗(yàn)證和分析組合機(jī)器人行為的新技術(shù)。通過(guò)分區(qū)圖，我們可以對(duì)自主機(jī)器人之間的高級(jí)交互進(jìn)行建模，并檢測(cè)出諸如死鎖（deadlock）、缺少終止（lack of termination）等異常情況。我們提出了使用模型檢驗(yàn)方法對(duì)組合機(jī)器人行為進(jìn)行驗(yàn)證和分析的技術(shù)。文中所描述的系統(tǒng)Dedan驗(yàn)證器仍處于開(kāi)發(fā)階段。在不久的將來(lái)，計(jì)劃進(jìn)行定時(shí)和概率驗(yàn)證。

介紹

如今，群體自主移動(dòng)設(shè)備（機(jī)器人）的應(yīng)用范圍越來(lái)越廣，這與它們對(duì)個(gè)體機(jī)器人的故障/碰撞和環(huán)境變化作出適當(dāng)響應(yīng)的自然能力有關(guān)。這種協(xié)作自主機(jī)器人系統(tǒng)可以應(yīng)用于諸如軍事偵察、監(jiān)視和警戒系統(tǒng)等多個(gè)領(lǐng)域，因此它們的開(kāi)發(fā)應(yīng)該得到高度重視。實(shí)際上，群體機(jī)器人的研究面臨著諸多挑戰(zhàn)。我們可以針對(duì)有限數(shù)量的機(jī)器人分析多個(gè)自主機(jī)器人之間的協(xié)作，但想要進(jìn)一步擴(kuò)展更多的解決方案則是一個(gè)需要新技術(shù)的領(lǐng)域。在本文中，我們專(zhuān)注于研究基于分區(qū)行為算法的群體機(jī)器人的彈性協(xié)作問(wèn)題。我們的內(nèi)容涵蓋了自主性局部和全部死鎖檢測(cè)技術(shù)，以及自主性局部和全部分布式終端的必然性檢測(cè)技術(shù)。在本文中，我們?cè)噲D回答以下若干研究問(wèn)題：

（1）狀態(tài)圖是如何用于有效地描述大量機(jī)器人的？

（2）我們可以在多大程度上對(duì)解決方案進(jìn)行擴(kuò)展，以在考慮分布式中止和避免死鎖的情況下，保證群體機(jī)器人能夠進(jìn)行適當(dāng)?shù)膮f(xié)作。

（3）我們可以在多大程度上對(duì)解決方案進(jìn)行擴(kuò)展，以在考慮任務(wù)目標(biāo)（如區(qū)域覆蓋范圍、每個(gè)受保護(hù)地點(diǎn)的檢測(cè)頻率等）的情況下，保證群體機(jī)器人能夠進(jìn)行適當(dāng)?shù)膮f(xié)作。

（4）我們可以在多大程度上對(duì)解決方案進(jìn)行擴(kuò)展，以在我們充分響應(yīng)個(gè)體機(jī)器人的故障/碰撞和環(huán)境變化時(shí)，保證群體機(jī)器人能夠進(jìn)行適當(dāng)?shù)膮f(xié)作。

（5）自主移動(dòng)平臺(tái)協(xié)作正確性的實(shí)時(shí)驗(yàn)證可行性如何？

在本文中，我們專(zhuān)注于研究室內(nèi)環(huán)境中自主機(jī)器人的導(dǎo)航問(wèn)題。我們假設(shè)機(jī)器人不僅可以直接對(duì)環(huán)境做出響應(yīng)，還可以對(duì)其他機(jī)器人的動(dòng)作做出響應(yīng)。狀態(tài)圖以前往往用于描述機(jī)器人的行為，通常情況下，可以基于諸如此類(lèi)的模型手動(dòng)開(kāi)發(fā)適當(dāng)?shù)能浖?。為了加速開(kāi)發(fā)過(guò)程，我們創(chuàng)建了一個(gè)新的工具，以用于機(jī)器人行為的設(shè)計(jì)和驗(yàn)證。這種工具對(duì)于機(jī)器人反應(yīng)行為的快速修正非常有用，因?yàn)樗试S開(kāi)發(fā)人員逐步地修正設(shè)計(jì)。此外，該工具的功能能夠自動(dòng)生成機(jī)器人行為以響應(yīng)不斷變化的要求。

在本文中，我們描述了分析傳統(tǒng)狀態(tài)圖的技術(shù)，并對(duì)其進(jìn)行修正，使其更適合于群體機(jī)器人以及大量此類(lèi)狀態(tài)圖的集成。狀態(tài)圖使得我們可以對(duì)自主機(jī)器人群體之間的高級(jí)交互進(jìn)行建模，并且可以確保機(jī)器人交互的正確性。當(dāng)需要對(duì)機(jī)器人行為進(jìn)行快速修正時(shí)，對(duì)機(jī)器人之間的交互進(jìn)行快速檢查是至關(guān)重要的。狀態(tài)圖的模型檢查方法可以識(shí)別諸如死鎖或活鎖（live-lock）之類(lèi)的問(wèn)題，從而為機(jī)器人設(shè)計(jì)人員提供了一套即用型算法和技術(shù)，用于分析基于完整群體的系統(tǒng)屬性。

通過(guò)CTL時(shí)間公式AG EX true（對(duì)于任何一個(gè)狀態(tài)來(lái)說(shuō)，都存在下一個(gè)狀態(tài)）檢查出無(wú)死鎖（deadlock freeness）。然而，局部死鎖卻不那么容易被識(shí)別出來(lái)，因此我們提出了許多用于在具有特定形狀的系統(tǒng)中進(jìn)行自動(dòng)死鎖檢測(cè)的方法。

在分布式系統(tǒng)的分析中，可以觀察到兩種進(jìn)程中止：不合時(shí)宜的進(jìn)程缺失（死鎖），這是一個(gè)錯(cuò)誤;被稱(chēng)之為進(jìn)程終止的預(yù)期停止。死鎖檢測(cè)和終止檢測(cè)方法必須能夠區(qū)分兩種中斷的區(qū)別，或者只是簡(jiǎn)單地禁止其中一種。然而，完全終止似乎也是類(lèi)似的情況：不存在未來(lái)。在循環(huán)系統(tǒng)中，我們不期望存在終止，公式AG EX true能夠識(shí)別出死鎖。這就是為什么許多死鎖檢測(cè)技術(shù)只針對(duì)無(wú)限循環(huán)系統(tǒng)（停止是一個(gè)死鎖）。

在終端系統(tǒng)中，應(yīng)將總死鎖與總終止區(qū)分開(kāi)來(lái)。實(shí)際上，各種分布式終止檢測(cè)技術(shù)都在迅速發(fā)展，這些方法大都基于對(duì)分布式進(jìn)程的某些特征的觀察或?qū)ο⒘髁康目刂?。有時(shí)，分布式進(jìn)程的特殊元素被定義用于終止檢測(cè)。

與死鎖檢測(cè)一樣，終止檢測(cè)的動(dòng)態(tài)（運(yùn)行時(shí)）方法需要系統(tǒng)的一些測(cè)試。它通常發(fā)送一些消息，報(bào)告各個(gè)進(jìn)程的狀態(tài)，以及將它們組合成分布式終止的全局決策的機(jī)制。在測(cè)試、處理失敗的進(jìn)程或鏈接失敗、接受臨時(shí)網(wǎng)絡(luò)劃分方面存在不同的方法。靜態(tài)終止檢測(cè)方法是基于對(duì)單個(gè)進(jìn)程終端狀態(tài)的觀察，模型檢查技術(shù)適用于此目的，使用模型特定公式或通用公式。計(jì)數(shù)智能體的結(jié)構(gòu)可以進(jìn)行動(dòng)態(tài)的和靜態(tài)的應(yīng)用。轉(zhuǎn)換不變量使得我們能夠檢查在初始狀態(tài)下開(kāi)始的每個(gè)執(zhí)行是否是有限的。

我們的方法是基于對(duì)分布式系統(tǒng)規(guī)范中的終止動(dòng)作進(jìn)行區(qū)分。

環(huán)境資源

從機(jī)器人程序員的角度來(lái)看，了解機(jī)器人將要經(jīng)過(guò)的環(huán)境類(lèi)型是非常重要的。一般來(lái)說(shuō)，環(huán)境可以是已知的，也可以是未知的。在本文中，我們將集中描述機(jī)器人在已知環(huán)境中的行為。已知的環(huán)境通常通過(guò)一張地圖進(jìn)行描述，地圖上標(biāo)注了建筑物的所有部分，我們將其稱(chēng)為房間，房間之間的開(kāi)口，我們將其簡(jiǎn)稱(chēng)為門(mén)。建筑結(jié)構(gòu)的簡(jiǎn)單表示之一可以是一個(gè)圖形，其以節(jié)點(diǎn)形式顯示所有可訪(fǎng)問(wèn)的位置，并以指定訪(fǎng)問(wèn)房間順序的圖路徑形式顯示到達(dá)這些位置的方法。

任何以圖形形式出現(xiàn)的拓?fù)鋱D也可以作為環(huán)境資源圖表進(jìn)行說(shuō)明。這意味著圖形的每個(gè)節(jié)點(diǎn)也可以被解釋為資源，并且當(dāng)機(jī)器人位置與該節(jié)點(diǎn)相關(guān)聯(lián)時(shí)，我們可以宣稱(chēng)機(jī)器人獲得了這個(gè)資源。當(dāng)機(jī)器人離開(kāi)節(jié)點(diǎn)時(shí)，我們聲稱(chēng)它釋放了資源。兩個(gè)節(jié)點(diǎn)之間的鏈接也可以解釋為可以獲取和釋放的資源。對(duì)拓?fù)鋱D的這種解釋使得我們可以將已知的資源分配算法應(yīng)用于多個(gè)機(jī)器人行為的描述，并隨后將其擴(kuò)展到機(jī)器人群體中。

考慮圖1中所示的拓?fù)鋱D，它顯示了若干個(gè)房間，且房間與房間之間有門(mén)。前綴A表示側(cè)間，而前綴Q表示在機(jī)器人操作期間可能發(fā)生沖突的中央房間。房間的名稱(chēng)取自于基本方向。我們假設(shè)任何時(shí)候一個(gè)機(jī)器人可能出現(xiàn)在典型的房間QNW、QNE、QSW和QSE內(nèi)，同時(shí)還有側(cè)間AW、AN、AE和AS，使得多個(gè)機(jī)器人可以進(jìn)行共同定位。我們還假設(shè)每個(gè)中央房間QNW、QNE、QSW和QSE都具有通往其他兩個(gè)中央房間的開(kāi)口，和通往其他兩個(gè)側(cè)間的門(mén)/開(kāi)口。

用于群體機(jī)器人導(dǎo)航的快速生成狀態(tài)圖的實(shí)用程序

在以往的研究成果中，對(duì)確定性狀態(tài)圖進(jìn)行了很好的描述。通常來(lái)說(shuō)，確定性狀態(tài)圖除了狀態(tài)之外，還具有由觸發(fā)器和動(dòng)作組成的轉(zhuǎn)換，觸發(fā)器會(huì)導(dǎo)致機(jī)器人從一個(gè)狀態(tài)轉(zhuǎn)換到另一個(gè)狀態(tài)，而動(dòng)作會(huì)在轉(zhuǎn)換過(guò)程中被觸發(fā)。觸發(fā)器由連續(xù)計(jì)算評(píng)估的布爾條件表示，以響應(yīng)環(huán)境的變化。

為了指定狀態(tài)圖，我們使用基于通用建模語(yǔ)言（Universal Modeling Language，UML）的符號(hào)，其中狀態(tài)由方框表示，轉(zhuǎn)換由帶有標(biāo)簽的箭頭指示。轉(zhuǎn)換標(biāo)簽的第一部分（在斜杠的前面）指定觸發(fā)器，斜杠后面的部分指定在轉(zhuǎn)換期間要調(diào)用的動(dòng)作（或消息）。概率規(guī)范的語(yǔ)法被描述為另外的第三個(gè)組成部分，用于指定整個(gè)轉(zhuǎn)換的概率。

由于多種原因，顯式依賴(lài)于位置的狀態(tài)圖可以便捷地指定機(jī)器人行為。首先，該圖可以通過(guò)相對(duì)簡(jiǎn)單的環(huán)境資源圖的轉(zhuǎn)換進(jìn)行構(gòu)建。其次，可以相對(duì)容易地添加概率組合。最后，協(xié)作機(jī)器人的行為可以通過(guò)并發(fā)性狀態(tài)圖進(jìn)行描述，并且所有成熟的用于并發(fā)性程序分析的技術(shù)都可以使用，即死鎖檢測(cè)或死鎖避免算法。并發(fā)性分析可以自動(dòng)完成，機(jī)器人程序可以直接從狀態(tài)圖模型生成。

基于環(huán)境圖和相應(yīng)的環(huán)境觸發(fā)器，我們可以快速指定各種位置相關(guān)的狀態(tài)圖。使用自主機(jī)器人，我們可以對(duì)它們的行為進(jìn)行規(guī)劃，指定它們遵循的通用規(guī)則。規(guī)則可以給定機(jī)器人的目標(biāo)房間，在圖2中，從AS開(kāi)始的機(jī)器人可以被引導(dǎo)到最終回到AS的AW、AN、AE側(cè)室中，并訪(fǎng)問(wèn)路線(xiàn)上的中央房間。一組路線(xiàn)可以彼此獨(dú)立，如在圖2中，具有4個(gè)巡邏機(jī)器人的系統(tǒng)中，它們的方向總是向右的。

對(duì)于機(jī)器人，我們考慮行為A描述圖2中右側(cè)ROBOT1移動(dòng)的簡(jiǎn)單路徑：從特殊的側(cè)間AE開(kāi)始，然后沿著通向QNE的門(mén)，再繼續(xù)直到進(jìn)入AN并停止。

為了對(duì)這種行為進(jìn)行建模，可以使用狀態(tài)圖模型。一般來(lái)說(shuō)，我們可以使用多層模型，但在本文中為了簡(jiǎn)化表示，我們假設(shè)使用兩層模型。上層模型是通過(guò)變換環(huán)境圖獲得的，即，將非定向邊轉(zhuǎn)換為有向邊，并提供必要的觸發(fā)器、動(dòng)作和消息。

更確切地說(shuō)，兩個(gè)節(jié)點(diǎn)（例如AN和QNE）之間的鏈接可以進(jìn)行如下解釋?zhuān)喝绻麢C(jī)器人被分配了資源AN，則它應(yīng)該首先在釋放資源AN之前獲取資源QNE。圖2中所示的狀態(tài)圖詳細(xì)地指定了ROBOT1的行為A。類(lèi)似地，可以相應(yīng)地描述機(jī)器人2、3和4的行為。

為了正式指定如圖2所示的說(shuō)法，我們需要拓?fù)湫宰R(shí)別觸發(fā)器、拓?fù)鋭?dòng)作和同步消息按此順序?qū)λ鼈冞M(jìn)行描述。這些拓?fù)浣Y(jié)構(gòu)中的每一個(gè)都可以由較低級(jí)別的圖進(jìn)行定義。

不同的拓?fù)湮恢?，即不同的資源，通常會(huì)對(duì)機(jī)器人的傳感器產(chǎn)生不同的值。傳感器信號(hào)處理算法，即，將描述機(jī)器人傳感器信號(hào)轉(zhuǎn)換成可用于直接識(shí)別環(huán)境的高電平信號(hào)的算法。我們將假設(shè)較低級(jí)別的狀態(tài)圖可以描述這種算法，并且我們將這些信號(hào)稱(chēng)為供更高級(jí)別圖表使用的環(huán)境觸發(fā)器（environment trigger）。

多個(gè)自主機(jī)器人之間的協(xié)作

接下來(lái)，我們將討論自主機(jī)器人之間的協(xié)作。有許多理論和實(shí)踐解決方案可供考慮。

模型檢查提供了一種最為通用的方法，不僅可用于避免死鎖或檢測(cè)，還可以用于檢測(cè)和驗(yàn)證各種進(jìn)程協(xié)作特性。通常情況下，模型檢查是基于有限狀態(tài)方法的，以便可以直接應(yīng)用于我們的狀態(tài)圖。因此，對(duì)于一些機(jī)器人行為的驗(yàn)證具有重要的實(shí)用價(jià)值。遺憾的是，對(duì)于所描述的異步和概率模型，傳統(tǒng)的模型檢查方法不能提供一組即用型算法和技術(shù)來(lái)分析多個(gè)機(jī)器人系統(tǒng)的屬性。

使用現(xiàn)有的時(shí)間驗(yàn)證器如Spin、NuSMV或Uppaal，可以很容易地證明無(wú)死鎖性。然而，為了更為有效的機(jī)器人合作，我們需要更多細(xì)微的功能。例如，局部死鎖是危險(xiǎn)的，因?yàn)樵谶@種情況下，一些機(jī)器人繼續(xù)工作，但其中一些機(jī)器人卡住了，無(wú)法取得任何進(jìn)展。所提到的任何一種通用模型檢查器都不能自動(dòng)發(fā)現(xiàn)局部死鎖，用戶(hù)必須根據(jù)已驗(yàn)證系統(tǒng)的特征自行指定此功能。

從上文所進(jìn)行的描述以及圖1中所預(yù)先給出的拓?fù)鋱D可以知道，一組路線(xiàn)是可以彼此獨(dú)立的，如在圖2中，在具有4個(gè)巡邏機(jī)器人的系統(tǒng)中，它們的方向總是向右的。然而，如圖5所示，路徑可能會(huì)發(fā)生干擾。如果房間QNW、QNE、QSW和QSE被占用，則會(huì)發(fā)生明顯的總死鎖。我們可以使用防止死鎖的路由來(lái)避免這種死鎖，例如，只允許從AW和AN開(kāi)始的兩個(gè)機(jī)器人（如圖6所示）進(jìn)行一些選定的轉(zhuǎn)換。而從AS和AE開(kāi)始的其他機(jī)器人則保留了完全的選擇自由，如圖7所示。

在本文中，我們將以往關(guān)于協(xié)作自主機(jī)器人的研究擴(kuò)展到室內(nèi)環(huán)境中，提出了一種使用機(jī)器人行為劃分的新方法。描述機(jī)器人行為的子圖使得我們能夠基于有限數(shù)量的狀態(tài)組合對(duì)自主機(jī)器人之間的高級(jí)交互進(jìn)行建模，從而避免狀態(tài)爆炸。我們確定了可以確保機(jī)器人交互正確性的系統(tǒng)，并提出了驗(yàn)證和分析組合機(jī)器人行為的技術(shù)。

Dedan驗(yàn)證環(huán)境使用模型檢查技術(shù)，以用于查找部分以及全部的通信死鎖和資源死鎖。此外，同時(shí)，還進(jìn)行自動(dòng)驗(yàn)證分布式終端。除此之外，系統(tǒng)可以自動(dòng)從服務(wù)器視圖轉(zhuǎn)換到智能體視圖，可以觀察和模擬系統(tǒng)的狀態(tài)空間，并且系統(tǒng)可以轉(zhuǎn)換為Promela（旋轉(zhuǎn)驗(yàn)證器輸入形式）和Uppaal。在系統(tǒng)中，我們可以使用經(jīng)過(guò)驗(yàn)證的系統(tǒng)表征的圖形形式，并支持對(duì)組件服務(wù)器/智能體的圖形仿真。目前，我們所描述的系統(tǒng)仍在開(kāi)發(fā)中，在不久的將來(lái)，我們會(huì)將自身用于非窮舉部分死鎖研究的算法納入研究之中。分布式自動(dòng)機(jī)的新概念正在開(kāi)發(fā)中，使用計(jì)時(shí)自動(dòng)機(jī)（以驗(yàn)證實(shí)時(shí)依賴(lài)性）和概率模型檢查，將提供更高級(jí)的驗(yàn)證形式，最先進(jìn)的功能之一將是能夠進(jìn)行自動(dòng)或半自動(dòng)行為修改，而這將顯著改善協(xié)作自主機(jī)器人的動(dòng)態(tài)彈性。