一种对于分散式交易市场中基于智能体的服务提供者的责任执行验证方法

随着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项目实现的。

该原型实现了一个简单的真实案例，即一个机器人根据给定路线行驶，并进行了后续责任验证。最后，我们讨论了所提解决方案对于未来的影响。