Specification, Verification, and Synthesis of Autonomous Adaptive Agents

自主自适应代理的规范、验证和综合

• 批准号: RGPIN-2015-03756
• 负责人: Lesperance, Yves
• 金额: $ 1.75万
• 依托单位: York University
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2018
• 资助国家: 加拿大
• 起止时间: 2018-01-01 至 2019-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=657274
• 关键词: Specification; Verification; Synthesis; Autonomous; Adaptive

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

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