Abstract:
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.
