稠密时间系统的TCTL必然性分析
摘要：分支时态逻辑中的必然性属性与语法为forall eventually phi的性质相关，其中phi是一个任意的（定时的）CTL公式。从"好事情将会发生"的意义上来说，它们与线性时态逻辑中的"活跃性"属性相似。在密集时态逻辑中，这种必然性属性可以通过最大不动点计算进行分析。我们提出了模型检验必然性属性的算法，包括要求非Zeno计算和不要求非Zeno计算的情况。我们讨论了一种在时态逻辑中提前决策最大不动点的技术，并通过非Zeno计算对最大不动点的评估进行了实验。我们还讨论了仅含有全局路径量词的TCTL子类，该子类允许对必然性属性进行安全抽象分析。最后，我们报告了我们的实现和实验结果，以展示我们的想法的合理性。
作者：Farn Wang, Geng-Dian Hwang and Fang Yu
论文ID：cs/0304003
分类：Symbolic Computation
分类简称：cs.SC
提交时间：2007-05-23