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

Bounded Model Checking Algorithm to Reduce the State Space in Multi-Agent Systems

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

In order to specify properties relating to probability, real time, and knowledge on multi-agent systems, a logic system PTCTLK is proposed. Model checking is an automatic technique for checking if a multi-agent system satisfies a PTCTLK formula. The state explosion problem is the key obstacle in checking the feasibility of the model. In this paper, a bounded model checking algorithm for PTCTLK is proposed. First the model checking of PTCTLK is reduced to the model checking of PBTLK, which does not contain real time operators. Second, the bounded semantics of PBTLK is defined and its correctness is proven. Third, the bounded model checking procedure of PBTLK is transformed into a linear equation. Finally, the paper discusses the law of increasing of probability measure, and some termination criterions are given. The case study shows that compared with the unbounded model checking, if the length of the witness is short, then the bounded model checking needs less space.