Specification, Verification, and Synthesis of Autonomous Adaptive Agents

该项目专注于开发语言、算法和工具，用于验证和合成满足给定规范的代理和多代理系统。验证很重要，因为多智能体系统通常具有难以预测的紧急性质，客户希望在信任此类系统之前得到保证。代理通常用于实现可自我监控和修复的自适应系统。它们很难手工设计和调试。自动合成技术可用于支持配置和适配。 重点并不主要放在计划上，在计划中，一个人从一系列原始的行动中综合出一个计划来实现一个目标。相反，我们考虑这样的问题：定制/监督，其中我们已经有一个代理或系统，并且我们希望约束其行为以满足一组规范；以及组合/编排，其中我们有一组可用代理，并且我们希望组合它们以获得满足某些临时扩展目标的新系统。 我们最近工作中的一个主要进展是识别了一类重要的行动理论，对于这些行动理论，时间性质的验证是可决定的。在该项目中，我们将进一步发展这个有界行动理论框架，以适应更现实的代理模型。我们还将开发技术和工具来对此类有界理论进行验证和综合。 我们将把这些方法应用于代理监督，这是一种定制形式，其中代理的行为被约束为满足规范。由于某些操作可能是不可控的，因此可能无法限制代理执行符合规范的操作序列集。我们的方法找到了最大限度允许的主管，它给代理尽可能多的灵活性/自主权，同时确保它符合规范。在该项目中，我们将推广我们的代理监管框架，以处理复杂的分层/模块化系统。 我们还将继续研究用于代理验证和合成的不动点逼近技术。这些技术是不完整的，但可以用于一般的无限状态系统。

The project focuses on the development of languages, algorithms, and tools for verifying and synthesizing agents and multiagent systems that satisfy given specifications. Verification is important because multiagent systems often have emergent properties that are hard to predict and clients want guarantees before they will trust such systems. Agents are often used to implement adaptive systems that can monitor and repair themselves. They are difficult to design and debug by hand. Automated synthesis techniques can be used to support configuration and adaptation. The focus is not primarily on planning, where one synthesizes a plan to achieve a goal from a set of primitive actions. Instead, we consider problems such as customization/supervision, where we already have an agent or system and we want to constrain its behaviour to meet a set of specifications, and composition/orchestration, where we have a set of available agents and we want to compose them to obtain a new system that meets satisfies some temporally extended goal. A major advance in our recent work has been the identification of an important class of action theories for which verification of temporal properties is decidable. In the project, we will further develop this bounded action theories framework to accomodate more realistic models of agents. We will also develop techniques and tools for doing verification and synthesis for such bounded theories. We will apply these methods to agent supervision, a form of customization where the agent's behaviour is constrained to satisfy a specification. Since some actions may be uncontrollable, it may not be possible to restrict the agent to perform exactly the set of action sequences that satisfy the specification. Our approach finds the maximally permissive supervisor that gives as much flexibility/autonomy to the agent as possible while ensuring that it complies with the specification. In the project, we will generalize our agent supervision framework to handle complex hierarchical/modular systems. We will also continue our work on fixpoint approximation techniques for agent verification and synthesis. These techniques are incomplete, but can be used on general infinite state systems.