%0 Journal Article
%T 多智体系统中约简状态空间的限界模型检测算法
%A 周从华？
%A 叶萌？
%A 王昌达？
%A 刘志锋？
%J 软件学报
%P 2835-2861
%D 2012
%R 10.3724/SP.J.1001.2012.04304
%X 为了形式化描述多智体系统中与概率、实时、知识相关的性质,提出了一种概率实时认知逻辑ptctlk.模型检测是验证多智体系统是否满足ptctlk公式的主要技术,状态空间爆炸是该技术实用化的主要瓶颈,为此提出一种ptctlk的限界模型检测算法.其基本思想是,在有限的局部可达空间中逐步搜索属性成立的证据,从而达到约简状态空间的目的.首先,将ptctlk的模型检测问题转换为无实时算子的pbtlk的模型检测问题;其次,定义pbtlk的限界语义,并证明其正确性;然后,设计基于线性方程组求解的限界模型检测算法;最后,依据概率度量的演化规律,探索检测过程终止的判别准则.实例研究结果表明,与无界模型检测相比,在属性为真的证据较短的情况下,限界模型检测完成验证所需空间更小.
%K 多智体系统
%K 模型检测
%K 限界模型检测
%K 状态空间爆炸
%U http://www.jos.org.cn/ch/reader/view_abstract.aspx?file_no=4304&flag=1