作者：梁常建; 李永明可能性理论计算树逻辑模型检测时间复杂性规约
摘要：本文首先分别给出了“约束可达”,“总是可达”这两个公式在广义可能性计算树逻辑（GPo CTL）中的另外两种等价形式;其次讨论了基于广义可能性测度的计算树逻辑的模型检测问题,将GPo CTL的模型检测问题规约为经典的CTL模型检测问题,利用截集的方法,给出了计算GPo CTL的模型检测问题的算法及其复杂度,并通过实例分析说明了这种算法的可行性;最后,研究了具有公平性假设的GPo CTL模型检测问题的计算复杂度,得到了与上面相似的结论.
注：因版权方要求，不能公开全文，如需全文，请咨询杂志社
