協調數百個機器人之間的復雜行為

在2002年大片《少數派報告》中最令人難忘的一幕中，湯姆·克魯斯(Tom Cruise)被迫躲藏在一群蜘蛛狀機器人中，他們搜尋著高聳的公寓大樓。雖然大多數觀眾可能會因小型敏捷獵犬的替代而感到困惑，但計算機工程師可能會對他們優雅的控制系統感到驚訝。

在一個有幾層樓高，有許多房間，數百個障礙物和數千個檢查場所的建筑物中，數十個機器人作為一個有凝聚力的單元移動。他們以搜索模式展開，以徹底檢查整個建筑物，同時拆分任務，以免浪費時間加倍返回自己的路徑或重新檢查其他機器人已經去過的地方。

對于人類控制器而言，這種凝聚力將很難實現，更不用說人工控制器實時計算了。

“如果控制問題在一個只有幾個房間的世界中生活著三到四個機器人，并且如果通過簡單的邏輯規則指定了協作任務，則可以使用最先進的工具來計算出最佳解決方案可以在合理的時間內滿足任務。”杜克大學機械工程與材料科學副教授Mary Milus Yoh和小Harold L. Yoh表示：“ Michael M. Zavlanos

Zavlanos說：“而且，如果您不關心最佳解決方案，則可以在幾分鐘內解決更多房間和更復雜的任務，但機器人頂部仍然只有十幾個。” “除此之外，當前的算法無法克服尋找解決方案的巨大可能性。”

Zavlanos及其最新博士學位于4月29日在線發表在《國際機器人研究雜志》上。研究生Yiannis Kantaros現在是賓夕法尼亞大學的博士后研究員，他提出了一種應對這一挑戰的新方法，稱為STyLuS *，適用于大規模最佳時間邏輯綜合，它可以解決的問題比當前算法所能處理的大得多，其中有數百個機器人，數以萬計的房間和高度復雜的任務，僅需很少的時間。

要了解這種新方法的基礎，必須首先了解線性時態邏輯，它并不像聽起來那樣可怕。假設您要對少數幾個機器人進行編程，以便每天從附近收集郵件并將其發送到郵局。線性時序邏輯是一種記錄完成此任務所需的命令的方式。

例如，這些命令可能包括依次訪問每個房屋，返回郵局，然后等待有人取回收集的郵件，然后再次出發。盡管這可能很容易用英語說出來，但用數學表達起來卻更加困難。線性時間邏輯可以通過使用自己的符號來做到這一點，盡管對于普通觀察者來說，它們看起來像克林貢語，但它們對于表達復雜的控制問題非常有用。

坎塔羅斯說：“使用線性一詞是因為時間點具有基于離散線性時間模型的唯一后繼，而時間是指使用運算符，例如直到，下一個，最終和始終。” “使用這種數學形式主義，我們可以構建復雜的命令，例如'參觀除二號房屋之外的所有房屋'，'依次參觀三號和四號房屋'和'等到你住過一所房屋再到五所房屋。” ”