基于可能性测度的计算树逻辑

首先,提出了可能的Kripke结构的定义,建立了可能的Kripke结构的可能性测度空间,并分析了可能的Kripke结构的一系列性质,即任一路径转移的可能性可由其初始状态的可能性分布与各转移的可能性取下确界而得到;依据可能的Kripke结构所定义的可能性测度具有其合理性等等。其次,给出了可能性计算树逻辑(PoCTL)的概念,讨论了两个PoCTL状态公式以及PoCTL与经典计算树逻辑(CTL)公式的等价性。最后,证明了PoCTL公式有与CTL*公式中"一致性"相对应的公式。

Computation Tree Logic Based on Possibility Measure

Firstly,the definition of possibilistic Kripke structure is presented,and the possibility measure space based on it is established.The properties of possibilistic Kripke structure are discussesd,such as the possibility of each path is the infimum of the initial distribution and all of the transisiton possibilities,and the possibility measure which is defined in accordance with the possibilistic Kripke structure is reasonable,etc.Secondly,the possibility computation tree logic(PoCTL) is defined,the equivalence between two PoCTL formulae is studied,and the problems whether some PoCTL formulae are equivalent to some CTL formulae are analyzed.Finally,the persistence property corresponding to PoCTL in CTL*are proved.