多自主机器人协作及群体行为分析

一直以来，多自主机器人协作都是机器人学中的一个研究热点，以往的方法在优化效率和自适应性方面存在着很多亟待解决的问题。最近，费耶特维尔州立大学数学与计算机科学系，华沙理工大学计算机科学研究所的科学家们，对多自主机器人协作及群体行为进行了研究，提出了使用机器人行为划分的全新方法，在室内环境下对机器人的行为进行研究，并提出了验证和分析组合机器人行为的技术。

在本文中，我们对以往有关协作自主机器人的研究进行了扩展，将环境变化和群体中机器人数量的变化会影响分配给机器人群体的任务执行效率的情况，纳入了研究之中。我们提出了一种全新的基于机器人行为划分的方法，描述子路径的子图使得我们能够使用有限数量的状态组合对自主机器人之间的高级交互进行建模，避免可达性组合爆炸（combinatorial explosion）。我们对可以确保机器人交互正确性的系统进行了确认，提出了验证和分析组合机器人行为的新技术。通过分区图，我们可以对自主机器人之间的高级交互进行建模，并检测出诸如死锁（deadlock）、缺少终止（lack of termination）等异常情况。我们提出了使用模型检验方法对组合机器人行为进行验证和分析的技术。文中所描述的系统Dedan验证器仍处于开发阶段。在不久的将来，计划进行定时和概率验证。

介绍

如今，群体自主移动设备（机器人）的应用范围越来越广，这与它们对个体机器人的故障/碰撞和环境变化作出适当响应的自然能力有关。这种协作自主机器人系统可以应用于诸如军事侦察、监视和警戒系统等多个领域，因此它们的开发应该得到高度重视。实际上，群体机器人的研究面临着诸多挑战。我们可以针对有限数量的机器人分析多个自主机器人之间的协作，但想要进一步扩展更多的解决方案则是一个需要新技术的领域。在本文中，我们专注于研究基于分区行为算法的群体机器人的弹性协作问题。我们的内容涵盖了自主性局部和全部死锁检测技术，以及自主性局部和全部分布式终端的必然性检测技术。在本文中，我们试图回答以下若干研究问题：

（1）状态图是如何用于有效地描述大量机器人的？

（2）我们可以在多大程度上对解决方案进行扩展，以在考虑分布式中止和避免死锁的情况下，保证群体机器人能够进行适当的协作。

（3）我们可以在多大程度上对解决方案进行扩展，以在考虑任务目标（如区域覆盖范围、每个受保护地点的检测频率等）的情况下，保证群体机器人能够进行适当的协作。

（4）我们可以在多大程度上对解决方案进行扩展，以在我们充分响应个体机器人的故障/碰撞和环境变化时，保证群体机器人能够进行适当的协作。

（5）自主移动平台协作正确性的实时验证可行性如何？

在本文中，我们专注于研究室内环境中自主机器人的导航问题。我们假设机器人不仅可以直接对环境做出响应，还可以对其他机器人的动作做出响应。状态图以前往往用于描述机器人的行为，通常情况下，可以基于诸如此类的模型手动开发适当的软件。为了加速开发过程，我们创建了一个新的工具，以用于机器人行为的设计和验证。这种工具对于机器人反应行为的快速修正非常有用，因为它允许开发人员逐步地修正设计。此外，该工具的功能能够自动生成机器人行为以响应不断变化的要求。

在本文中，我们描述了分析传统状态图的技术，并对其进行修正，使其更适合于群体机器人以及大量此类状态图的集成。状态图使得我们可以对自主机器人群体之间的高级交互进行建模，并且可以确保机器人交互的正确性。当需要对机器人行为进行快速修正时，对机器人之间的交互进行快速检查是至关重要的。状态图的模型检查方法可以识别诸如死锁或活锁（live-lock）之类的问题，从而为机器人设计人员提供了一套即用型算法和技术，用于分析基于完整群体的系统属性。

通过CTL时间公式AG EX true（对于任何一个状态来说，都存在下一个状态）检查出无死锁（deadlock freeness）。然而，局部死锁却不那么容易被识别出来，因此我们提出了许多用于在具有特定形状的系统中进行自动死锁检测的方法。

