Possibilistic Computation Tree Logic over Finitely-Valued Kripke Structures: Decidability and Complete Axiomatization

Abstract

Possibilistic computation tree logic (PoCTL) is a branching-time temporal logic for specifying and verifying systems whose behavior is described by possibility theory. Although the model-checking problem for PoCTL has been investigated, its satisfiability problem and proof-theoretic foundations, particularly the development of a sound and complete axiomatization,remain largely unexplored. We investigate these problems over normalized possibilistic Kripke structures whose transition possibilities take finitely many values; their state spaces may be countably infinite. A counterexample shows that unrestricted countable structures do not have the finite-model property, thereby distinguishing the semantic scope of the present results. For the finitely-valued class, we extract a finite threshold scale from the input formula and define canonical admissible transitions by the set $D(s,t)$. Independent eventuality ranks guide the selection of local witnesses. Finite supported fragments are then spliced cyclically to obtain a model, without requiring the ranks of different eventualities to decrease simultaneously. This yields a finite-model property. Satisfiability for the unbounded language over this class is EXPTIME-complete, and the tableau procedure runs in time $2^{O(n^2)}$. Bounded operators are handled by explicit finite unfolding, with complexity measured after this preprocessing. Finally, we establish a sound and weakly complete finitary axiomatization by translating tableau deletion into formal refutations.