不确定型模糊Kripke结构的计算树逻辑模型检测

doi:10.3969/j.issn.0372-2112.2018.01.021

电子学报 ›› 2018, Vol. 46 ›› Issue (1): 152-159.DOI: 10.3969/j.issn.0372-2112.2018.01.021

不确定型模糊Kripke结构的计算树逻辑模型检测

范艳焕^1,2, 李永明¹, 潘海玉^1,3

1. 陕西师范大学计算机科学学院, 陕西西安 710062;
2. 青海师范大学民师院数学系, 青海西宁 810008;
3. 泰州学院计算机科学与技术学院, 江苏泰州 225300

收稿日期:2017-05-19 修回日期:2017-08-14 出版日期:2018-01-25
- 通讯作者:
- 李永明
- 作者简介:
- 范艳焕,女,1987年生于河南商丘.现为陕西师范大学计算机科学学院博士研究生.主要研究方向为定量模型检测.E-mail:fan.fan1222@163.com
- 基金资助:
- 国家自然科学基金 (No.11671244，No.61261047，No.61672023，No.61673352）; 教育部博士点基金 (No.20130202110001）; 青海省自然科学基金 (No.2014-ZJ-908）; 江苏高校"青蓝工程"

Computation Tree Logic Model Checking for Nondeterminisitc Fuzzy Kripke Structure

FAN Yan-huan^1,2, LI Yong-ming¹, PAN Hai-yu^1,3

1. College of Computer Science, Shaanxi Normal University, Xi'an, Shaanxi 710062, China;
2. Department of Mathematics in National Normal College, Qinghai Normal University, Xining, Qinghai 810008, China;
3. College of Computer Science and Technology, Taizhou University, Taizhou, Jiangsu 225300, China

Received:2017-05-19 Revised:2017-08-14 Online:2018-01-25 Published:2018-01-25
- Supported by:
- National Natural Science Foundation of China (No.11671244, No.61261047, No.61672023, No.61673352); Ph.D. Programs Foundation of Ministry of Education of China (No.20130202110001); Natural Science Foundation of Qinghai Province (No.2014-ZJ-908); Blue Project in Jiangsu Province

摘要/Abstract

摘要： 本文研究了不确定型模糊Kripke结构的计算树逻辑的模型检测问题，并说明了该问题可以在对数多形式时间内解决.首先给出了不确定型模糊Kripke结构的定义，引入了模糊计算树逻辑的语法和语义.为了刻画存在量词∃和任意量词∀在不确定型模糊Kripke结构中的两种语义解释，在模糊计算树逻辑语法中引入了路径量词∃_sup，∃_inf和∀_sup，∀_inf，分别用于替换存在量词∃和任意量词∀.其次讨论了基于不确定型模糊Kripke结构的计算树逻辑模型检测算法，特别地对于模糊计算树逻辑公式∃_suppUq，∀_suppUq，∃_infpUq和∀_infpUq分别给出时间复杂度为对数多项式时间的改进算法.

关键词: 模型检测, 计算树逻辑, 模糊逻辑, Kripke结构, 时态逻辑

Abstract: This paper studys model-checking problem for FCTL (fuzzy computation tree logic) over nondeterministic fuzzy system and shows that it can be solved in linear-logarithmic running time in the size of the system. Firstly, we introduce NFKS (nondeterministic fuzzy kripke structure) which is adapted to model nondeterministic fuzzy system. The syntax and semantics of fuzzy computation tree logic over NFKS are presented. For describing two kinds of semantic explanation, we use path quantifiers ∃_sup, ∃_inf and ∀_sup, ∀_inf as substitutes for an existential path quantifier ∃ and a universal path quantifier ∀ in the syntax of the CTL. Then, we study the model checking algorithm for fuzzy computation tree logic over NFKS. Furthermore, the improvement algorithms for FCTL formuleas ∃_suppUq, ∀_suppUq, ∃_infpUq and ∀_infpUq are given, whose time complexities are linear-logarithmic running time in the size of the system.

Key words: model checking, computation tree logic, fuzzy logic, Kripke structure, temporal logic

中图分类号:

TP301.2

范艳焕, 李永明, 潘海玉. 不确定型模糊Kripke结构的计算树逻辑模型检测[J]. 电子学报, 2018, 46(1): 152-159.

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.

参考文献

[1] Christe B,Joost P K.Principles of Model Checking[M].Cambridge:The MIT Press,2008.
[2] 林慧民,张文辉.模型检测:理论、方法与应用[J].电子学报,2002,36(12A):1907-1912. LIN Hui-min,ZHANG Wen-hui.Model checking:Theories,techniques and applications[J].Acta Electronica Sinica,2002,36(12A):1907-1912.(in Chinese)
[3] Pnueli A.The temporal logic of programs[A].Proceedings of the 18th IEEE Symposium on Foundations of Computer Science[C].USA:IEEE,2017.46-67.
[4] 朱维军,周清雷,李永亮.以DNA为载体的线性时序逻辑模型检测[J].电子学报,2016,44(6):1265-1271. Zhu Wei-jun,Zhou Qing-lei,Li Yong-liang.Conduct linear temporal logic model checking via DNA molecules[J].Acta Electronica Sinica,2016,44(6):1265-1271.(in Chinese)
[5] Glenn B,Patrice G.Model checking with multi-valued modal logic[A].Proceedings of the 31st International Colloquium Automata,Languages and Programming[C].Turku,Finland,2004.281-293.
[6] Marsha C,Benet D,Steve E,Arie G.Multi-valued symbolic model-checking[J].ACM Transactions on Software Engineering and Methodology,2003,12(C):371-408.
[7] Yong M Li,Manfred D,Li H L.Model checking of linear-time properties based on multi-valued systems[J].Information Sciences,2017,377:51-74.
[8] Yong M Li,Li J Li.Model checking of linear-time properties based on possibility measures[J].IEEE Transactions on Fuzzy Systems,2013,21(5):842-854.
[9] Yong M Li,Ya L Li,Zhan Y Ma.Computation tree logic model checking based on possibility measures[J].Fuzzy Sets and Systems,2015,262(C):44-59.
[10] Yong M Li,Zhan Y Ma.Quantitative computation tree logic model checking based on generalized possibility measures[J].IEEE Transactions on Fuzzy Systems,2015,23(C):2034-2047.
[11] Li Y M.Quantitative Model checking of linear-time properties based on generalized possibility measures[J].Fuzzy Sets and Systems,2017,320(C):17-39.
[12] Seong-ick M,Ko-Hsin L,Doheo L.Fuzzy branching temporal logic[J].IEEE Transactions on System,Man and Cybernetics,Part B(Cybernetics),2004,34(2):1045-1055.
[13] Subhankar M,Pallab D.A fuzzy real-time temporal logic[J].International Journal of Approximate Reasoning,2013,54(9):1452-1470.
[14] Pan H Y,Li Y M,Cao Y Z C,Ma Z Y.Model checking fuzzy computation tree logic[J].Fuzzy Sets and Systems,2015,262(C):60-77.
[15] Pan H Y,Li Y M,Cao Y Z,Ma Z Y.Model checking computation tree logic over finite lattices[J].Theoretical Computer Scinece,2016,612(C):45-62.
[16] Li Y M.Finite automata theory with membership valued in lattice[J].Information Science,2011,181(C):1003-1017.
[17] Cao Y Z,Yoshinoru E.Nondeterministic fuzzy automata[J].Information Sciences,2012,191(C):86-97.
[18] 李永明,李平.模糊计算理论[M].北京:科学出版社,2016.
[19] 马占有,李永明.基于决策过程的广义可能性计算树逻辑模型检测[J].中国科学:信息科学,2016,46(11):1591-1607. MA Zhan-you,LI Yong-ming.Computation tree logic model checking for generalized possibilistic decision processes[J]. Scientia Sinica(Informationis),2016,46(11):1591-1607.(in Chinese)
[20] 郦丽,沈应兄,潘海玉.不确定多值Kripke结构的模型检测[J].模糊系统与数学,2016,30(5):60-70. Li L,Shen Y X,Pan H Y.Nondeterministic multi-valued Kripke structure model checking[J].Fuzzy Systems and Sets,2016,30(5):60-70.(in Chinese)
[21] Lotfi A Z.Fuzzy sets[J].Information and Control,1965,8(C):338-353.
[22] Alfred T.A lattice-theoretical fixpoint theorem and its applications[J].Pacific Journal of Mathematics,1955,5(2):285-309.
[23] Luca D A,Marco F,Thomas A H,et al.Model checking discounted temporal proerties[J].Theoretical Computer Science,2005,345(C):139-170.
[24] Pan H Y,Li Y M,Cao Y Z,et.al.Reachability in fuzzy game graphs[J].IEEE Transactions on Systems,2017,25(4):972-984.

不确定型模糊Kripke结构的计算树逻辑模型检测

Computation Tree Logic Model Checking for Nondeterminisitc Fuzzy Kripke Structure

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics

[1]	王舜, 杜晔, 韩臻. 基于模块化Abstract-Refine算法框架的软件模型检测方法[J]. 电子学报, 2020, 48(5): 997-1002.
[2]	梁常建, 李永明. 具有模糊时态的广义可能性线性时序逻辑的模型检测[J]. 电子学报, 2017, 45(12): 2971-2977.
[3]	梁常建, 李永明. 广义可能性计算树逻辑的模型检测问题[J]. 电子学报, 2017, 45(11): 2641-2648.
[4]	朱维军, 周清雷, 李永亮. 以DNA为载体的线性时序逻辑模型检测[J]. 电子学报, 2016, 44(6): 1265-1271.
[5]	周开军, 桂卫华, 阳春华, 谢永芳. 基于模糊三值模式的矿物浮选泡沫图像边缘检测方法[J]. 电子学报, 2014, 42(4): 658-665.
[6]	罗成, 谢维信. 传感器网络拥塞避免与控制的模糊AQM算法[J]. 电子学报, 2014, 42(4): 679-684.
[7]	林运国, 雷红轩, 李永明. 量子马尔可夫链安全性模型检测[J]. 电子学报, 2014, 42(11): 2191-2197.
[8]	刘志锋, 孙博, 周从华. 概率实时时态认知逻辑模型检测中抽象技术的研究[J]. 电子学报, 2013, 41(7): 1343-1351.
[9]	杜贞斌;宋宜斌. 基于模糊逼近的非线性多时延系统的自适应跟踪控制[J]. 电子学报, 2012, 40(5): 897-900.
[10]	周从华, 孙博, 刘志锋, 葛云. 概率时态认知逻辑模型检测中三值抽象技术的研究[J]. 电子学报, 2012, 40(10): 2052-2061.
[11]	王曦;徐中伟. 基于启发式SCCs的广义Büchi 自动机判空检测算法[J]. 电子学报, 2012, 40(1): 95-102.
[12]	张广泉;戎玫;朱雪阳;何亚丽;石慧娟. 基于XYZ/ADL的Web服务组合描述与验证[J]. 电子学报, 2011, 39(3A): 86-93.
[13]	尹传龙;庄雷;王从银;. 实时模型检测中基于驻留环的精确加速[J]. 电子学报, 2011, 39(3): 489-493.
[14]	张广泉;戎玫;王 Sheng. 时间感知Web服务交互行为建模与失配检测方法研究[J]. 电子学报, 2011, 39(11): 2568-2575.
[15]	吴洪博;张琼. NMŁ系统的有限强完备性[J]. 电子学报, 2010, 38(6): 1414-1418.