广义可能性计算树逻辑的模型检测问题

摘要

Firstly,two alternative equivalent forms of GPoCTL state formulas,"until","always",are given respectively.Secondly,it shows that the model checking problem of GPoCTL can be reduced to which of CTL,its algorithm is given through the method of cut set,and whose availability is explained with an example analysis,as a result,the time complexity of the algorithm is obtained.Finally,the properties of the GPoCTL model checking problem with fairness assumptions,which are similar to the GPoCTL,are studied by the similar method with GPoCTL.%本文首先分别给出了“约束可达”,“总是可达”这两个公式在广义可能性计算树逻辑(GPoCTL)中的另外两种等价形式;其次讨论了基于广义可能性测度的计算树逻辑的模型检测问题,将GPoCTL的模型检测问题规约为经典的CTL模型检测问题,利用截集的方法,给出了计算GPoCTL的模型检测问题的算法及其复杂度,并通过实例分析说明了这种算法的可行性;最后,研究了具有公平性假设的GPoCTL模型检测问题的计算复杂度,得到了与上面相似的结论.