| 摘要: |
| 为了缓解概率计算树逻辑模型检测中的状态空间爆炸问题,提出了概率计算树逻辑的限界模型检测技术.该技术首先定义概率计算树逻辑的限界语义,并证明其正确性;之后,通过实例说明在传统限界模型检测中,以路径长度作为判断检测过程终止的标准已经失效,基于数值计算中牛顿迭代法的终止准则,设计了新的终止判断标准;然后提出基于线性方程组求解的限界模型检测算法;最后,通过3 个测试用例说明,概率计算树逻辑限界模型检测方法在反例较短的情况下能够快速完成检测过程,而且比概率计算树逻辑的无界模型检测算法所需求得的状态空间要少. |
| 关键词: 模型检测 限界模型检测 概率计算树逻辑 马尔可夫链 |
| DOI：10.3724/SP.J.1001.2012.04089 |
| 分类号: |
| 基金项目:国家自然科学基金(61003288, 61111130184, 60773049); 江苏省自然科学基金(BK2010192); 教育部博士点基金(20093227110005) |
|
| Bounded Model Checking for Probabilistic Computation Tree Logic |
|
ZHOU Cong-Hua, LIU Zhi-Feng, WANG Chang-Da
|
|
School of Computer Science and Telecommunication Engineering, Jiangsu University, Zhenjiang 212013, China
|
| Abstract: |
| 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. |
| Key words: model checking bounded model checking probabilistic computation tree logic Markov chains |
