{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,3]],"date-time":"2025-12-03T18:57:06Z","timestamp":1764788226345,"version":"3.46.0"},"reference-count":34,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"4","license":[{"start":{"date-parts":[[2025,12,1]],"date-time":"2025-12-01T00:00:00Z","timestamp":1764547200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2025,12,1]],"date-time":"2025-12-01T00:00:00Z","timestamp":1764547200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2025,12,1]],"date-time":"2025-12-01T00:00:00Z","timestamp":1764547200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["62462036","62462037"],"award-info":[{"award-number":["62462036","62462037"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004479","name":"Natural Science Foundation of Jiangxi Province","doi-asserted-by":"publisher","award":["20242BAB26017"],"award-info":[{"award-number":["20242BAB26017"]}],"id":[{"id":"10.13039\/501100004479","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Cultivation Project for Academic and Technical Leader in Major Disciplines in Jiangxi Province of China","award":["20232BCJ22013"],"award-info":[{"award-number":["20232BCJ22013"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Rel."],"published-print":{"date-parts":[[2025,12]]},"DOI":"10.1109\/tr.2025.3607781","type":"journal-article","created":{"date-parts":[[2025,9,23]],"date-time":"2025-09-23T17:25:20Z","timestamp":1758648320000},"page":"4971-4984","source":"Crossref","is-referenced-by-count":0,"title":["Functional Modeling and Mechanized Verification of Bisimulations for NFTS"],"prefix":"10.1109","volume":"74","author":[{"ORCID":"https:\/\/orcid.org\/0009-0000-1076-9962","authenticated-orcid":false,"given":"Zhen","family":"You","sequence":"first","affiliation":[{"name":"School of Artificial Intelligence, Jiangxi Normal University, Nanchang, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-0721-483X","authenticated-orcid":false,"given":"Jiawei","family":"Wu","sequence":"additional","affiliation":[{"name":"School of Artificial Intelligence and Big Data, Jiangxi University of Technology, Nanchang, Jiangxi, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3601-4979","authenticated-orcid":false,"given":"Changjing","family":"Wang","sequence":"additional","affiliation":[{"name":"School of Artificial Intelligence, Jiangxi Normal University, Nanchang, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7118-3727","authenticated-orcid":false,"given":"Zhengkang","family":"Zuo","sequence":"additional","affiliation":[{"name":"School of Artificial Intelligence, Jiangxi Normal University, Nanchang, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref1","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-10235-3","volume-title":"A Calculus of Communicating Systems.","author":"Milner","year":"1980"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0017309"},{"key":"ref3","first-page":"1136","article-title":"A process algebra approach to fuzzy reasoning","volume-title":"Proc. Joint 2009 Int. Fuzzy Syst. Assoc. World Congr.; 2009 Eur. Soc. Fuzzy Log. Technol. Conf.","author":"Derrico","year":"2009"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1016\/j.knosys.2012.02.008"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1109\/TFUZZ.2011.2117431"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.2962"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1991.151651"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1016\/j.fss.2017.02.008"},{"issue":"6","key":"ref9","first-page":"138","article-title":"Comparison of two fuzzy bisimulations","volume-title":"Fuzzy Syst. Math.","volume":"29","author":"Wu","year":"2015"},{"issue":"1","key":"ref10","first-page":"35","article-title":"A local algorithm for fuzzy bisimulations","volume":"43","author":"Hu","year":"2023","journal-title":"J. Guilin Univ. Electron. Technol."},{"article-title":"The study of fuzzy bisimulation verifcation algorithm","year":"2021","author":"Hu","key":"ref11"},{"issue":"6","key":"ref12","first-page":"2113","article-title":"Preface of special topic on theorem proving theory and applications","volume":"33","author":"Cao","year":"2022","journal-title":"J. Softw."},{"issue":"1","key":"ref13","doi-asserted-by":"crossref","first-page":"82","DOI":"10.3724\/SP.J.1001.2012.04101","article-title":"Overview on mechanized theorem proving","volume":"31","author":"Jiang","year":"2020","journal-title":"J. Softw."},{"key":"ref14","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic.","author":"Nipkow","year":"2002"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2024.114876"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.09.014"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1016\/j.ins.2023.03.055"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(65)90241-X"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1109\/TFUZZ.2012.2230177"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1016\/j.ijar.2018.04.010"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1016\/j.fss.2015.09.012"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1109\/TFUZZ.2017.2670605"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1109\/TFUZZ.2020.2985000"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1016\/j.fss.2024.109194"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1109\/TFUZZ.2022.3227400"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1016\/j.fss.2023.108533"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1016\/j.jfranklin.2023.11.027"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1016\/j.ijar.2020.12.005"},{"article-title":"The calculus of communicating systems","year":"2012","author":"Bengtson","key":"ref29"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-5(2:16)2009"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2021.100642"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1109\/FUZZY.2008.4630561"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1109\/TFUZZ.2009.2035816"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1016\/j.fss.2011.07.003"}],"container-title":["IEEE Transactions on Reliability"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx8\/24\/11273031\/11176445.pdf?arnumber=11176445","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,12,3]],"date-time":"2025-12-03T18:42:08Z","timestamp":1764787328000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/11176445\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,12]]},"references-count":34,"journal-issue":{"issue":"4"},"URL":"https:\/\/doi.org\/10.1109\/tr.2025.3607781","relation":{},"ISSN":["0018-9529","1558-1721"],"issn-type":[{"type":"print","value":"0018-9529"},{"type":"electronic","value":"1558-1721"}],"subject":[],"published":{"date-parts":[[2025,12]]}}}