Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Possibilistic Computation Tree Logic: Decidability and Complete Axiomatization

Yongming Li

TL;DR

This work resolves the satisfiability and axiomatization problems for Possibilistic Computation Tree Logic (PoCTL) by introducing possibilistic Hintikka structures and a tableau-based decision procedure, proving satisfiability is decidable in exponential time and establishing the small-model and tree-model properties. It also provides a complete axiomatization, $ ext{AxSys}_{ ext{PoCTL}}$, with a soundness and weak completeness guarantee. The approach hinges on extracting possibility information from PoCTL formulas, employing a positive normal form, and ensuring eventualities are fulfilled via structured fragments, linking local consistency to global satisfiability. The findings lay a solid theoretical foundation for PoCTL-based verification in uncertain domains, while outlining avenues for extending PoCTL to generalized and fuzzy temporal logics and more complex decision-making frameworks.

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.

Possibilistic Computation Tree Logic: Decidability and Complete Axiomatization

TL;DR

This work resolves the satisfiability and axiomatization problems for Possibilistic Computation Tree Logic (PoCTL) by introducing possibilistic Hintikka structures and a tableau-based decision procedure, proving satisfiability is decidable in exponential time and establishing the small-model and tree-model properties. It also provides a complete axiomatization, , with a soundness and weak completeness guarantee. The approach hinges on extracting possibility information from PoCTL formulas, employing a positive normal form, and ensuring eventualities are fulfilled via structured fragments, linking local consistency to global satisfiability. The findings lay a solid theoretical foundation for PoCTL-based verification in uncertain domains, while outlining avenues for extending PoCTL to generalized and fuzzy temporal logics and more complex decision-making frameworks.

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.
Paper Structure (14 sections, 14 theorems, 22 equations, 1 table)

This paper contains 14 sections, 14 theorems, 22 equations, 1 table.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Possibility theory
  4. PoCTL formulae and their positive normal forms
  5. Syntax of PoCTL
  6. Semantics of PoCTL
  7. The positive normal form of PoCTL formulae
  8. The satisfiability for PoCTL
  9. Possibilistic Hintikka structures for the formulae of PoCTL
  10. The satisfiability of PoCTL
  11. The axiomatization for PoCTL
  12. The axiomatic system $\text{AxSys}_{\text{PoCTL}}$
  13. The completeness of $\text{AxSys}_{\text{PoCTL}}$
  14. Conclusion

Key Result

Theorem 1

li13$Po$ is a possibility measure on $\Omega=2^{Paths(M)}$, i.e., $Po$ satisfies the following conditions: (1) $Po(\varnothing)=0$, $Po(Paths(M))=1$; (2) $Po(\bigcup\limits_{i\in I}A_{i})={\rm sup}\{Po(A_{i}): i\in I\}$ for any $A_{i}\in\Omega$, $i\in I$.

Theorems & Definitions (37)

  • Definition 1
  • Definition 2
  • Remark 1
  • Definition 3
  • Theorem 1
  • Remark 2
  • Definition 4
  • Definition 5
  • Definition 6
  • Definition 7
  • ...and 27 more