多智体系统中约简状态空间的限界模型检测算法

作     者：周从华 叶萌 王昌达 刘志锋 

作者机构：江苏大学计算机科学与通信工程学院江苏镇江212013 

基　　金：国家自然科学基金(61003288 61111130184) 教育部博士点基金(20093227110005) 江苏省自然科学基金(BK2010192) 

出 版 物：《软件学报》 (Journal of Software)

年 卷 期：2012年第23卷第11期

页      码：2835-2861页

摘      要：为了形式化描述多智体系统中与概率、实时、知识相关的性质,提出了一种概率实时认知逻辑PTCTLK.模型检测是验证多智体系统是否满足PTCTLK公式的主要技术,状态空间爆炸是该技术实用化的主要瓶颈,为此提出一种PTCTLK的限界模型检测算法.其基本思想是,在有限的局部可达空间中逐步搜索属性成立的证据,从而达到约简状态空间的目的.首先,将PTCTLK的模型检测问题转换为无实时算子的PBTLK的模型检测问题;其次,定义PBTLK的限界语义,并证明其正确性;然后,设计基于线性方程组求解的限界模型检测算法;最后,依据概率度量的演化规律,探索检测过程终止的判别准则.实例研究结果表明,与无界模型检测相比,在属性为真的证据较短的情况下,限界模型检测完成验证所需空间更小.

主 题 词：多智体系统 模型检测 限界模型检测 状态空间爆炸 

学科分类：12[管理学] 1201[管理学-管理科学与工程类] 081104[081104] 08[工学] 0835[0835] 0811[工学-水利类] 0812[工学-测绘类] 

核心收录：

D　O　I：10.3724/SP.J.1001.2012.04304

馆 藏 号：203980711...