主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2018-2019年专刊出版计划 微信服务介绍 最新一期:2018年第12期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
张业迪,宋富.异构多智能体系统模型检查.软件学报,2018,29(6):1582-1594
异构多智能体系统模型检查
Model-Checking for Heterogeneous Multi-Agent Systems
投稿时间:2017-06-29  修订日期:2017-09-01
DOI:10.13328/j.cnki.jos.005462
中文关键词:  模型检查  多智能体系统  交替时态逻辑  策略类型
英文关键词:model-checking  multi-agent system  alternating-time temporal logic  strategy abilities
基金项目:国家自然科学基金(61402179,61532019)
作者单位E-mail
张业迪 上海科技大学 信息科学与技术学院, 上海 201210  
宋富 上海科技大学 信息科学与技术学院, 上海 201210 songfu@shanghaitech.edu.cn 
摘要点击次数: 640
全文下载次数: 560
中文摘要:
      模型检查作为一种自动化系统验证方法,已被应用于多智能体系统的验证.由此延伸出的规约描述语言——交替时态逻辑(ATL),也被给予了高度关注.根据智能体是否可以看到全局信息,分为不完全信息和完全信息;根据智能体是否可以记录历史信息,分为记忆能力和限记忆能力,提出了4种经典的策略类型.这些策略类型是通过ATL的语义进行刻画的.然而在一个多智能体系统中,考虑完全信息和限记忆能力时,所有智能体都只能选择这一种策略类型;在考虑不完全信息或记忆能力时,仅在联合模态操作<<A>>φ和[[A]]φA里出现的智能体具备这种策略类型,而其他智能体还是完全信息和限记忆能力策略类型.这可能会导致嵌套联合模态操作中智能体策略类型的不一致,且智能体策略类型取决于逻辑公式和逻辑的语义.而在实际多智能体系统中,智能体的策略类型往往取决于系统本身,且不同智能体具有不同的策略类型,即,智能体策略类型是异构的,这种多智能体系统被称为异构多智能体系统.针对这些问题,提出了一种在语法层对智能体策略类型进行刻画的系统模型——带类型解释系统.带类型解释系统在已有的解释系统中为每个智能体引入策略类型这一属性,允许不同智能体具备不同的策略类型.带类型解释系统可用于异构多智能体系统的建模.针对提出的系统模型,对ATL语义进行了研究,设计了ATL模型检查算法,实现了相应的模型检查工具ShTMC.
英文摘要:
      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.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利