Possibilistic Computation Tree Logic: Decidability and Complete Axiomatization

Possibilistic computation tree Logic (PoCTL) is one kind of branching temporal logic combined with uncertain information in possibility theory, which was introduced in order to cope with the systematic verification on systems with uncertain information in possibility theory. There are two decision problems related to PoCTL: the model checking problem and the satisfiability problem. The model checking problem of PoCTL has been studied, while the satisfiability problem of PoCTL was not discussed. One of the purpose of this work is to study the satisfiability problem of PoCTL. By introducing some techniques to extract possibility information from PoCTL formulae and constructing their possibilistic Hintikka structures, we show that the satisfiability problem of PoCTL is decidable in exponential time. Furthermore, we give a complete axiomatization of PoCTL, which is another important inference problem of PoCTL.