Fuzzy computation tree logic* model checking based on fuzzy measures

Abstract

Abstract: A fuzzy computation tree logic* model checking algorithm based on fuzzy measures is proposed for the verification problem of complex systems with fuzziness and uncertainty. Firstly, the syntax and semantics of fuzzy computation tree logic* are introduced based on fuzzy decision process model. Secondly, a fuzzy computation tree logic* model checking algorithm is proposed, which transforms the model checking problem into matrix operation and has the advantages of simplicity of computation and lower complexity. Finally, a medical expert system example is given to illustrate the effectiveness of the model checking algorithm.

Key words: fuzzy decision process, fuzzy measure, fuzzy computation tree logic*, model checking, matrix operation

LIU Zi-yuan, MA Zhan-you, LI Xia, GAO Ying-nan, HE Na-na, HUANG Rui-qi. Fuzzy computation tree logic* model checking based on fuzzy measures[J]. Computer Engineering & Science, 2024, 46(04): 676-683.

References ［23］

［1］	Baier C,Katoen J P.Principles of model checking［M］.Cambridge:MIT Press,2008.
［2］	Edmund M, Grumberg O, Peled D. Model checking［M］.Cambridge:MIT Press,1999.
［3］	马占有,李永明.基于决策过程的广义可能性计算树逻辑模型检测［J］.中国科学:信息科学,2016,46(11):1591-1607.
	Ma Zhan-you,Li Yong-ming.Model checking generalized possibilistic computation tree logic based on decision processes ［J］.SCIENTIA SINICA Informationis,2016,46(11):1591-1607.
［4］	杨维禹,刘文奇.基于量子逻辑的模糊线性时序逻辑的模型检测［J］.模糊系统与数学,2021,35(1):9-21.
	Yang Wei-yu,Liu Wen-qi.Model checking of fuzzy linear sequential logic based on quantum logic ［J］.Fuzzy Systems and Mathematics,2021,35(1):9-21.
［5］	李永明.可能LTL模型检测的两种方法［J］.陕西师范大学学报(自然科学版),2014,42(6):21-25.
	Li Yong-ming.Two methods of possible LTL model checking ［J］.Journal of Shaanxi Normal University (Natural Science Edition),2014,42(6):21-25.
［6］	袁冠杰.公平约束条件下的CTL模型检测及其扩展应用研究［D］.贵阳:贵州大学,2017.
	Yuan Guan-jie.Research on CTL model checking under fair-ness constraints and its extended application ［D］.Guiyang:Guizhou University,2017.
［7］	Hart S,Sharir M.Probabilistic propositional temporal logics［J］.Information and Control,1986,70(2-3):97-155.
［8］	Chechik M,Devereux B,Easterbrook S,et al.Multi-valued symbolic model-checking［J］.ACM Transactions on Software Engineering Methodology,2003,12(4):371-408.
［9］	Chechik M,Gurfinkel A,Devereux B,et al.Data structures for symbolic multi-valued model-checking［J］.Formal Methods in System Design,2006,29(3):295-344.
［10］	李召恺,马占有,李健祥,等.基于模糊决策过程的模糊计算树逻辑模型检测［J］.计算机工程与科学,2022,44(2):266-275.
	Li Zhao-kai,Ma Zhan-you,Li Jian-xiang,et al.Model checking of fuzzy computation tree logic based on fuzzy decision process［J］.Computer Engineering & Science,2022,44(2):266-275.
［11］	Li Y M,Li L J. Model checking of linear-time propertiesbased on possibility measure ［J］.IEEE Transactions on Fuzzy Systems,2013,21(5):842-854.
［12］	Li Y M, Li Y L,Ma Z Y.Computation tree logic model che-cking based on possibility measures［J］.Fuzzy Sets and Systems,2015,262(C):44-59.
［13］	Li Y M,Lei L H,Li S J.Computation tree logic model checking based on multi-valued possibility measures［J］.Information Sciences,2019,485:87-113.
［14］	Li Y M,Wei J L.Possibilistic fuzzy linear temporal logic and its model checking ［J］.IEEE Transactions on Fuzzy Systems,2021,29(7):1899-1913.
［15］	范艳焕,李永明.模糊线性时序逻辑的可实现性［J］.电子学报,2018,46(2):341-346.
	Fan Yan-huan,Li Yong-ming. The realizability of fuzzy linear temporal logic ［J］.Electronics,2018,46(2):341-346.
［16］	范艳焕,李永明,潘海玉.不确定型模糊Kripke结构的计算树逻辑模型检测［J］.电子学报,2018,46(1):152-159.
	Fan Yan-huan,LI Yong-ming,Pan Hai-yu.Computational tree logic model detection of uncertain fuzzy Kripke structures ［J］.Acta Electronica Sinica,2018,46(1):152-159.
［17］	潘海玉,张敏,陈仪香.基于模糊逻辑的几类Kripke结构之间的关系［J］.计算机科学,2013,40(5):42-44.
	Pan Hai-yu,Zhang Min,Chen Yi-xiang.Relationships among several types of Kripke structures based on fuzzy logic ［J］.Computer Science,2013,40(5):42-44.
