隨著AI技術的發展，自主智能體在速度和精確度方面有了很大的提升，變得更加智能和高效，展現出在各種具體任務上的令人印象深刻的性能，并成功地互相協作，實現了自己的獨立目標。在本文中，俄羅斯Innopolis大學機器人研究所的Konstantin Danilov、Ruslan Rezin、Alexander Kolotov和Ilya Afanasyev教授提出了一種分散式交易市場的概念，可將其稱之為“機器人經濟學（robonomics）”。

在這種市場中，自主智能體可以根據共識協議消費和生產服務。那么，在這種市場中，客戶如何根據服務提供商執行責任的程度獲取對他們的信任程度？又或者如何檢測服務提供商沒能夠正確執行責任從而中止支付交易呢？ 對此，專家們給出了新的答案。

一般來說，分散式交易市場方法（decentralized trading market approach），即自主的智能體和人員都可以消費和生產服務，以擴大自己實現目標的機會，這作為第四次工業革命的一部分，看起來很有發展前景。

該方法的關鍵組成部分是區塊鏈平臺（blockchain platform），該平臺使得智能體之間通過責任智能合約（liability smart contract）進行交互。服務提供者的可靠性通常取決于聲譽模型（reputation model）。然而，這種解決方案只會警醒未來的客戶對服務提供商的信任程度，以防它無法正確執行任何以前的責任。

另一方面，區塊鏈共識協議（blockchain consensus protocol）還可以包含一個驗證程序，用于檢測不正確的責任執行情況，以便暫停向有問題的服務提供者的支付交易。本文提出了一種對于分散式交易市場中基于智能體的服務提供者的責任執行驗證方法，該方法使用了基于有限狀態自動機（finite state automata）的數學模型和有用的時間邏輯屬性（Temporal Logic property）的模型檢測方法（Model Checking method）。

為了說明這個概念，我們在Duckietown應用程序中實施了這個方法：移動一個自主的移動機器人，并使用在一個完整場景結束時所進行的接下來的行為驗證（behavior validation）實現一個任務目標。

圖1：在責任生命周期中自主智能體之間進行交互的通用方案。

在過去的十年中，自主智能體在速度和精確度方面變得更加智能和高效，展現出在各種具體任務上的令人印象深刻的性能，并成功地互相協作，實現了自己的獨立目標。這就提出了分散式交易市場的概念，在這種市場中，自主智能體可以根據共識協議消費和生產服務。

由于區塊鏈技術的出現，特別是解決了雙重支出攻擊問題（double-spending attack problem）的比特幣的實現（Bitcoin），分散式的多智能體系統概念開始變得可行，只要智能體不依賴于單點故障，并且它們的操作對于監控而言是透明的。

雖然區塊鏈最初是作為加密貨幣的解決方案引入的，但它啟發了以太坊平臺（Ethereum platform）的開發人員提出了一個新的概念：智能合約——一種協議的算法執行。很快，它成為了分散式應用程序的最大平臺，為銷售計算機的處理能力和分散式計算存儲等市場服務的研發提供了新的動力。

基于區塊鏈的平臺的另一個例子是，以IoT（Internet of Things，物聯網）市場為導向的自主智能體IOTA的分散式網絡。盡管我們所討論的項目變得通用了，但它們都集中在特定類型的自主智能體上，這嚴重限制了可用的服務。AIRA項目首先引入了分散式交易市場的概念，自主智能體和人員可以消費和提供服務。

作者將這個概念定義為“機器人經濟學”（robonomics）。這種AIRA方法建議拒絕集中式機器人控制的原則，以在機器人和人類之間提供分散式通信，使用基于區塊鏈的智能合約作為這些通信的基礎。由于責任依賴于現實世界的流程，所以不能保證智能體始終能夠正確地執行它們。

這可能是由服務提供者造成的，因為（1）故意欺詐或（2）由于故障而導致的不正確行為。對于第一個問題，AIRA開發人員認為，可以開發一個聲譽模型并將其集成到共識協議中，該協議將在區塊鏈信息中反映出對智能體的信任程度。

因此，消費者可以進一步依賴這些信息來選擇服務提供者。對于第二個問題，AIRA項目仍然需要技術和理論的解決方案，這是本文的重點。

圖2：我們在Duckietown環境中的實驗。Duckiebot執行一項任務，通過遵循責任智能合約中的標簽順序，并將觀察到的標簽記錄到日志中，這是由驗證人在任務結束后進行驗證得到的，從而最終穿過“城市”。

在這項研究中，我們將注意力集中在那些其行為可以用非確定性有限狀態自動機進行描述的智能體上（（又可以被稱之為基于智能體系統））。對于這些智能體，我們提供了全新的責任執行的驗證方法，使得能夠檢測出由故障的智能體。

