欢迎您！东篱公司
退出
-
申报数据库
-
立项数据库
-
成果数据库
-
项目获奖数据库
中文摘要：
为讨论可能的计算树逻辑（PoCTL）与计算树逻辑（CTL）的关系,给出PoCTL公式与CTL公式等价的概念,利用公式的等价性证明了CTL是PoCTL的一个真子集.通过PoCTL模型检测算法与PoCTL公式的分析,解决了PoCTL模型检测的时间复杂度问题.最后对重复事件与持久性事件的定性性质及定量性质进行研究,用实例验证了CTL公式与PoCTL公式在可能性测度与概率测度下的本质区别.
英文摘要：
In order to discuss the relation between PoCTL and CTL,the definitions of the equivalence of PoCTL formulae and CTL formulae are given.It is proved that CTL is a proper subset of PoCTL by the equivalence of the formulae.Then,the problem of the time complexity of possibility model checking for possibilistic Kripke structure is solved by using an analysis for the algorithms of the PoCTL model checking and the PoCTL formulae.Finally,the quantitative properties and qualitative properties of repeated reachability and persistence are discussed,and the essential difference between CTL formulae and PoCTL formulae in possibility measure and probability measure are verificated by an example.
同期刊论文项目
同项目期刊论文
期刊信息
位置：