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