它的工作原理是假定出現故障的服務提供商所產生的結果與其行為模型相矛盾，并導致自動暫停購買。驗證方法是基于正式的軟件驗證方法，即模型檢查（Model Checking）。由于移動機器人可以在諸如物流、運輸等方面的現實生活中加以使用，所以我們為Duckietown環境提供了簡單的原型實現，其中，一個移動機器人穿過城鎮，以給定的標簽序列為導向，在一個完整場景結束時通過自身的行為驗證實現任務目標。

我們的驗證方法可以（1）直接實現到一個共識協議中，或（2）實現作為分散式區塊鏈應用程序的一部分。在前一種情況下，假定責任執行的驗證可以在驗證者節點（采礦者）和交易上以分散形式進行，確認服務是以一種適當的方式進行提供的，將被包括在新區塊中。

例如，它可以通過支持可插拔共識的現有解決方案來實現，如Parity或Hyperledger。而在后一種情況下，它被集成到AIRA的方法中，其中驗證由第三方應用程序執行，該應用程序將驗證結果提交給以太坊智能合約。

這項研究是全周期責任執行的概念驗證，涵蓋了驗證階段。有了這個證明概念，那么如今評估現有的roboomics基礎設施并提出相關改善是非常重要的。這項研究的重要組成部分是現實生活中實際應用案例的分析。

在這項研究中，我們考慮簡單的行為模型，它可以被評估為復雜的出租車服務原型的第一級，并作為案例研究的起點。通過不斷地添加的新組件便可以順序地增加其復雜性。每個組件和案例都是進一步調查的主題。尚未解決的問題如下：

1）通常情況下，用戶會要求出租車服務從A點到B點去接他們。這應該被定義為，完整循環（移到A然后移到B）的目標是什么？以及我們應該為這種情況創建多少智能合同。

2）在我們簡單的案例中，用戶直接與robocar進行交易，這意味著用戶應提前知道汽車的位置和地址。但是，通常情況并非如此。某些中間服務需要連接到用戶和服務提供商。

3）隨著物聯網設備數量的不斷增加以及道路基礎設施的不斷完善，我們有可能將其轉變為robeconomic的一部分。例如，汽車可以與基礎設施進行交互，以建立最佳路線，甚至還可以從基礎設施那里獲得有力支持。

4）AIRA責任驗證模型假定機器人不會故意偽造目標執行日志（objective execution intentionally）。這意味著，服務提供者可以選擇接受報酬，盡管其尚未提供相應服務。目前，有可能解決這一問題的方案是引入“記錄器”（recorders），例如，它可以將智能體在特定時間內，于特定地點出現的事實，記錄在區塊鏈中。在日志檢驗過程中可以考慮這些信息。我們應該建立完整的過程描述以及經濟模型：有人應該為這些數據支付費用。

顯然，復雜的智能體行為需要通過建模和檢驗框架進行改進：

?模型校驗方法的主要缺點是，對于基于基于智能體的系統而言，其狀態數量會隨變量數量的增加，而呈現出增長態勢。這意味著并非所有模型都可以進行物理處理，因此需要一種機制來限制模型的復雜性。

?當概率模型比非確定性模型更適用時，就必須開展更多的工作來擴展這一方法。在這種情況下，可以采用概率模型檢驗（Probabilistic Model Checking）。

?檢驗框架也可以得到增強。特別是這樣一種工具的實現，即該工具使得能夠從模型檢驗模型（Model Checking model）中自動生成高級代碼，并將其集成到服務開發項目中。

?使用新的屬性類型可以使屬性生成工具得到增強。此外，我們還可以將工具的使用權限擴展至客戶，允許他們構建自己的屬性，例如，允許服務提供者在履行責任之前，檢驗所提交的模型是否滿足他們的需求。

在本文中，我們提出了一種針對自主智能體（autonomous agents）分散交易市場模型的概念，并將其命名為robonomics。針對基于智能體的特殊系統，我們還引入了一種基于模型檢驗的正式軟件驗證技術的新方法，以解決責任執行的驗證問題，這有助于中止對發生故障的服務提供者的支付行為，并可與聲譽模型一起集成于區塊鏈共識協議中。

驗證過程試圖證明服務提供者在執行操作后所提交的結果與其事先提交的行為模型相對應。然而，要將屬性作為輸入傳遞給模型檢驗器（Model Checker），就必須將其轉換為時態邏輯公式（Temporal Logic formula）。

此外，復雜系統模型的構建也是一項復雜的任務，該模型適合于模型檢驗器的執行。因此，我們建立了有助于解決這兩項問題的框架。驗證方法作為復雜AIRA robonomics原型的一部分受到了評估，該原型是使用Duckietown項目實現的。

該原型實現了一個簡單的真實案例，即一個機器人根據給定路線行駛，并進行了后續責任驗證。最后，我們討論了所提解決方案對于未來的影響。