摘要

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