基于模糊决策过程的模糊计算树逻辑模型检测

计算机工程与科学 ›› 2022, Vol. 44 ›› Issue (02): 266-275.

基于模糊决策过程的模糊计算树逻辑模型检测

李召恺,马占有,李健祥,郭昊

(北方民族大学计算机科学与工程学院，宁夏银川 750021)

收稿日期:2021-10-09 修回日期:2021-11-12 接受日期:2022-02-25 出版日期:2022-02-25 发布日期:2022-02-17
基金资助:
国家自然科学基金(61962001)；宁夏自然科学基金(2018AAC03127)；北方民族大学引进人员科研项目 (2020KYQD14)

Model checking of fuzzy computation tree logic based on fuzzy decision process

LI Zhao-kai,MA Zhan-you,LI Jian-xiang,GUO Hao

(College of Computer Science and Engineering,North Minzu University,Yinchuan 750021,China)

Received:2021-10-09 Revised:2021-11-12 Accepted:2022-02-25 Online:2022-02-25 Published:2022-02-17

摘要/Abstract

摘要： 针对由数据表述产生的不确定性模糊系统的模型检测问题，给出模糊计算树逻辑模型检测算法。首先，引入模糊决策过程作为此类系统的模型，其最大特点是在迁移过程中对动作的不确定性选择和状态表述的模糊性。然后，在模糊决策过程基础上，给出模糊计算树逻辑的语法和语义。最后，给出模糊计算树逻辑模型检测算法，该算法是将模糊计算树逻辑模型检测问题转换为模糊矩阵的合成运算，其优势是时间复杂度低、计算过程较为简洁。

关键词: 模型检测, 不确定性系统, 模糊决策过程, 模糊计算树逻辑, 模糊矩阵

Abstract: Aiming at the model checking problem of uncertain fuzzy systems generated by data representation, a model checking algorithm of fuzzy computational tree logic is given.First of all, the fuzzy decision-making process is introduced as the model of this type of system. Its biggest feature is the uncertain choice of actions and the ambiguity of state expression during the migration process. Then, based on the fuzzy decision-making process, the grammar and semantics of fuzzy computation tree logic are given. Finally, a model detection algorithm of fuzzy computational tree logic is given. The algorithm is a synthetic operation that converts the model detection problem of fuzzy computational tree logic into a fuzzy matrix. Its advantages are low time complexity and a relatively simple calculation process.

Key words: model checking, nondeterministic system, fuzzy decision process, fuzzy computation tree logic, fuzzy matrix

李召恺, 马占有, 李健祥, 郭昊. 基于模糊决策过程的模糊计算树逻辑模型检测[J]. 计算机工程与科学, 2022, 44(02): 266-275.

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.

参考文献［22］

［1］	Baier C,Katoen J P.Principles of model checking［M］. Massachusetts:The MIT Press,2008.
［2］	Xie D,Wen X,Lei B,et al.Deriving unbounded reachability proof of linear hybrid automata during bounded checking procedure［J］.IEEE Transactions on Computers,2017,66(3):416-430.
［3］	Baier C,Alfaro L D,Forejt V,et al.Model checking probabilistic systems［M］∥Handbook of Model Checking.Berlin:Springer,2018:963-999.
［4］	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.
［5］	Li Y M, Li L J. Model checking of linear-time properties based on possibility measure［J］.IEEE Transactions on Fuzzy Systems,2013,21(5):842-854.
［6］	Li Y M,Ma Z Y.Quantitative computation tree logic model checking based on generalized possibility measures［J］.IEEE Transactions on Fuzzy Systems,2015,23(6):2034-2047.
［7］	Li Y M, Li Y L, Ma Z Y. Computation tree logic model checking based on possibility measures［J］.Fuzzy Sets & Systems,2015,262:44-59.
［8］	Li Y M,Lei L H,Li S J.Computation tree logic model check- ing based on multi-valued possibility measures［J］.Information Sciences,2019,485:87-113.
［9］	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.
［10］	Li Zhao-ni, Ma Zhan-you,Li Yong-ming.Research on management decision of project based on possibility measure［J］.Computer Science,2014,41(8):118-121.(in Chinese)
［11］	Li Y M.Quantitative model checking of linear-time properties based on generalized possibility measures［J］.Fuzzy Sets & Systems,2017,320:17-39.
［12］	Ma Zhan-you,Li Yong-ming.Model checking of reachability problems based on generalized possibility measures［J］.Fuzzy Systems and Mathematics,2014,28(6):88-97.(in Chinese)
［13］	Zhang S L, Li Y M.Expressive power of linear-temporal logic based on generalized possibility measures［C］∥Proc of 2016 IEEE International Conference on Fuzzy Systems,2016:431-436.
［14］	Ma Zhan-you, Li Yong-ming.Model checking generalized possibilistic computation tree logic based on decision pro-cesses［J］.Science China Information Sciences,2016,46(11):1591-1607.(in Chinese)
［15］	Liang Chang-jian,Li You-ming.Model checking of fuzzy linear temporal logic based on generalized possibility measures［J］.Acta Electronica Sinica,2017,45(12):2971-2977.(in Chinese)
［16］	Pan H Y,Li Y M,Cao Y Z,et al.Model checking fuzzy computation tree logic［J］.Fuzzy Sets and Systems,2015,262:60-77.
［17］	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.(in Chinese)
［18］	Fan Yan-huan,Li Yong-ming,Pan Hai-yu.Computation tree logic model checking for nondeterminisitc fuzzy Kripke structure［J］.Acta Electronica Sinica,2018,46(1):152-159.(in Chinese)
［19］	Intrigila B,Magazzeni D,Melatti I,et al.A model checking technique for the verification of fuzzy control systems［C］∥Proc of International Conference on Computational Intelligence for Modelling,Control & Automation,& International Conference on Intelligent Agents,Web Technologies & Internet Commerce,2006:536-542.
［20］	Ding Z, Yuan Z,Zhou M C.Stability analysis of switched fuzzy systems via model checking［J］.IEEE Transactions on Fuzzy Systems,2014,22(6):1503-1514.
［21］	Zadeh L A.Fuzzy sets［J］.Information & Control,1965,8(3):338-353.
［22］	Li Yong-ming.Fuzzy system analysis［M］.Beijing:Science Press,2005.(in Chinese)
［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］.Mathware & Soft Computing,2007,16(2):175-191.
	附中文参考文献：
