可能性测度下计算树逻辑的若干性质

• 作 者: 李亚利 李永明
• 机 构: 陕西师范大学计算机科学学院
• 出 处: 陕西师范大学学报：自然科学版
• 发表日期: 2013年6期
• 关键词: 计算树逻辑 可能的Kripke结构 等价性 定性性质 定量性质 computation tree logic possibilistic Kripke stru
• 基金项目: 国家自然科学基金资助项目（11271237,61228305）,中央高校基本科研业务费专项资金项目（GK201001003）.

为讨论可能的计算树逻辑（PoCTL）与计算树逻辑（CTL）的关系,给出PoCTL公式与CTL公式等价的概念,利用公式的等价性证明了CTL是PoCTL的一个真子集.通过PoCTL模型检测算法与PoCTL公式的分析,解决了PoCTL模型检测的时间复杂度问题.最后对重复事件与持久性事件的定性性质及定量性质进行研究,用实例验证了CTL公式与PoCTL公式在可能性测度与概率测度下的本质区别.