智能体交互合作的逻辑建模与验证技术研究

The interactions and cooperation among agents are one of the most significant exhibitions of complex intelligence, and thus deserve intensive studies. However, the traditional models and theory impose presumptions that are too ideal to be realistic. This research project aims to formalize the interactions and cooperation of agents and the corresponding model checking techniques along with applications in logic-theoretic approaches, based on the theory and methodologies from some relevant subjects like Cooperative Game Theory. To be more specific, we will (1)propose logical constructs for the interactions and cooperation among agents with bounded rationality and actions, with a more realistic and computationally grounded semantics; (2)investigate how the model evolves by internal and external factors; (3)search for highly efficient symbolic model checking algorithms based on OBDD and SAT, which will be implemented and applied in specification and verification of scenarios in Service Computing (SC). The ultimate goal of this project is to provide concise, rich and practical logical languages to specify and verify the more realistic scenarios where interactions and cooperation among agents take place, and then apply them to analyze some typical cases in interactions and cooperation among service components in Service Computing (SC).

智能体的交互合作是复杂智能行为的深刻体现之一, 具有重要的研究意义.而传统的智能体交互合作模型都包含很理想化的理性假设, 这些假设距离智能体之间的现实交互较远. 本项目拟使用基于逻辑的方法, 融合合作博弈论等相关学科的最新思想理论, 对多智能体系统的交互合作进行形式化建模, 以及研究其相应的模型检测技术和应用. 具体内容包括(1)提出面向理性受限和行为受限的智能体交互合作逻辑语言,并且给出更加贴近实际情景, 且基于计算(Computationally Grounded)的语义模型;(2)研究智能体交互合作的动态模型; (3)设计高效的基于OBDD和SAT的模型检测算法并实现, 最后应用于服务计算场景的建模验证中. 本项目旨在为智能体在实际的交互合作情景提供简洁,高效和丰富的基于逻辑的建模和规范语言, 并能对服务计算场景中服务组件的交互合作规范进行分析和验证.

智能体的交互合作是复杂智能行为的深刻体现之一, 具有重要的研究意义. 而传统的智能体交互合作模型都包含很理想化的理性假设, 这些假设距离智能体之间的现实交互较远. 本项目使用基于逻辑的形式化方法, 对多智能体系统的交互合作进行形式化建模, 以及研究其相应的模型检测技术和应用. 主要研究内容包括(1)面向受限智能体交互合作的逻辑模型; (2)智能体交互合作的动态模型; (3)高效的符号化模型检测算法和底层基础算法包的优化。经过四年研究，本项目已在多智能体交互合作的逻辑建模、动态模型、符号化模型检测、底层BDD和SAT逻辑优化计算方面取得一系列突出成果, 在国际著名期刊和会议上已经发表论文13篇，其中包括CCF A类论文8篇 (AAAI 2篇 , IJCAI 4篇, AIJ 2篇)，CCF B类论文1篇，CCF C类论文2篇，培养了4名青年教师团队成员和6名研究生，完成了原计划指标任务。