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

• 作者: 刘志锋 叶萌 周从华 王昌达
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 多智体系统 模型检测 限界模型检测 状态空间爆炸
• 年，卷（期）: 2012,（11）
• 页码范围: 2835-2861
• 分类号: TP18
• 字数: 21216字
• 语种: 中文

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	王昌达	江苏大学计算机科学与通信工程学院	50	237	9.0	13.0
2	周从华	江苏大学计算机科学与通信工程学院	46	193	7.0	11.0
3	刘志锋	江苏大学计算机科学与通信工程学院	29	118	5.0	10.0
4	叶萌	江苏大学计算机科学与通信工程学院	1	7	1.0	1.0