摘要：概率模型检验建立在非概率模型检验技术的基础上，不仅能够对系统进行定性的验证，还能够定量判断系统满足相关性质的概率，具有广泛的适用性。LTL概率模型检验算法的复杂度较高，达到双重指数级别，现有的工具如PRISM与MRMC均不支持对LTL性质的验证。针对这个问题，通过对原有的LTL概率模型检验算法进行优化，实现了一个高效的LTL概率模型检验工具。通过对比实验验证了该工具的有效性。

关键词：ltl 概率模型检验 优化 

单位：国防科学技术大学计算机学院; 湖南长沙410073