2014/01/19 by Yongming Li, Yali Li, Li, Yongming +3 · 1 citation
Computer Science · #68Q85 #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.1401.4658
openalex publication_date 2014/01/19 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
In order to deal with the systematic verification with uncertain infromation in possibility theory, Li and Li \citeli12 introduced model checking of linear-time properties in which the uncertainty is modeled by possibility measures. Xue, Lei and Li \citeXue09 defined computation tree logic (CTL) based on possibility measures, which is called possibilistic CTL (PoCTL). This paper is a continuation of the above work. First, we study the expressiveness of PoCTL. Unlike probabilistic CTL, it is shown that PoCTL (in particular, qualitative PoCTL) is more powerful than CTL with respect to their expressiveness. The equivalent expressions of basic CTL formulae using qualitative PoCTL formulae are presented in detail. Some PoCTL formulae that can not be expressed by any CTL formulae are presented. In particular, some qualitative properties of repeated reachability and persistence are expressed using PoCTL formulae. Next, adapting CTL model-checking algorithm, a method to solve the PoCTL model-checking problem and its time complexity are discussed in detail. Finally, an example is given to illustrate the PoCTL model-checking method.