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.***