Abstract:

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.

Key words: possibilistic Kripke structure;possibility measure;possibility computation tree logic；persistence property