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

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

介紹

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

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

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

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

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

（5）自主移動平臺協(xié)作正確性的實時驗證可行性如何？

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

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

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

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

在終端系統(tǒng)中，應將總死鎖與總終止區(qū)分開來。實際上，各種分布式終止檢測技術都在迅速發(fā)展，這些方法大都基于對分布式進程的某些特征的觀察或對消息流量的控制。有時，分布式進程的特殊元素被定義用于終止檢測。

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

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

環(huán)境資源

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

任何以圖形形式出現(xiàn)的拓撲圖也可以作為環(huán)境資源圖表進行說明。這意味著圖形的每個節(jié)點也可以被解釋為資源，并且當機器人位置與該節(jié)點相關聯(lián)時，我們可以宣稱機器人獲得了這個資源。當機器人離開節(jié)點時，我們聲稱它釋放了資源。兩個節(jié)點之間的鏈接也可以解釋為可以獲取和釋放的資源。對拓撲圖的這種解釋使得我們可以將已知的資源分配算法應用于多個機器人行為的描述，并隨后將其擴展到機器人群體中。

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

用于群體機器人導航的快速生成狀態(tài)圖的實用程序

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

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

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

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

對于機器人，我們考慮行為A描述圖2中右側ROBOT1移動的簡單路徑：從特殊的側間AE開始，然后沿著通向QNE的門，再繼續(xù)直到進入AN并停止。

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

更確切地說，兩個節(jié)點（例如AN和QNE）之間的鏈接可以進行如下解釋：如果機器人被分配了資源AN，則它應該首先在釋放資源AN之前獲取資源QNE。圖2中所示的狀態(tài)圖詳細地指定了ROBOT1的行為A。類似地，可以相應地描述機器人2、3和4的行為。

為了正式指定如圖2所示的說法，我們需要拓撲性識別觸發(fā)器、拓撲動作和同步消息按此順序對它們進行描述。這些拓撲結構中的每一個都可以由較低級別的圖進行定義。

不同的拓撲位置，即不同的資源，通常會對機器人的傳感器產生不同的值。傳感器信號處理算法，即，將描述機器人傳感器信號轉換成可用于直接識別環(huán)境的高電平信號的算法。我們將假設較低級別的狀態(tài)圖可以描述這種算法，并且我們將這些信號稱為供更高級別圖表使用的環(huán)境觸發(fā)器（environment trigger）。

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

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

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

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

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

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

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