论文部分内容阅读
本文首先分别给出了“约束可达”,“总是可达”这两个公式在广义可能性计算树逻辑（GPo CTL）中的另外两种等价形式;其次讨论了基于广义可能性测度的计算树逻辑的模型检测问题,将GPo CTL的模型检测问题规约为经典的CTL模型检测问题,利用截集的方法,给出了计算GPo CTL的模型检测问题的算法及其复杂度,并通过实例分析说明了这种算法的可行性;最后,研究了具有公平性假设的GPo CTL模型检测问题的计算复杂度,得到了与上面相似的结论.