论文部分内容阅读
连续时间马尔科夫链(CTMC)在网络性能分析、模型检测和系统生物学等领域受到了广泛的关注。本文关注以连续时间马尔科夫链为模型、以条件连续随机逻辑(CCSL)为性质描述语言的概率模型检测问题。CCSL通过引入条件概率运算符扩展了Aziz等人提出的连续随机逻辑(CSL)，从而可以表达和检测CTMC更多的性质，本文针对CCSL逻辑提出了基于参数乘积CTMC的近似模型检测算法，并分析了该算法的理论时间复杂度。进而，本文介绍了针对CSL和CCSL逻辑开发的概率模型检测工具CCMC，已有的概率模型检测工具如PRISM和MRMC仅仅支持CSL二元Until公式，CCMC是第一个支持CSL全部语法形式和其扩展的概率模型检测工具。最后，本文通过一些实例分析展示了工具的性能和实用价值。