论文部分内容阅读
本文在Pandya提出的CTL*[DC]逻辑[1]的基础上，对其语法和语义进行扩展，在描述向前状态序列的性质前面引入量词，并对路径长度进行限制，定义了一个新的逻辑CTL*[k-QDDC]，使其可以更加灵活的描述前向性质，CTL*[K-QDDC]可应用于实时系统的描述和验证。本文给出了在Kripke结构中直接验证CTL*[k-QDDC]逻辑公式在某状态是否成真的基本算法，并分析了其算法复杂度。在某些假设下，证明了CTL*[k-QDDC]中的某个逻辑运算符的验证问题是NP完全的，这就说明CTL*[k-QDDC]的验证问题至少是NP难的，这使得难以为CTL*[K-QDDC]验证问题找到有效的算法。