{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,2]],"date-time":"2025-11-02T05:55:18Z","timestamp":1762062918210,"version":"build-2065373602"},"reference-count":30,"publisher":"MDPI AG","issue":"9","license":[{"start":{"date-parts":[[2022,8,24]],"date-time":"2022-08-24T00:00:00Z","timestamp":1661299200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61962001","YCX22196","YCX22184","2020KYQD 14","2019BEB04032","2021A1017"],"award-info":[{"award-number":["61962001","YCX22196","YCX22184","2020KYQD 14","2019BEB04032","2021A1017"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100012481","name":"Graduate Innovation Project of North Minzu University","doi-asserted-by":"publisher","award":["61962001","YCX22196","YCX22184","2020KYQD 14","2019BEB04032","2021A1017"],"award-info":[{"award-number":["61962001","YCX22196","YCX22184","2020KYQD 14","2019BEB04032","2021A1017"]}],"id":[{"id":"10.13039\/501100012481","id-type":"DOI","asserted-by":"publisher"}]},{"name":"North Minzu University","award":["61962001","YCX22196","YCX22184","2020KYQD 14","2019BEB04032","2021A1017"],"award-info":[{"award-number":["61962001","YCX22196","YCX22184","2020KYQD 14","2019BEB04032","2021A1017"]}]},{"name":"Provincial key R&amp; D of Ningxia Science and Technology Department","award":["61962001","YCX22196","YCX22184","2020KYQD 14","2019BEB04032","2021A1017"],"award-info":[{"award-number":["61962001","YCX22196","YCX22184","2020KYQD 14","2019BEB04032","2021A1017"]}]},{"name":"Provincial Natural Science Foundation of Ningxia","award":["61962001","YCX22196","YCX22184","2020KYQD 14","2019BEB04032","2021A1017"],"award-info":[{"award-number":["61962001","YCX22196","YCX22184","2020KYQD 14","2019BEB04032","2021A1017"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Entropy"],"abstract":"<jats:p>In order to solve the problems in fuzzy computation tree logic model checking with cost operator, we propose a fuzzy decision process computation tree logic model checking method with cost. Firstly, we introduce a fuzzy decision process model with cost, which can not only describe the uncertain choice and transition possibility of systems, but also quantitatively describe the cost of the systems. Secondly, under the model of the fuzzy decision process with cost, we give the syntax and semantics of the fuzzy computation tree logic with cost operators. Thirdly, we study the problem of computation tree logic model checking for fuzzy decision process with cost, and give its matrix calculation method and algorithm. We use the example of medical expert systems to illustrate the method and model checking algorithm.<\/jats:p>","DOI":"10.3390\/e24091183","type":"journal-article","created":{"date-parts":[[2022,8,24]],"date-time":"2022-08-24T21:03:51Z","timestamp":1661375031000},"page":"1183","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Model Checking Fuzzy Computation Tree Logic Based on Fuzzy Decision Processes with Cost"],"prefix":"10.3390","volume":"24","author":[{"given":"Zhanyou","family":"Ma","sequence":"first","affiliation":[{"name":"School of Computer Science and Engineering, North Minzu University, Yinchuan 750000, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5350-956X","authenticated-orcid":false,"given":"Zhaokai","family":"Li","sequence":"additional","affiliation":[{"name":"School of Computer Science and Engineering, North Minzu University, Yinchuan 750000, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Weijun","family":"Li","sequence":"additional","affiliation":[{"name":"School of Computer Science and Engineering, North Minzu University, Yinchuan 750000, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yingnan","family":"Gao","sequence":"additional","affiliation":[{"name":"School of Computer Science and Engineering, North Minzu University, Yinchuan 750000, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xia","family":"Li","sequence":"additional","affiliation":[{"name":"School of Computer Science and Engineering, North Minzu University, Yinchuan 750000, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"1968","published-online":{"date-parts":[[2022,8,24]]},"reference":[{"key":"ref_1","unstructured":"Baier, C., and Katoen, J.P. (2008). Principles of Model Checking, MIT Press."},{"key":"ref_2","doi-asserted-by":"crossref","first-page":"416","DOI":"10.1109\/TC.2016.2604308","article-title":"Deriving unbounded reachability proof of linear hybrid automata during bounded checking procedure","volume":"66","author":"Xie","year":"2017","journal-title":"IEEE Trans. Comput."},{"key":"ref_3","doi-asserted-by":"crossref","first-page":"644","DOI":"10.1109\/TCST.2018.2877621","article-title":"Supervisory control of labeled transition systems subject to multiple reachability requirements via symbolic model checking","volume":"28","author":"Rawlings","year":"2020","journal-title":"IEEE Trans. Control. Syst. Technol."},{"key":"ref_4","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1016\/S0019-9958(86)80001-8","article-title":"Probabilistic propositional temporal logics","volume":"70","author":"Hart","year":"1986","journal-title":"Inf. Control."},{"key":"ref_5","unstructured":"Graf, S., and Schwartzbach, M. (2000). Symbolic model checking of probabilistic processes using mtbdds and the kronecker representation. Tools and Algorithms for the Construction and Analysis of Systems, Springer."},{"key":"ref_6","doi-asserted-by":"crossref","unstructured":"Degano, P., Gorrieri, R., and Marchetti-Spaccamela, A. (1997). Symbolic model checking for probabilistic processes. International Colloquium on Automata, Languages, and Programming, Springer.","DOI":"10.1007\/3-540-63165-8"},{"key":"ref_7","unstructured":"Baier, C., Ciesinski, F., and Grosser, M. (2004, January 23\u201325). Probmela: A Modeling Language for Communicating Probabilistic Processes. Proceedings of the Second ACM and IEEE International Conference on Formal Methods and Models for Co-Design, San Diego, CA, USA."},{"key":"ref_8","doi-asserted-by":"crossref","unstructured":"Baier, C., de Alfaro, L., Forejt, V., and Kwiatkowska, M. (2018). Model Checking Probabilistic Systems, Springer International Publishing.","DOI":"10.1007\/978-3-319-10575-8_28"},{"key":"ref_9","doi-asserted-by":"crossref","unstructured":"Brinksma, E., and Larsen, K.G. (2002). Xchek: A Multi-Valued Model-Checker. Computer Aided Verification, Springer.","DOI":"10.1007\/3-540-45657-0"},{"key":"ref_10","unstructured":"Chechik, M., Easterbrook, S., and Devereux, B. (2001, January 22\u201324). Model checking with multi-valued temporal logics. Proceedings of the 31st IEEE International Symposium on Multiple-Valued Logic, Warsaw, Poland."},{"key":"ref_11","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1016\/j.ins.2016.10.030","article-title":"Model checking of linear-time properties in multi-valued systems","volume":"377","author":"Li","year":"2017","journal-title":"Inf. Sci."},{"key":"ref_12","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_13","doi-asserted-by":"crossref","first-page":"842","DOI":"10.1109\/TFUZZ.2012.2232298","article-title":"Model checking of linear-time properties based on possibility measure","volume":"21","author":"Li","year":"2013","journal-title":"IEEE Trans. Fuzzy Syst."},{"key":"ref_14","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_15","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_16","doi-asserted-by":"crossref","unstructured":"Zhang, S., and Li, Y. (2016, January 24\u201329). Expressive power of linear-temporal logic based on generalized possibility measures. Proceedings of the 2016 IEEE International Conference on Fuzzy Systems (FUZZ-IEEE), Vancouver, BC, Canada.","DOI":"10.1109\/FUZZ-IEEE.2016.7737719"},{"key":"ref_17","doi-asserted-by":"crossref","first-page":"1452","DOI":"10.1016\/j.ijar.2013.06.004","article-title":"A fuzzy real-time temporal logic","volume":"54","year":"2013","journal-title":"Int. J. Approx. Reason."},{"key":"ref_18","doi-asserted-by":"crossref","first-page":"2017","DOI":"10.1109\/TFUZZ.2017.2760278","article-title":"\u03f5-bisimulation relations for fuzzy automata","volume":"26","author":"Yang","year":"2018","journal-title":"IEEE Trans. Fuzzy Syst."},{"key":"ref_19","doi-asserted-by":"crossref","first-page":"60","DOI":"10.1016\/j.fss.2014.07.008","article-title":"Model checking fuzzy computation tree logic","volume":"262","author":"Pan","year":"2015","journal-title":"Fuzzy Sets Syst."},{"key":"ref_20","doi-asserted-by":"crossref","first-page":"338","DOI":"10.1016\/S0019-9958(65)90241-X","article-title":"Fuzzy sets","volume":"8","author":"Zadeh","year":"1965","journal-title":"Inf. Cont."},{"key":"ref_21","doi-asserted-by":"crossref","unstructured":"Zimmermann, H.-J. (2001). Fuzzy Set Theory and Its Applications, Springer.","DOI":"10.1007\/978-94-010-0646-0"},{"key":"ref_22","doi-asserted-by":"crossref","first-page":"1","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_23","first-page":"175","article-title":"An algorithm to compute the transitive closure, a transitive approximation and a transitive opening of a proximity","volume":"16","year":"2009","journal-title":"Mathw. Soft Comput."},{"key":"ref_24","doi-asserted-by":"crossref","unstructured":"Zhang, P., Jiang, J., Ma, Z., and Zhu, H. (2019, January 5\u20138). Quantitative \u03bc-calculus model checking algorithm based on generalized possibility measures. Proceedings of the 2019 IEEE Intl Conference on Dependable, Autonomic and Secure Computing, International Conference on Pervasive Intelligence and Computing, International Conference on Cloud and Big Data Computing, International Conference on Cyber Science and Technology Congress (DASC\/PiCom\/CBDCom\/CyberSciTech), Fukuoka, Japan.","DOI":"10.1109\/DASC\/PiCom\/CBDCom\/CyberSciTech.2019.00091"},{"key":"ref_25","unstructured":"Choi, J., and Lee, K.Y. (2022). Fuzzy Decision Making for TEP, Wiley-IEEE Press."},{"key":"ref_26","doi-asserted-by":"crossref","first-page":"1899","DOI":"10.1109\/TFUZZ.2020.2988848","article-title":"Possibilistic fuzzy linear temporal logic and its model checking","volume":"29","author":"Li","year":"2021","journal-title":"IEEE Trans. Fuzzy Syst."},{"key":"ref_27","doi-asserted-by":"crossref","first-page":"4342","DOI":"10.1007\/s10489-020-01796-z","article-title":"A novel additive consistency for intuitionistic fuzzy preference relations in group decision making","volume":"50","author":"Yang","year":"2020","journal-title":"Appl. Intell."},{"key":"ref_28","doi-asserted-by":"crossref","first-page":"6224","DOI":"10.1007\/s10489-021-02216-6","article-title":"Decision making under measure-based granular uncertainty with intuitionistic fuzzy sets","volume":"51","author":"Xue","year":"2021","journal-title":"Appl. Intell."},{"key":"ref_29","unstructured":"Li, Y.M. (2005). Analysis of Fuzzy Systems, Science Press. (In Chinese)."},{"key":"ref_30","doi-asserted-by":"crossref","first-page":"837","DOI":"10.1007\/s10489-018-1292-1","article-title":"Programming model-based method for ranking objects from group decision making with interval-valued hesitant fuzzy preference relations","volume":"49","author":"Zhang","year":"2019","journal-title":"Appl. Intell."}],"container-title":["Entropy"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/1099-4300\/24\/9\/1183\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T00:14:52Z","timestamp":1760141692000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/1099-4300\/24\/9\/1183"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,8,24]]},"references-count":30,"journal-issue":{"issue":"9","published-online":{"date-parts":[[2022,9]]}},"alternative-id":["e24091183"],"URL":"https:\/\/doi.org\/10.3390\/e24091183","relation":{},"ISSN":["1099-4300"],"issn-type":[{"type":"electronic","value":"1099-4300"}],"subject":[],"published":{"date-parts":[[2022,8,24]]}}}