Fuzzy Computation Tree Temporal Logic with Quality Constraints and Its Model Checking

The encapsulation of particular quality functions and predicates within temporal logic formulas markedly enhances the representation of detailed temporal characteristics within a system. During our preliminary investigations, we innovatively combined quality constraint functions and predicates with Possibility Linear Temporal Logic (PoLTL), yielding the conception of Fuzzy Linear Temporal Logic with Quality Constraints (QFLTL). This amalgamation results in a significant elevation of QFLTL’s expressivity relative to PoLTL, ensuring the preservation of informational integrity whilst achieving a synchronized, yet selectively inclined, and exact consolidation of path reachability specifics alongside property satisfaction evaluations. This treatise represents a significant contribution to the field by integrating quality constraint functions and predicates into Possibility Computation Tree Temporal Logic (PoCTL), thus giving rise to Fuzzy Computation Tree Temporal Logic with Quality Constraints (QFCTL). We provide a comprehensive definition of QFCTL’s syntax, conduct an in-depth analysis of its logical characteristics, outline a precise model checking algorithm for QFCTL, and perform a meticulous complexity assessment of said algorithm. It is illustrated by examples that PoCTL is a proper subset of QFCTL, and QFCTL has stronger expressive power than PoCTL and can characterize more refined temporal properties of the system. An in-depth exploration of the logical characteristics of QFCTL was carried out, showing its unique logical characteristics that are distinct from other temporal logic systems under the influence of quality constraints. In particular, the introduction of characteristic predicates effectively classifies the satisfaction of temporal formulas, making the logical framework of QFCTL more complete compared to the existing probabilistic temporal logic. Moreover, by enriching QFCTL with a quantitative characteristic predicate operator, we innovate, culminating in the development of an enhanced Fuzzy Computation Tree Temporal Logic with Quality Constraints (QFCTL*). The logical characteristics of QFCTL* are explored in detail. It is shown that with the support of quantitative feature predicates, QFCTL* can divide the satisfaction of temporal formulas more delicately than QFCTL. The decision theorems for the semantics of QFCTL* formulas containing quantitative feature predicates are given, and the decidability of QFCTL* is strictly proved. Through the bounded-depth search of GPKS, a model-checking algorithm of QFCTL* on GPKS is presented. The correctness of the algorithm is proved, and the complexity of the algorithm is analyzed. In order to prove the practical applications and strong expressive capabilities of QFCTL and QFCTL*, we present a model-checking example as empirical evidence for the effectiveness of the proposed model-checking algorithms. Through this example, we verify that, compared with the existing PoCTL, QFCTL and QFCTL* can avoid the loss of system path reachability information or system property satisfaction information, ensure the synchronization of the two types of information, and fuse these two types of information according to weight preferences. QFCTL and QFCTL* can also synthesize temporal formulas that characterize the subproperties of the system according to weight preferences. These application examples also verify that the QFCTL and QFCTL* model-checking algorithms proposed in this article are automatic and effective.