多智能体动作推理及高级控制的理论与技术研究

Reasoning about actions and change is an important research area in Artificial Intelligence, and it lays the theoretical foundation for high-level agent control, two main methods for which are planning and high-level program execution. So far, research in reasoning about actions and high-level agent control has mainly been concerned with the single-agent case. However, in real-world applications, multiple agents interact in complex ways: an agent’s actions might be partially observable to other agents, an agent has to reason about other agents’ knowledge and belief in order to interact with them, and different agents might have conflicts of interests. Thus reasoning about actions and high-level agent control become much more challenging for multi-agent systems. Building on the situation calculus, by exploiting new developments in epistemic logic, game theory, and computational logic, this project aims to develop theory and techniques for reasoning about actions and high-level agent control in multi-agent domains, including: representation and reasoning about knowledge and belief change, representation and reasoning about strategic abilities and strategies, epistemic planning and high-level epistemic program execution, and automatic verification of agent programs, and eventually apply the above theory and techniques to general game playing (GGP).

关于动作和变化的推理是人工智能中的一个重要研究领域，是实现智能体高级控制的理论基础。智能体高级控制的两种主要方法是规划和高级程序执行。但目前这一领域的研究主要针对的是单智能体情形。然而，在现实世界中，常常有多个智能体以复杂的方式相互作用：智能体的动作对其他智能体可能是部分可观察的，智能体需要对其他智能体的知识和信念进行推理，且不同智能体之间可能存在竞争关系。因而多智能体系统对关于动作的推理和智能体高级控制带来了极大的挑战。本项目拟以情景演算为基础，结合认知逻辑，博弈论和计算逻辑中的最新进展，发展多智能体动作推理和高级控制的理论和技术，包括：多智能体知识和信念及其变化的表示和推理，策略能力和策略的表示和推理，认知规划和高级认知程序执行，及智能体程序的自动验证，并将以上理论和技术应用于通用游戏博弈(GGP)中。

本项目研究多智能体动作推理和高级控制的理论和技术。主要取得了以下成果：1. 研究了多智能体模态逻辑中的遗忘，证明除了K4n和S4n，其他主要的多智能体模态系统在遗忘下都是封闭的。2. 基于情景演算提出了完全信息和不完全信息下的结构化策略和策略能力的表示和推理的一般框架。基于ATL和LDL，提出了在策略约束下关于联合能力表示和推理的一种模态逻辑，并证明了针对无记忆策略的该逻辑的模型检测问题的复杂性为PSPACE。3.提出了自动验证Golog程序部分正确性及通过数学归纳法自动验证动态系统活性性质的可靠但不完备的方法。4. 提出了基于高阶信念变化的多智能体认知规划框架，并将其扩展到公共知识。5. 提出了一种从所有小实例的解中学习的通用规划求解方法。提出了通用策略的有穷自动机（FSA）表示方法，并提出了基于反例驱动的不变式的局部搜索的一种FSA策略的自动验证方法。基于此验证方法，提出了通用策略的一种自动生成方法。6. 研究了通过遗忘来实现动作理论的抽象。我们证明了：给定一个低级动作理论和一个从高级符号到低级表示的细化映射，可以使用遗忘来构造一个高级动作理论，构成低级动作理论的抽象。本项目已在Artificial Intelligence期刊发表论文1篇，在国际人工智能联合会议IJCAI发表论文5篇，在国际人工智能会议AAAI发表论文1篇，在欧洲人工智能会议ECAI发表论文2篇。