{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,2]],"date-time":"2026-05-02T07:08:23Z","timestamp":1777705703801,"version":"3.51.4"},"reference-count":23,"publisher":"SAGE Publications","issue":"5","license":[{"start":{"date-parts":[[2023,5,4]],"date-time":"2023-05-04T00:00:00Z","timestamp":1683158400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IFS"],"published-print":{"date-parts":[[2023,5,4]]},"abstract":"<jats:p>The verification of reachability properties of fuzzy systems is usually based on the fuzzy Kripke structure or possibilistic Kripke structure. However, fuzzy Kripke structure or possibilistic Kripke structure is not enough to describe nondeterministic and concurrent fuzzy systems in real life. In this paper, firstly, we propose the generalized possibilistic decision process as the model of nondeterministic and concurrent fuzzy systems, and deduce the possibilities of sets of paths of the generalized possibilistic decision process relying on defining of schedulers. Then, we give fuzzy matrices calculation methods of the maximal possibilities and the minimal possibilities of eventual reachability, always reachability, constrained reachability, repeated reachability and persistent reachability. Finally, we propose a model checking approach to convert the verification of safety property into the analysis of reachabilities.<\/jats:p>","DOI":"10.3233\/jifs-222803","type":"journal-article","created":{"date-parts":[[2023,3,3]],"date-time":"2023-03-03T10:48:59Z","timestamp":1677840539000},"page":"8357-8373","source":"Crossref","is-referenced-by-count":3,"title":["Quantitative reachability analysis of generalized possibilistic decision processes"],"prefix":"10.1177","volume":"44","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1016-6608","authenticated-orcid":false,"given":"Zhanyou","family":"Ma","sequence":"first","affiliation":[{"name":"School of Computer Science and Engineering, North Minzu University, Yinchuan, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yingnan","family":"Gao","sequence":"additional","affiliation":[{"name":"School of Computer Science and Engineering, North Minzu University, Yinchuan, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhaokai","family":"Li","sequence":"additional","affiliation":[{"name":"School of Computer Science and Engineering, North Minzu University, Yinchuan, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xia","family":"Li","sequence":"additional","affiliation":[{"name":"School of Computer Science and Engineering, North Minzu University, Yinchuan, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ziyuan","family":"Liu","sequence":"additional","affiliation":[{"name":"School of Computer Science and Engineering, North Minzu University, Yinchuan, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"179","reference":[{"key":"10.3233\/JIFS-222803_ref2","doi-asserted-by":"crossref","first-page":"60","DOI":"10.1016\/j.fss.2014.07.008","article-title":"Model checking fuzzy computation tree logic[J]","volume":"262","author":"Pan","year":"2015","journal-title":"Fuzzy sets and Systems"},{"issue":"5","key":"10.3233\/JIFS-222803_ref3","doi-asserted-by":"crossref","first-page":"615","DOI":"10.1093\/comjnl\/bxp025","article-title":"Principles of Model Checking[J]","volume":"53","author":"Laroussinie","year":"2010","journal-title":"The Computer Journal"},{"issue":"12","key":"10.3233\/JIFS-222803_ref4","doi-asserted-by":"crossref","first-page":"2511","DOI":"10.1016\/j.scico.2013.02.007","article-title":"Reachability analysis of complex planar hybrid systems[J]","volume":"78","author":"Hansen","year":"2013","journal-title":"Science of Computer Programming"},{"issue":"5","key":"10.3233\/JIFS-222803_ref6","doi-asserted-by":"publisher","first-page":"725","DOI":"10.1109\/3477.875448","article-title":"Reachability analysis of real-time systems using time Petri nets","volume":"30","author":"Wang","year":"2000","journal-title":"IEEE Trans Syst Man Cybern B Cybern"},{"issue":"3","key":"10.3233\/JIFS-222803_ref8","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[J]","volume":"66","author":"Xie","year":"2016","journal-title":"IEEE Transactions on Computers"},{"issue":"5","key":"10.3233\/JIFS-222803_ref10","doi-asserted-by":"crossref","first-page":"2688","DOI":"10.1002\/joc.7386","article-title":"Differences in multi-model ensembles of CMIP5 and CMIP6 projections for future droughts in South Korea[J]","volume":"42","author":"Song","year":"2022","journal-title":"International Journal of Climatology"},{"key":"10.3233\/JIFS-222803_ref11","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[J]","volume":"377","author":"Li","year":"2017","journal-title":"Information Sciences"},{"issue":"9","key":"10.3233\/JIFS-222803_ref12","doi-asserted-by":"crossref","first-page":"1183","DOI":"10.3390\/e24091183","article-title":"Model Checking Fuzzy Computation Tree Logic Based on Fuzzy Decision Processes with Cost[J]","volume":"24","author":"Ma","year":"2022","journal-title":"Entropy"},{"key":"10.3233\/JIFS-222803_ref13","doi-asserted-by":"crossref","first-page":"158738","DOI":"10.1109\/ACCESS.2021.3130569","article-title":"Directed Model Checking for Fast Abstract Reachability Analysis[J]","volume":"9","author":"Lee","year":"2021","journal-title":"IEEE Access"},{"issue":"8-9","key":"10.3233\/JIFS-222803_ref15","doi-asserted-by":"crossref","first-page":"945","DOI":"10.1016\/j.artint.2007.12.002","article-title":"Reachability analysis of uncertain systems using bounded-parameter Markov decision processes[J]","volume":"172","author":"Wu","year":"2008","journal-title":"Artificial Intelligence"},{"issue":"8-9","key":"10.3233\/JIFS-222803_ref16","doi-asserted-by":"crossref","first-page":"945","DOI":"10.1016\/j.artint.2007.12.002","article-title":"Reachability analysis of uncertain systems using bounded-parameter Markov decision processes[J]","volume":"172","author":"Wu","year":"2008","journal-title":"Artificial Intelligence"},{"issue":"5","key":"10.3233\/JIFS-222803_ref17","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[J]","volume":"21","author":"Li","year":"2012","journal-title":"IEEE Transactions on Fuzzy Systems"},{"issue":"7","key":"10.3233\/JIFS-222803_ref18","doi-asserted-by":"crossref","first-page":"1899","DOI":"10.1109\/TFUZZ.2020.2988848","article-title":"Possibilistic fuzzy linear temporal logic and itsmodel checking[J]","volume":"29","author":"Li","year":"2020","journal-title":"IEEE Transactions on Fuzzy Systems"},{"issue":"7","key":"10.3233\/JIFS-222803_ref19","doi-asserted-by":"crossref","first-page":"2594","DOI":"10.3390\/app10072594","article-title":"The \u03bc-calculus model-checkingalgorithm for generalized possibilistic decision process[J]","volume":"10","author":"Jiang","year":"2020","journal-title":"Applied Sciences"},{"key":"10.3233\/JIFS-222803_ref20","doi-asserted-by":"crossref","first-page":"577","DOI":"10.1016\/j.tcs.2019.09.021","article-title":"Model-checking graded computation-tree logic with finite path semantics[J]","volume":"806","author":"Am","year":"2020","journal-title":"Theoretical Computer Science"},{"key":"10.3233\/JIFS-222803_ref21","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1016\/j.fss.2017.03.012","article-title":"Quantitative model checking of linear-time properties based on generalized possibility measures[J]","volume":"320","author":"Li","year":"2017","journal-title":"Fuzzy sets and Systems"},{"issue":"6","key":"10.3233\/JIFS-222803_ref22","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[J]","volume":"23","author":"Li","year":"2015","journal-title":"IEEE Transactions on Fuzzy Systems"},{"key":"10.3233\/JIFS-222803_ref23","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1016\/j.ic.2018.09.001","article-title":"Reachability analysis of quantum Markov decision processes[J],","volume":"263","author":"Ying","year":"2018","journal-title":"Information and Computation"},{"key":"10.3233\/JIFS-222803_ref24","doi-asserted-by":"crossref","first-page":"100743","DOI":"10.1016\/j.jlamp.2021.100743","article-title":"A tableau construction for finite linear-time temporal logic[J]","volume":"125","author":"Huang","year":"2022","journal-title":"Journal of Logical and Algebraic Methods in Programming"},{"issue":"2","key":"10.3233\/JIFS-222803_ref26","doi-asserted-by":"crossref","first-page":"829","DOI":"10.1007\/s10586-014-0420-x","article-title":"FUGE: A joint meta-heuristic approach to cloud job scheduling algorithm using fuzzy theory and a genetic method[J]","volume":"18","author":"Shojafar","year":"2015","journal-title":"Cluster Computing"},{"key":"10.3233\/JIFS-222803_ref27","doi-asserted-by":"crossref","first-page":"34","DOI":"10.1016\/j.ins.2017.10.015","article-title":"Fuzzy alternating automata over distributive lattices[J]","volume":"425","author":"Wei","year":"2018","journal-title":"Information Sciences"},{"key":"10.3233\/JIFS-222803_ref29","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2021.3117506"},{"issue":"2","key":"10.3233\/JIFS-222803_ref30","first-page":"175","article-title":"An algorithm to compute the transitive closure, a transitive approximation and a transitive opening of a fuzzy proximity[J]","volume":"16","author":"Garmendia","year":"2009","journal-title":"Mathware and Soft Computing"}],"container-title":["Journal of Intelligent &amp; Fuzzy Systems"],"original-title":[],"link":[{"URL":"https:\/\/content.iospress.com\/download?id=10.3233\/JIFS-222803","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T09:44:50Z","timestamp":1777455890000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/full\/10.3233\/JIFS-222803"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,5,4]]},"references-count":23,"journal-issue":{"issue":"5"},"URL":"https:\/\/doi.org\/10.3233\/jifs-222803","relation":{},"ISSN":["1064-1246","1875-8967"],"issn-type":[{"value":"1064-1246","type":"print"},{"value":"1875-8967","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,5,4]]}}}