模型检测多智体系统中的一种状态空间约简技术-限界模型检测
为了形式化描述多智体系统中与概率、实时、知识相关的性质，提出一种概率实时认知逻辑PTCTLK.模型检测是验证多智体系统是否满足PTCTLK公式的主要技术，状态空间爆炸是该技术实用化的主要瓶颈，为此提出一种PTCTLK的限界模型检测算法，其基本思想是在有限的局部可达空间中逐步搜索属性成立的证据，从而达到约简状态空间的目的.首先将PTCTLK的模型检测问题转换为无实时算子的PBTLK的模型检测问题；其次定义PBTLK的限界语义，并证明其正确性；然后设计基于线性方程组求解的限界模型检测算法；最后依据概率度量的演化规律，探索检测过程终止的判别准则.实例研究表明在属性为真的证据较短的情况下，限界模型检测能快速完成验证.
多智体系统 模型检测 限界模型检测 状态空间爆炸
周从华 叶萌 王昌达 刘志锋
江苏大学计算机科学与通信工程学院,镇江 212013
国内会议
长春
中文
1-27
2012-08-04（万方平台首次上网日期，不代表论文的发表时间）