删除或更新信息,请邮件至freekaoyan#163.com(#换成@)

异构多智能体系统模型检查

本站小编 Free考研考试/2022-01-02

摘要:模型检查作为一种自动化系统验证方法,已被应用于多智能体系统的验证.由此延伸出的规约描述语言——交替时态逻辑(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.



PDF全文下载地址:

http://jos.org.cn/jos/article/pdf/5462
相关话题/智能 信息 系统 逻辑 语言

  • 领限时大额优惠券,享本站正版考研考试资料!
    大额优惠券
    优惠券领取后72小时内有效,10万种最新考研考试考证类电子打印资料任你选。涵盖全国500余所院校考研专业课、200多种职业资格考试、1100多种经典教材,产品类型包含电子书、题库、全套资料以及视频,无论您是考研复习、考证刷题,还是考前冲刺等,不同类型的产品可满足您学习上的不同需求。 ...
    本站小编 Free壹佰分学习网 2022-09-19
  • 基于SMT的时钟约束语言CCSL的形式化分析方法与工具
    摘要:时钟约束语言CCSL是一种用于描述实时嵌入式系统中事件之间约束的形式化语言,它是UML针对实时嵌入式系统建模的扩展包MARTE(modelingandanalysisofreal-timeandembeddedsystems)中用于对时间建模的一个子语言.给定一组由CCSL定义的时钟约束条件, ...
    本站小编 Free考研考试 2022-01-02
  • 一种嵌套中断系统的建模和分析方法
    摘要:在嵌入式系统和各类操作系统中,中断机制是确保实时响应各类异步事件的重要方法.通常在处理一个中断事件的过程中,往往会有更紧迫的中断事件请求响应,因而发生中断嵌套.建模并验证嵌套中断系统是具有挑战性的工作.提出一种建模和验证嵌套中断系统的方法.首先,提出基于投影时序逻辑(projectiontem ...
    本站小编 Free考研考试 2022-01-02
  • 机器人关节通信总线系统的建模与验证
    摘要:高速串行现场总线(controllerareanetwork,简称CAN)被广泛部署到机器人通信系统中.而服务机器人任务具有并发性和高实时性的特点,因此,如何根据总线协议规范和应用需求精化设计模型,保证系统设计的正确性和实时性要求,避免设计阶段的漏洞十分必要.针对传统方法的局限性,提出使用形式 ...
    本站小编 Free考研考试 2022-01-02
  • 医学影像计算机辅助检测与诊断系统综述
    摘要:计算机辅助检测/诊断(computer-aideddetection/diagnosis,简称CAD)能够提高诊断的准确性,减少假阳性的产生,为医生提供有效的诊断决策支持.旨在分析计算机辅助诊断工具的最新发展.以CAD研究较多的四大致命性癌症的发病医学部位为主线,按照不同的成像技术和病类,对目 ...
    本站小编 Free考研考试 2022-01-02
  • 基于同态加密系统的图像鲁棒可逆水印算法
    摘要:同态加密技术可用于保护数据隐私并允许对密文数据进行算术操作,在云计算安全上有着很好的应用前景.针对云计算中的隐私保护和数据安全等问题,提出了一种基于同态加密系统的图像鲁棒可逆水印算法,主要思想为:(1)对原始图像进行分块和利用Paillier加密系统进行加密得到密文图像;(2)在加密域中,通过 ...
    本站小编 Free考研考试 2022-01-02
  • 基于创意序列学习的艺术风格学习与绘制系统
    摘要:在众多传统艺术绘画形式中,笔触是被现代计算机绘画工具(GIMP、Photoshop和Painter)普遍采用的形式之一.创新性地提出了服务于非真实感渲染AI辅助艺术创作系统(A4).系统能够实现自动生成特定艺术家风格的笔触效果.该系统在强化学习框架下,主要进行以下研究工作:(1)提出基于PGP ...
    本站小编 Free考研考试 2022-01-02
  • 分布式图处理系统技术综述
    摘要:图作为一种基本的数据类型,是对现实世界中对象及其关联关系的一种抽象.现实中,许多科学问题都可以被模型化为图的问题,因此,对图数据进行分析非常重要.图数据分析在语义Web分析、社交网络、生物基因分析以及信息检索等领域有着广泛的应用.随着移动互联、物联网等信息技术的发展,图数据的规模处于持续增长的 ...
    本站小编 Free考研考试 2022-01-02
  • 基于疾病信息网络的表型相似基因搜索
    摘要:人类基因组计划的成果推动了生物信息学研究的发展.基于疾病表型相似性策略寻找功能上存在联系的致病基因,即表型相似基因,具有重要的研究价值和广阔的应用前景,是新兴的研究热点.然而,生物医学领域尚没有利用计算机方法开展基于基因-疾病-表型关系网络的表型相似基因搜索研究.对此,利用疾病公开数据库构建了 ...
    本站小编 Free考研考试 2022-01-02
  • 一种融合节点先验信息的图表示学习方法
    摘要:图表示学习是实现各类图挖掘任务的基础.现实中的图数据不仅包含复杂的网络结构,还包括多样化的节点信息.如何将网络结构和节点信息更加有效地融入图的表示学习中,是一个重要的问题.为了解决这一问题,基于深度学习,提出了融合节点先验信息的图表示学习方法.该方法将节点特征作为先验知识,要求学习到的表示向量 ...
    本站小编 Free考研考试 2022-01-02
  • 经验研究中情景感知需求获取与建模系统文献综述
    摘要:情景感知(contextaware)的应用是当前的一个研究热点,但是,由于情景的复杂性和不确定性,如何获取这些应用的需求面临着巨大挑战,需求工程领域出现了大量的研究来解决这一挑战.使用系统文献综述(systematicliteraturereview)的方法首先分析了不同情景维度对需求获取与建 ...
    本站小编 Free考研考试 2022-01-02