在分布式系统的分析中，可以观察到两种进程中止：不合时宜的进程缺失（死锁），这是一个错误;被称之为进程终止的预期停止。死锁检测和终止检测方法必须能够区分两种中断的区别，或者只是简单地禁止其中一种。然而，完全终止似乎也是类似的情况：不存在未来。在循环系统中，我们不期望存在终止，公式AG EX true能够识别出死锁。这就是为什么许多死锁检测技术只针对无限循环系统（停止是一个死锁）。

在终端系统中，应将总死锁与总终止区分开来。实际上，各种分布式终止检测技术都在迅速发展，这些方法大都基于对分布式进程的某些特征的观察或对消息流量的控制。有时，分布式进程的特殊元素被定义用于终止检测。

与死锁检测一样，终止检测的动态（运行时）方法需要系统的一些测试。它通常发送一些消息，报告各个进程的状态，以及将它们组合成分布式终止的全局决策的机制。在测试、处理失败的进程或链接失败、接受临时网络划分方面存在不同的方法。静态终止检测方法是基于对单个进程终端状态的观察，模型检查技术适用于此目的，使用模型特定公式或通用公式。计数智能体的结构可以进行动态的和静态的应用。转换不变量使得我们能够检查在初始状态下开始的每个执行是否是有限的。

我们的方法是基于对分布式系统规范中的终止动作进行区分。

环境资源

从机器人程序员的角度来看，了解机器人将要经过的环境类型是非常重要的。一般来说，环境可以是已知的，也可以是未知的。在本文中，我们将集中描述机器人在已知环境中的行为。已知的环境通常通过一张地图进行描述，地图上标注了建筑物的所有部分，我们将其称为房间，房间之间的开口，我们将其简称为门。建筑结构的简单表示之一可以是一个图形，其以节点形式显示所有可访问的位置，并以指定訪问房间顺序的图路径形式显示到达这些位置的方法。

任何以图形形式出现的拓扑图也可以作为环境资源图表进行说明。这意味着图形的每个节点也可以被解释为资源，并且当机器人位置与该节点相关联时，我们可以宣称机器人获得了这个资源。当机器人离开节点时，我们声称它释放了资源。两个节点之间的链接也可以解释为可以获取和释放的资源。对拓扑图的这种解释使得我们可以将已知的资源分配算法应用于多个机器人行为的描述，并随后将其扩展到机器人群体中。

考虑图1中所示的拓扑图，它显示了若干个房间，且房间与房间之间有门。前缀A表示侧间，而前缀Q表示在机器人操作期间可能发生冲突的中央房间。房间的名称取自于基本方向。我们假设任何时候一个机器人可能出现在典型的房间QNW、QNE、QSW和QSE内，同时还有侧间AW、AN、AE和AS，使得多个机器人可以进行共同定位。我们还假设每个中央房间QNW、QNE、QSW和QSE都具有通往其他两个中央房间的开口，和通往其他两个侧间的门/开口。

用于群体机器人导航的快速生成状态图的实用程序

在以往的研究成果中，对确定性状态图进行了很好的描述。通常来说，确定性状态图除了状态之外，还具有由触发器和动作组成的转换，触发器会导致机器人从一个状态转换到另一个状态，而动作会在转换过程中被触发。触发器由连续计算评估的布尔条件表示，以响应环境的变化。

为了指定状态图，我们使用基于通用建模语言（Universal Modeling Language，UML）的符号，其中状态由方框表示，转换由带有标签的箭头指示。转换标签的第一部分（在斜杠的前面）指定触发器，斜杠后面的部分指定在转换期间要调用的动作（或消息）。概率规范的语法被描述为另外的第三个组成部分，用于指定整个转换的概率。

由于多种原因，显式依赖于位置的状态图可以便捷地指定机器人行为。首先，该图可以通过相对简单的环境资源图的转换进行构建。其次，可以相对容易地添加概率组合。最后，协作机器人的行为可以通过并发性状态图进行描述，并且所有成熟的用于并发性程序分析的技术都可以使用，即死锁检测或死锁避免算法。并发性分析可以自动完成，机器人程序可以直接从状态图模型生成。

基于环境图和相应的环境触发器，我们可以快速指定各种位置相关的状态图。使用自主机器人，我们可以对它们的行为进行规划，指定它们遵循的通用规则。规则可以给定机器人的目标房间，在图2中，从AS开始的机器人可以被引导到最终回到AS的AW、AN、AE侧室中，并访问路线上的中央房间。一组路线可以彼此独立，如在图2中，具有4个巡逻机器人的系统中，它们的方向总是向右的。