［10］	李召妮,马占有,李永明.基于可能性测度的工程管理决策的研究［J］.计算机科学,2014,41(8):118-121.
［12］	马占有,李永明.基于广义可能性测度的可达性问题的模型检测［J］.模糊系统与数学,2014,28(6):88-97.
［14］	马占有,李永明.基于决策过程的广义可能性计算树逻辑模型检测［J］.中国科学:信息科学,2016,46(11):1591-1607.
［15］	梁常建,李永明.具有模糊时态的广义可能性线性时序逻辑的模型检测［J］.电子学报,2017,45(12):2971-2977.
［17］	潘海玉,张敏,陈仪香.基于模糊逻辑的几类Kripke结构之间的关系［J］.计算机科学,2013,40(5):42-44.
［18］	范艳焕,李永明,潘海玉.不确定型模糊Kripke结构的计算树逻辑模型检测［J］.电子学报,2018,46(1):152-159.
［22］	李永明.模糊系统分析［M］.北京：科学出版社,2005.

[1]	郑小宇, 刘冬梅, 杜益宁, 周子健, 邱玫媚, 朱鸿. 模式驱动的系统安全性设计的验证[J]. 计算机工程与科学, 2020, 42(07): 1197-1207.
[2]	袁申,魏杰林,李永明. 具有多值决策过程的广义可能性计算树逻辑模型检测[J]. 计算机工程与科学, 2019, 41(01): 88-97.
[3]	钟小妹，肖美华，李伟，谌佳，李娅楠. RFID超轻量级认证协议RCIA形式化分析与改进[J]. 计算机工程与科学, 2018, 40(12): 2183-2192.
[4]	王亚鹏，雷丽晖. 基于CTL模型检测的胃腺癌核心路径形式化验证[J]. 计算机工程与科学, 2018, 40(12): 2280-2286.
[5]	雷丽晖，郭越，张延波. 可能性测度下的CTL符号化模型检测[J]. 计算机工程与科学, 2018, 40(11): 2008-2014.
[6]	肖美华1，梅映天1,2，李伟1，李娅楠1，钟小妹1，宋子繁1. 基于时间戳私钥签名技术的Nayak-T协议安全性分析[J]. 计算机工程与科学, 2017, 39(12): 2252-2259.
[7]	袁红娟1,2,马艳芳3,潘海玉1,2. 模糊交互时态逻辑的模型检测[J]. 计算机工程与科学, 2017, 39(12): 2290-2296.
[8]	吴格格，庄雷，张坤丽，王国卿. 移动支付协议PCMS的形式化分析和验证[J]. 计算机工程与科学, 2017, 39(01): 67-73.
[9]	程道雷,肖美华,刘欣倩,梅映天,李伟. 运用SPIN对开放授权协议OAuth 2.0的分析与验证[J]. J4, 2015, 37(11): 2121-2127.
[10]	马占有1，2，李永明1. 广义可能性决策过程的计算树逻辑模型检测[J]. J4, 2015, 37(11): 2162-2168.
[11]	刘姣，雷丽晖. 一种基于扩展不完全Kripke结构的三值逻辑模型检测方法[J]. J4, 2015, 37(10): 1884-1889.
[12]	徐亮，刘宏. 基于SMT的TECTL性质的限界模型检测方法[J]. J4, 2013, 35(10): 166-171.
[13]	周璇,汪学明. 微支付协议Millicent的改进与模型检测[J]. J4, 2012, 34(12): 22-26.
[14]	陈国彬1，任〓强2,张广泉2,3. 一种基于抽象与精化技术的Web服务组合验证方法[J]. J4, 2011, 33(9): 76-80.
[15]	龙士工，王扣武. 多智体系统时序认知规范的SPIN模型检测[J]. J4, 2011, 33(12): 12-16.