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.