对于机器人，我们考虑行为A描述图2中右侧ROBOT1移动的简单路径：从特殊的侧间AE开始，然后沿着通向QNE的门，再继续直到进入AN并停止。

为了对这种行为进行建模，可以使用状态图模型。一般来说，我们可以使用多层模型，但在本文中为了简化表示，我们假设使用两层模型。上层模型是通过变换环境图获得的，即，将非定向边转换为有向边，并提供必要的触发器、动作和消息。

更确切地说，两个节点（例如AN和QNE）之间的链接可以进行如下解释：如果机器人被分配了资源AN，则它应该首先在释放资源AN之前获取资源QNE。图2中所示的状态图详细地指定了ROBOT1的行为A。类似地，可以相应地描述机器人2、3和4的行为。

为了正式指定如图2所示的说法，我们需要拓扑性识别触发器、拓扑动作和同步消息按此顺序对它们进行描述。这些拓扑结构中的每一个都可以由较低级别的图进行定义。

不同的拓扑位置，即不同的资源，通常会对机器人的传感器产生不同的值。传感器信号处理算法，即，将描述机器人传感器信号转换成可用于直接识别环境的高电平信号的算法。我们将假设较低级别的状态图可以描述这种算法，并且我们将这些信号称为供更高级别图表使用的环境触发器（environment trigger）。

多个自主机器人之间的协作

接下来，我们将讨论自主机器人之间的协作。有许多理论和实践解决方案可供考虑。

模型检查提供了一种最为通用的方法，不仅可用于避免死锁或检测，还可以用于检测和验证各种进程协作特性。通常情况下，模型检查是基于有限状态方法的，以便可以直接应用于我们的状态图。因此，对于一些机器人行为的验证具有重要的实用价值。遗憾的是，对于所描述的异步和概率模型，传统的模型检查方法不能提供一组即用型算法和技术来分析多个机器人系统的属性。

使用现有的时间验证器如Spin、NuSMV或Uppaal，可以很容易地证明无死锁性。然而，为了更为有效的机器人合作，我们需要更多细微的功能。例如，局部死锁是危险的，因为在这种情况下，一些机器人继续工作，但其中一些机器人卡住了，无法取得任何进展。所提到的任何一种通用模型检查器都不能自动发现局部死锁，用户必须根据已验证系统的特征自行指定此功能。

从上文所进行的描述以及图1中所预先给出的拓扑图可以知道，一组路线是可以彼此独立的，如在图2中，在具有4个巡逻机器人的系统中，它们的方向总是向右的。然而，如图5所示，路径可能会发生干扰。如果房间QNW、QNE、QSW和QSE被占用，则会发生明显的总死锁。我们可以使用防止死锁的路由来避免这种死锁，例如，只允许从AW和AN开始的两个机器人（如图6所示）进行一些选定的转换。而从AS和AE开始的其他机器人则保留了完全的选择自由，如圖7所示。

在本文中，我们将以往关于协作自主机器人的研究扩展到室内环境中，提出了一种使用机器人行为划分的新方法。描述机器人行为的子图使得我们能够基于有限数量的状态组合对自主机器人之间的高级交互进行建模，从而避免状态爆炸。我们确定了可以确保机器人交互正确性的系统，并提出了验证和分析组合机器人行为的技术。

Dedan验证环境使用模型检查技术，以用于查找部分以及全部的通信死锁和资源死锁。此外，同时，还进行自动验证分布式终端。除此之外，系统可以自动从服务器视图转换到智能体视图，可以观察和模拟系统的状态空间，并且系统可以转换为Promela（旋转验证器输入形式）和Uppaal。在系统中，我们可以使用经过验证的系统表征的图形形式，并支持对组件服务器/智能体的图形仿真。目前，我们所描述的系统仍在开发中，在不久的将来，我们会将自身用于非穷举部分死锁研究的算法纳入研究之中。分布式自动机的新概念正在开发中，使用计时自动机（以验证实时依赖性）和概率模型检查，将提供更高级的验证形式，最先进的功能之一将是能够进行自动或半自动行为修改，而这将显著改善协作自主机器人的动态弹性。