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...
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
MDPI AG
2024-11-01
|
| Series: | Axioms |
| Subjects: | |
| Online Access: | https://www.mdpi.com/2075-1680/13/12/832 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1850240432487792640 |
|---|---|
| author | Xianfeng Yu Yongming Li Shengling Geng Huirong Li |
| author_facet | Xianfeng Yu Yongming Li Shengling Geng Huirong Li |
| author_sort | Xianfeng Yu |
| collection | DOAJ |
| description | 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. |
| format | Article |
| id | doaj-art-dd6ba19565664d8aa930a6839f3ece4b |
| institution | OA Journals |
| issn | 2075-1680 |
| language | English |
| publishDate | 2024-11-01 |
| publisher | MDPI AG |
| record_format | Article |
| series | Axioms |
| spelling | doaj-art-dd6ba19565664d8aa930a6839f3ece4b2025-08-20T02:00:51ZengMDPI AGAxioms2075-16802024-11-01131283210.3390/axioms13120832Fuzzy Computation Tree Temporal Logic with Quality Constraints and Its Model CheckingXianfeng Yu0Yongming Li1Shengling Geng2Huirong Li3College of Computer Science, Qinghai Normal University, Xining 810008, ChinaCollege of Computer Science, Qinghai Normal University, Xining 810008, ChinaCollege of Computer Science, Qinghai Normal University, Xining 810008, ChinaSchool of Mathematics and Computer Application, Shangluo University, Shangluo 726000, ChinaThe 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.https://www.mdpi.com/2075-1680/13/12/832quality functionquality predicateweighting functioninformation fusioninformation synchronizationinformation loss |
| spellingShingle | Xianfeng Yu Yongming Li Shengling Geng Huirong Li Fuzzy Computation Tree Temporal Logic with Quality Constraints and Its Model Checking Axioms quality function quality predicate weighting function information fusion information synchronization information loss |
| title | Fuzzy Computation Tree Temporal Logic with Quality Constraints and Its Model Checking |
| title_full | Fuzzy Computation Tree Temporal Logic with Quality Constraints and Its Model Checking |
| title_fullStr | Fuzzy Computation Tree Temporal Logic with Quality Constraints and Its Model Checking |
| title_full_unstemmed | Fuzzy Computation Tree Temporal Logic with Quality Constraints and Its Model Checking |
| title_short | Fuzzy Computation Tree Temporal Logic with Quality Constraints and Its Model Checking |
| title_sort | fuzzy computation tree temporal logic with quality constraints and its model checking |
| topic | quality function quality predicate weighting function information fusion information synchronization information loss |
| url | https://www.mdpi.com/2075-1680/13/12/832 |
| work_keys_str_mv | AT xianfengyu fuzzycomputationtreetemporallogicwithqualityconstraintsanditsmodelchecking AT yongmingli fuzzycomputationtreetemporallogicwithqualityconstraintsanditsmodelchecking AT shenglinggeng fuzzycomputationtreetemporallogicwithqualityconstraintsanditsmodelchecking AT huirongli fuzzycomputationtreetemporallogicwithqualityconstraintsanditsmodelchecking |