异构多智能体系统模型检查
作者:
作者单位:

作者简介:

张业迪(1996-),女,黑龙江五常人,硕士生,主要研究领域为模型检查;宋富(1983-),男,博士,tenure-track助理教授,研究员,博士生导师,CCF专业会员,主要研究领域为模型检查,程序分析与验证,系统安全.

通讯作者:

宋富,E-mail:songfu@shanghaitech.edu.cn

基金项目:

国家自然科学基金(61402179,61532019)


Model-Checking for Heterogeneous Multi-Agent Systems
Author:
Affiliation:

Fund Project:

National Natural Science Foundation of China (61402179, 61532019)

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
    摘要:

    模型检查作为一种自动化系统验证方法,已被应用于多智能体系统的验证.由此延伸出的规约描述语言——交替时态逻辑(ATL),也被给予了高度关注.根据智能体是否可以看到全局信息,分为不完全信息和完全信息;根据智能体是否可以记录历史信息,分为无记忆能力和无限记忆能力,提出了4种经典的策略类型.这些策略类型是通过ATL的语义进行刻画的.然而在一个多智能体系统中,考虑完全信息和无限记忆能力时,所有智能体都只能选择这一种策略类型;在考虑不完全信息或无记忆能力时,仅在联合模态操作<<A>>φ和[[A]]φA里出现的智能体具备这种策略类型,而其他智能体还是完全信息和无限记忆能力策略类型.这可能会导致嵌套联合模态操作中智能体策略类型的不一致,且智能体策略类型取决于逻辑公式和逻辑的语义.而在实际多智能体系统中,智能体的策略类型往往取决于系统本身,且不同智能体具有不同的策略类型,即,智能体策略类型是异构的,这种多智能体系统被称为异构多智能体系统.针对这些问题,提出了一种在语法层对智能体策略类型进行刻画的系统模型——带类型解释系统.带类型解释系统在已有的解释系统中为每个智能体引入策略类型这一属性,允许不同智能体具备不同的策略类型.带类型解释系统可用于异构多智能体系统的建模.针对提出的系统模型,对ATL语义进行了研究,设计了ATL模型检查算法,实现了相应的模型检查工具ShTMC.

    Abstract:

    Model-checking, an automatic verification methodology, has been applied to verify multi-agent systems. Alternating-time temporal logic (ATL), a property specification language for multi-agent systems was also investigated. According to whether agents are able to observe the whole information of the system and whether agents are able to record the history information, agents' strategies are divided into four types. These strategy abilities are defined in semantic level of ATL, as well as other logics. However, under perfect information and perfect recall setting, all agents have the same strategy ability. Under imperfect information and/or imperfect recall setting, only agents appeared in coalition modalities <<A>>φ and [[A]]φ have imperfect information and/or imperfect recall strategies, while other agents not in A still have perfect information and perfect recall strategies. When coalition modalities are nested, same agents may have different strategy abilities to fulfill different sub formulas, which results in inconsistency. On the other hand, in practice, agents' strategy abilities are usually decided by the multi-agent systems rather than the specifications, and different agents may own different strategy abilities. This kind of multi-agent systems is called heterogeneous mutli-agent systems. To overcome these problems, this paper proposes a new formal model, called typed interpreted systems which are able to define agent's strategy abilities at syntax level. Typed interpreted systems extend interpreted systems by associating each agent with a strategy type denoting the agent's strategy ability, therefore are able to model heterogeneous mutli-agent systems. The paper investigates the semantics of ATL on this new model and proposes an EXPTIME model-checking algorithm. The model-checking algorithm is implemented in a prototype tool ShTMC.

    参考文献
    相似文献
    引证文献
引用本文

张业迪,宋富.异构多智能体系统模型检查.软件学报,2018,29(6):1582-1594

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
历史
  • 收稿日期:2017-06-29
  • 最后修改日期:2017-09-01
  • 录用日期:2017-11-06
  • 在线发布日期: 2017-12-28
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号