Verification of resource-bounded multi-agent systems (VRBMAS)

多智能体系统是由多个交互智能体组成的系统。代理是一个自治实体，它有能力收集信息，对信息进行推理，并根据信息执行行动，以追求自己的目标或代表他人。代理的例子包括自动设备的控制器，如卫星、医疗保健系统、无人驾驶运输系统，如无人机，甚至传感器网络中的节点。多代理系统无处不在。许多分布式软件和硬件系统可以自然地建模为多代理系统。这类系统的组件本质上是极其复杂的，组件之间的相互作用可能会导致不易检测到的不良行为。因此，多智能体系统的自动验证是一个非常重要且蓬勃发展的研究领域。我们在这一领域提出了一个重要的进步，即生产验证工具，允许用户指定代理的行动需要哪些资源。目前的工具没有提供一个系统的框架来模拟代理人行动的资源需求。然而，这种能力对于许多系统的规范是非常重要的，例如节点的资源非常有限的传感器网络。

A multi-agent system is a system which is comprised of multiple interacting agents. An agent is an autonomous entity that has the ability to collect information, reason about it, and perform actions based on it in pursuit of its own goals or on behalf of others. Examples of agents are controllers for automatic devices such as satellites, health care systems, non-driver transport systems such as UAVs, and even nodes in sensor networks.Multi-agent systems are ubiquitous. Many distributed software and hardware systems can be naturally modelled as multi-agent systems. Such systems are by nature of their components extremely complex, and the interaction between components can lead to undesired behaviours that are not easy to detect. Hence, automated verification of multi-agent systems is a very important and thriving research area. We propose an important advance in this area, namely producing verification tools which allow users to specify which resources the agents need for their actions. Current tools do not offer a systematic framework for modelling resource requirements for agents' actions. However, such an ability is very important for specification of many systems, for example sensor networks where the nodes have very limited resources, e.g. energy.