Specification, Verification, and Synthesis of Autonomous Adaptive Agents

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

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

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