［18］	Pan H Y,Li Y M,Cao Y Z,et al.Model checking fuzzy computation tree logic ［J］.Fuzzy Sets and Systems,2015,262(C):60-77.
［19］	马占有.基于决策过程的广义可能性时态逻辑模型检测［D］.西安:陕西师范大学,2017.
	Ma Zhan-zhou.Generalized possibility temporal logic model detection based on decision process ［D］.Xi’an:Shaanxi Normal University,2017.
［20］	Zadeh L A.Fuzzy sets［J］.Information & Control,1965,8 (3):338-353.
［21］	李永明.模糊系统分析［M］.北京:科学出版社,2005.
	Li Yong-ming.Fuzzy system analysis［M］. Beijing:Science Press,2005.
［22］	张所娟,黄松,余晓晗,等.基于模糊测度的知识关联性建模方法［J］.模式识别与人工智能,2022,35(2):95-105.
	Zhang Suo-juan,Huang Song,Yu Xiao-han,et al.Knowledge association modeling method based on fuzzy measure ［J］.Pattern Recognition and Artificial Intelligence,2022,35(2):95-105.
［23］	Garmendia L,González R,Ferrés J R.An algorithm to compute the transitive closure,a transitive approximation and a transitive opening of a proximity［J］.［EB/OL］.［2009-12-31］. https://upcommons.upc.edu/bitstream/handle/2117/6638/FLINS2008.pdf;sequence=1.

[1]	LI Zhao-kai, MA Zhan-you, LI Jian-xiang, GUO Hao. Model checking of fuzzy computation tree logic based on fuzzy decision process [J]. Computer Engineering & Science, 2022, 44(02): 266-275.
[2]	ZHENG Xiao-yu, LIU Dong-mei, DU Yi-ning, ZHOU Zi-jian, QIU Mei-mei, ZHU Hong. Verification of pattern driven system security design [J]. Computer Engineering & Science, 2020, 42(07): 1197-1207.
[3]	YUAN Shen,WEI Jielin,LI Yongming. Model checking of generalized possibilistic computation tree logic with multi-valued decision process [J]. Computer Engineering & Science, 2019, 41(01): 88-97.
[4]	ZHONG Xiaomei，XIAO Meihua，LI Wei，CHEN Jia，LI Yanan. Formal analysis and improvement of RCIA: An ultra-lightweight RFID- mutual authentication protocol [J]. Computer Engineering & Science, 2018, 40(12): 2183-2192.
[5]	WANG Yapeng，LEI Lihui. Formal verification of gastric adenocarcinoma core pathway based on CTL model checking [J]. Computer Engineering & Science, 2018, 40(12): 2280-2286.
[6]	LEI Lihui，GUO Yue，ZHANG Yanbo. Symbolic CTL model checking based on possibility measure [J]. Computer Engineering & Science, 2018, 40(11): 2008-2014.
[7]	XIAO Mei-hua1,MEI Ying-tian1,2,LI Wei1,LI Ya-nan1,ZHONG Xiao-mei1,SONG Zi-fan1. Security analysis of Nayak-T protocol based on time stamp and private key signature [J]. Computer Engineering & Science, 2017, 39(12): 2252-2259.
[8]	YUAN Hong-juan1,2,MA Yan-fang3,PAN Hai-yu1,2. Model checking for fuzzy alternating-time temporal logic [J]. Computer Engineering & Science, 2017, 39(12): 2290-2296.
[9]	LIN Zhe-chao，DONG Wei. Implementation and optimization of LTL probabilistic model checker [J]. Computer Engineering & Science, 2017, 39(05): 892-896.
[10]	WU Gege，ZHUANG Lei，ZHANG Kunli，WANG Guoqing. Formal analysis and verification of mobile payment protocol PCMS [J]. Computer Engineering & Science, 2017, 39(01): 67-73.
[11]	CHENG Daolei,XIAO Meihua,LIU Xinqian,MEI Yingtian,LI Wei. Analyzing and verifying an open authorization protocol OAuth 2.0 with SPIN [J]. J4, 2015, 37(11): 2121-2127.
[12]	MA Zhanyou1，2，LI Yongming1. Computation tree logic model checking for generalized possibilistic decision processes [J]. J4, 2015, 37(11): 2162-2168.
[13]	LIU Jiao,LEI Lihui. A threevalued logic model checking approach based on extensional partial Kripke structure [J]. J4, 2015, 37(10): 1884-1889.
[14]	XU Liang，LIU Hong. Bounded model checking of TECTL properties based on SMT [J]. J4, 2013, 35(10): 166-171.
[15]	ZHOU Xuan,WANG Xueming. Improvement and Model Checking of Micro-Payment Protocol Millicent [J]. J4, 2012, 34(12): 22-26.

Fuzzy computation tree logic* model checking based on fuzzy measures

PDF

Knowledge

Abstract

Cite this article

share this article

References ［23］

Related Articles 15

Recommended Articles

Metrics

Comments