概率计算树逻辑的限界模型检测

Bounded Model Checking for Probabilistic Computation Tree Logic

为了缓解概率计算树逻辑模型检测中的状态空间爆炸问题,提出了概率计算树逻辑的限界模型检测技术.该技术首先定义概率计算树逻辑的限界语义,并证明其正确性;之后,通过实例说明在传统限界模型检测中,以路径长度作为判断检测过程终止的标准已经失效,基于数值计算中牛顿迭代法的终止准则,设计了新的终止判断标准;然后提出基于线性方程组求解的限界模型检测算法;最后,通过3个测试用例说明,概率计算树逻辑限界模型检测方法在反例较短的情况下能够快速完成检测过程,而且比概率计算树逻辑的无界模型检测算法所需求得的状态空间要少.

In order to overcome the state explosion problem in model checking the probabilistic computation tree logic, a bounded model checking technique is proposed. First, the bounded semantics of the probabilistic computation tree logic is presented, and then its correctness is proved. Second, by a simple instance the criterion of the traditional termination, based on the length of path, is shown to fail. Based on the termination criterion used in the Newton iteration in numerical computing, a new criterion is given. Third, the bounded model checking procedure of the probabilistic computation tree logic is transformed into linear equations. Finally, three benchmarks are used to present the advantages of the bounded model checking.