LTL概率模型检验优化技术的研究

摘要

概率模型检验是一种针对概率模型的形式化验证技术，与传统的非概率模型检验相比，概率模型检验不仅能对系统进行定性的检验，即判断系统是否满足某个给定的性质，而且还能定量的对概率系统，或者具有概率行为的系统进行检验，即模型在哪个概率区间满足给出的性质。概率模型检验中，通常用线性时序逻辑(Linear Temporal Logic，LTL)和计算树逻辑(Computational Tree Logic，CTL)来描述系统性质。虽然LTL与CTL表达能力有交集，但是如公平性性质这样重要的性质只能用LTL来表示。然而，相比于CTL，当前LTL概率模型检验算法的复杂度非常高，验证效率很低，因此目前已有的概率模型工具如MRMC和PRISM均不支持对LTL性质的验证。
　　针对这个问题，本文提出了一种基于概率保持的公式化简技术。该优化技术通过缩短待验证公式的长度来减小算法执行的时空开销，从而提高算法的执行效率，在一定程度上缓解了LTL概率模型检验算法复杂度高的难题。
　　以上述方法为基础，本文设计并实现了一个LTL概率模型检验工具，并针对现有概率模型检验的案例，利用该工具进行LTL概率模型检验的测试，以检验算法的有效性。

目录

声明

第一章 绪论

1.1 研究背景

1.2 模型检验技术

1.3 研究内容与研究动机

1.4 论文的主要工作和创新

1.5 论文组织结构

第二章 基础知识

2.1 基本概念

2.2 基本算法

2.3 小结

第三章 优化技术的研究

3.1 基于反例保持的公式化简技术

3.2 降低LTL概率模型检验算法复杂度的研究

3.3 基于概率保持的公式化简技术

3.4 小结

第四章 LTL概率模型检验工具的设计与实现

4.1 工具的设计

4.2 工具的实现

4.3 实验

4.4 小结

第五章 总结和展望

1、主要工作总结

2、 进一步工作

致谢

参考文献

作者在学期间取得的学术成果

附录A 工具实现细节