模型检验AORTA：验证具有验证意识的代理
Model Checking AORTA: Verification of Organization-Aware Agents
摘要：
随着代理系统变得越来越大，越来越复杂，越来越需要正式验证它们。此外，人们经常认为，复杂的系统可以使用组织模型进行管理，对系统中的代理人施加约束。能够理解系统中的组织模型和约束的代理被称为是组织感知的。本文研究了组织感知Agent的验证问题。我们将展示如何使用AORTA，使代理组织感知的框架，代理可以正式验证使用的代理Java Pathfront（AJPF），一个专门为代理程序设计语言设计的模型检验系统的扩展版本。我们集成AORTA与代理基础设施层（AIL），这是一个中间层上的APL可以实现的，并使用我们的扩展AJPF验证系统的代理，旨在写一份文件一起使用的组织协调。
英文摘要：
As agent systems grow larger and more complex, there is an increasing need to formally verify them. Furthermore, it is often suggested that complex systems can be regulated using organizational models, imposing constraints on the agents in the systems. Agents that can understand the organizational model and constraints in a system is said to be organization-aware. This paper is concerned with verification of organization-aware agents. We show how agents using AORTA, a framework for making agents organization-aware, can be formally verified using an extended version of the Agent Java PathFinder (AJPF), a model checking system designed specifically for agent programming languages. We integrate AORTA with the Agent Infrastructure Layer (AIL), which is an intermediate layer on top of which APLs can be implemented, and use our extension of AJPF to verify a system of agents aiming to write a paper together by using an organization for coordination.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
