Possibilistic Computation Tree Logic: Decidability and Complete Axiomatization

TL;DR

This paper investigates the satisfiability problem of Possibilistic Computation Tree Logic (PoCTL), proving its decidability in exponential time and providing a complete axiomatization for the logic.

Contribution

It introduces techniques to analyze PoCTL satisfiability, establishing its decidability and offering the first complete axiomatization of PoCTL.

Findings

Satisfiability problem of PoCTL is decidable in exponential time.

Constructed possibilistic Hintikka structures for PoCTL.

Provided a complete axiomatization of PoCTL.

Abstract

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.