{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T01:37:40Z","timestamp":1760146660204,"version":"build-2065373602"},"reference-count":36,"publisher":"MDPI AG","issue":"12","license":[{"start":{"date-parts":[[2024,11,27]],"date-time":"2024-11-27T00:00:00Z","timestamp":1732665600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"National Natural Science Foundation of China","award":["12071271","11671244","12471437","23JSZ011","23JSY048","2020YFC1523305","2022-QY-203","20SKY021"],"award-info":[{"award-number":["12071271","11671244","12471437","23JSZ011","23JSY048","2020YFC1523305","2022-QY-203","20SKY021"]}]},{"name":"Shaanxi Fundamental Science Research Project for Mathematics and Physics","award":["12071271","11671244","12471437","23JSZ011","23JSY048","2020YFC1523305","2022-QY-203","20SKY021"],"award-info":[{"award-number":["12071271","11671244","12471437","23JSZ011","23JSY048","2020YFC1523305","2022-QY-203","20SKY021"]}]},{"name":"National Key R&amp;D Plan","award":["12071271","11671244","12471437","23JSZ011","23JSY048","2020YFC1523305","2022-QY-203","20SKY021"],"award-info":[{"award-number":["12071271","11671244","12471437","23JSZ011","23JSY048","2020YFC1523305","2022-QY-203","20SKY021"]}]},{"name":"Key R&amp;D and Transformation Plan of Qinghai Province","award":["12071271","11671244","12471437","23JSZ011","23JSY048","2020YFC1523305","2022-QY-203","20SKY021"],"award-info":[{"award-number":["12071271","11671244","12471437","23JSZ011","23JSY048","2020YFC1523305","2022-QY-203","20SKY021"]}]},{"name":"Scientific and Technological Research Fund of Shangluo University","award":["12071271","11671244","12471437","23JSZ011","23JSY048","2020YFC1523305","2022-QY-203","20SKY021"],"award-info":[{"award-number":["12071271","11671244","12471437","23JSZ011","23JSY048","2020YFC1523305","2022-QY-203","20SKY021"]}]},{"name":"Shangluo University Key Disciplines Project","award":["12071271","11671244","12471437","23JSZ011","23JSY048","2020YFC1523305","2022-QY-203","20SKY021"],"award-info":[{"award-number":["12071271","11671244","12471437","23JSZ011","23JSY048","2020YFC1523305","2022-QY-203","20SKY021"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Axioms"],"abstract":"<jats:p>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\u2019s 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\u2019s 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.<\/jats:p>","DOI":"10.3390\/axioms13120832","type":"journal-article","created":{"date-parts":[[2024,11,27]],"date-time":"2024-11-27T10:05:56Z","timestamp":1732701956000},"page":"832","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Fuzzy Computation Tree Temporal Logic with Quality Constraints and Its Model Checking"],"prefix":"10.3390","volume":"13","author":[{"ORCID":"https:\/\/orcid.org\/0009-0002-3270-5542","authenticated-orcid":false,"given":"Xianfeng","family":"Yu","sequence":"first","affiliation":[{"name":"College of Computer Science, Qinghai Normal University, Xining 810008, China"},{"name":"School of Mathematics and Computer Application, Shangluo University, Shangluo 726000, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yongming","family":"Li","sequence":"additional","affiliation":[{"name":"College of Computer Science, Qinghai Normal University, Xining 810008, China"},{"name":"School of Mathematics and Statistics, Shaanxi Normal University, Xi\u2019an 710062, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shengling","family":"Geng","sequence":"additional","affiliation":[{"name":"College of Computer Science, Qinghai Normal University, Xining 810008, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2675-931X","authenticated-orcid":false,"given":"Huirong","family":"Li","sequence":"additional","affiliation":[{"name":"School of Mathematics and Computer Application, Shangluo University, Shangluo 726000, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"1968","published-online":{"date-parts":[[2024,11,27]]},"reference":[{"key":"ref_1","unstructured":"Baier, C., and Katoen, J.P. (2008). Principles of Model Checking, MIT Press."},{"key":"ref_2","unstructured":"Edmund, M., Grumberg, O., and Peled, D. (1999). Model Checking, MIT Press."},{"key":"ref_3","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1023\/A:1022920129859","article-title":"Model checking programs","volume":"10","author":"Visser","year":"2003","journal-title":"Autom. Softw. Eng."},{"key":"ref_4","doi-asserted-by":"crossref","first-page":"8","DOI":"10.1109\/2.65","article-title":"Formal verification of hardware correctness: Introduction and survey of current research","volume":"21","author":"Camurati","year":"1998","journal-title":"Computer"},{"key":"ref_5","doi-asserted-by":"crossref","first-page":"171752","DOI":"10.1109\/ACCESS.2019.2953858","article-title":"A research landscape on formal verification of software architecture descriptions","volume":"7","author":"Araujo","year":"2019","journal-title":"IEEE Access"},{"key":"ref_6","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1145\/307988.307989","article-title":"Formal verification in hardware design: A survey","volume":"4","author":"Kern","year":"1999","journal-title":"ACM Trans. Des. Autom. Electron. Syst. (TODAES)"},{"key":"ref_7","doi-asserted-by":"crossref","first-page":"589","DOI":"10.1007\/s10009-021-00633-z","article-title":"The probabilistic model checker Storm","volume":"24","author":"Hensel","year":"2022","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"ref_8","unstructured":"Trippel, T., Shin, K.G., Chernyakhovsky, A., Kelly, G., Rizzo, D., and Hicks, M. (2022, January 10\u201312). Fuzzing hardware like software. Proceedings of the 31st USENIX Security Symposium (USENIX Security 22), Boston, MA, USA."},{"key":"ref_9","first-page":"117","article-title":"Verification of communication protocols based on formal methods integration","volume":"9","year":"2012","journal-title":"Acta Polytech. Hung."},{"key":"ref_10","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1023\/A:1008719024240","article-title":"Symbolic verification of communication protocols with infinite state spaces using QDDs","volume":"14","author":"Boigelot","year":"1999","journal-title":"Form. Methods Syst. Des."},{"key":"ref_11","doi-asserted-by":"crossref","first-page":"16504","DOI":"10.1109\/TITS.2021.3129458","article-title":"A hybrid approach to trust node assessment and management for vanets cooperative data communication: Historical interaction perspective","volume":"23","author":"Gao","year":"2021","journal-title":"IEEE Trans. Intell. Transp. Syst."},{"key":"ref_12","doi-asserted-by":"crossref","first-page":"3533","DOI":"10.1109\/TITS.2020.2983835","article-title":"V2VR: Reliable hybrid-network-oriented V2V data transmission and routing considering RSUs and connectivity probability","volume":"22","author":"Gao","year":"2020","journal-title":"IEEE Trans. Intell. Transp. Syst."},{"key":"ref_13","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1007\/s00165-012-0269-9","article-title":"Formal verification of security protocol implementations: A survey","volume":"26","author":"Avalle","year":"2014","journal-title":"Form. Asp. Comput."},{"key":"ref_14","doi-asserted-by":"crossref","first-page":"601","DOI":"10.1016\/S1389-1286(03)00292-5","article-title":"Formal verification: An imperative step in the design of security protocols","volume":"43","author":"Coffey","year":"2003","journal-title":"Comput. Netw."},{"key":"ref_15","doi-asserted-by":"crossref","first-page":"95956","DOI":"10.1109\/ACCESS.2020.2995917","article-title":"BAKMP-IoMT: Design of blockchain enabled authenticated key management protocol for internet of medical things deployment","volume":"8","author":"Garg","year":"2020","journal-title":"IEEE Access"},{"key":"ref_16","doi-asserted-by":"crossref","first-page":"15824","DOI":"10.1109\/JSEN.2020.3009382","article-title":"Blockchain-enabled certificate-based authentication for vehicle accident detection and notification in intelligent transportation systems","volume":"21","author":"Vangala","year":"2020","journal-title":"IEEE Sens. J."},{"key":"ref_17","first-page":"314","article-title":"Consensus of switched multi-agent systems","volume":"63","author":"Zheng","year":"2016","journal-title":"IEEE Trans. Circ. Syst. II"},{"key":"ref_18","first-page":"1","article-title":"A novel group consensus protocol for heterogeneous multi-agent systems","volume":"106","author":"Zheng","year":"2015","journal-title":"Int. J. Contr."},{"key":"ref_19","doi-asserted-by":"crossref","first-page":"2043","DOI":"10.1109\/TAC.2010.2042982","article-title":"Consensus conditions of multi-agent systems with time-varying topologies and stochastic communication noises","volume":"55","author":"Li","year":"2010","journal-title":"IEEE Trans. Autom. Contr."},{"key":"ref_20","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/TAC.2010.2052384","article-title":"Distributed consensus with limited communication data rate","volume":"56","author":"Li","year":"2011","journal-title":"IEEE Trans. Autom. Contr."},{"key":"ref_21","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1007\/s004460050046","article-title":"Model checking for a probabilistic branching time logic with fairness","volume":"11","author":"Baier","year":"1998","journal-title":"Distrib. Comput."},{"key":"ref_22","doi-asserted-by":"crossref","first-page":"356","DOI":"10.1145\/2166.357214","article-title":"Termination of probabilistic concurrent programs","volume":"5","author":"Hart","year":"1983","journal-title":"ACM Trans. Prog. Lang. Syst."},{"key":"ref_23","doi-asserted-by":"crossref","first-page":"991","DOI":"10.1137\/0214070","article-title":"Concurrent probabilistic programs, or: How to schedule if you must","volume":"14","author":"Hart","year":"1985","journal-title":"SIAM J. Comput."},{"key":"ref_24","doi-asserted-by":"crossref","first-page":"6291","DOI":"10.1016\/j.eswa.2014.04.008","article-title":"Modeling and verifying probabilistic multi-agent systems using knowledge andsocial commitments","volume":"41","author":"Sultan","year":"2014","journal-title":"Expert Syst. Appl."},{"key":"ref_25","doi-asserted-by":"crossref","first-page":"397","DOI":"10.1016\/j.asoc.2014.04.014","article-title":"Model checking probabilistic social commitments for intelligent agent com-munication","volume":"22","author":"Sultan","year":"2014","journal-title":"Appl. Softw. Comput."},{"key":"ref_26","doi-asserted-by":"crossref","first-page":"114792","DOI":"10.1016\/j.eswa.2021.114792","article-title":"Model checking agent-based communities against uncertain group commitments and knowledge","volume":"177","author":"Sultan","year":"2021","journal-title":"Expert Syst. Appl."},{"key":"ref_27","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1145\/990010.990011","article-title":"Multi-valued symbolic model-checking","volume":"12","author":"Chechik","year":"2003","journal-title":"ACM Trans. Softw. Eng. Method."},{"key":"ref_28","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1007\/s10703-006-0016-z","article-title":"Data structures for symbolic multi-valued model-checking","volume":"29","author":"Chechik","year":"2006","journal-title":"Form. Methods Syst. Des."},{"key":"ref_29","doi-asserted-by":"crossref","first-page":"44","DOI":"10.1016\/j.fss.2014.03.009","article-title":"Computation tree logic model checking based on possibility measures","volume":"262","author":"Li","year":"2015","journal-title":"Fuzzy Sets. Syst."},{"key":"ref_30","doi-asserted-by":"crossref","first-page":"2034","DOI":"10.1109\/TFUZZ.2015.2396537","article-title":"Quantitative computation tree logic model checking based on generalized possibility measures","volume":"23","author":"Li","year":"2015","journal-title":"IEEE Trans. Fuzzy Syst."},{"key":"ref_31","doi-asserted-by":"crossref","first-page":"30","DOI":"10.1145\/2629606","article-title":"Fuzzy time in linear temporal logic","volume":"15","author":"Frigeri","year":"2014","journal-title":"ACM Trans. Comput. Log."},{"key":"ref_32","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2875421","article-title":"Formally reasoning about quality","volume":"63","author":"Almagor","year":"2016","journal-title":"J. ACM"},{"key":"ref_33","doi-asserted-by":"crossref","unstructured":"Yu, X., Li, Y., and Geng, S. (2024). Fuzzy Linear Temporal Logic with Quality Constraints. Mathematics, 12.","DOI":"10.3390\/math12193148"},{"key":"ref_34","doi-asserted-by":"crossref","unstructured":"Solaiman, B., Gu\u00e9riot, D., Almouahed, S., Alsahwa, B., and Boss\u00e9, \u00c9. (2021). A new hybrid possibilistic-probabilistic decision-making scheme for classification. Entropy, 23.","DOI":"10.3390\/e23010067"},{"key":"ref_35","doi-asserted-by":"crossref","first-page":"41","DOI":"10.3233\/FI-2011-598","article-title":"A possibilistic argumentation decision making framework with default reasoning","volume":"113","author":"Nieves","year":"2011","journal-title":"Fundam Informaticae"},{"key":"ref_36","doi-asserted-by":"crossref","first-page":"734","DOI":"10.2991\/ijcis.2017.10.1.49","article-title":"A piecewise type-2 fuzzy regression model","volume":"10","author":"Bajestani","year":"2017","journal-title":"Int. J. Comput. Intell. Syst."}],"container-title":["Axioms"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/2075-1680\/13\/12\/832\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T16:40:47Z","timestamp":1760114447000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/2075-1680\/13\/12\/832"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,27]]},"references-count":36,"journal-issue":{"issue":"12","published-online":{"date-parts":[[2024,12]]}},"alternative-id":["axioms13120832"],"URL":"https:\/\/doi.org\/10.3390\/axioms13120832","relation":{},"ISSN":["2075-1680"],"issn-type":[{"type":"electronic","value":"2075-1680"}],"subject":[],"published":{"date-parts":[[2024,11,27]]}}}