广义可能性计算树逻辑的模型检测问题

doi:10.3969/j.issn.0372-2112.2017.11.010

电子学报 ›› 2017, Vol. 45 ›› Issue (11): 2641-2648.DOI: 10.3969/j.issn.0372-2112.2017.11.010

广义可能性计算树逻辑的模型检测问题

梁常建^1,2, 李永明¹

1. 陕西师范大学数学与信息科学学院, 陕西西安 710119;
2. 商丘师范学院数学与统计学院, 河南商丘 476000

收稿日期:2016-04-11 修回日期:2017-04-25 出版日期:2017-11-25
- 作者简介:
- 梁常建,男,1981年出生于河南鹿邑,博士研究生,讲师,主要研究领域为定量模型检测.E-mail:liangcj37@snnu.edu.cn;李永明,男,1966年出生于陕西大荔,博士,教授,博士生导师,研究方向为计算智能、量子逻辑、量子计算、模型检测.E-mail:liyongm@snnu.edu.cn
- 基金资助:
- 国家自然科学基金 (No.11271237，No.11671244，No.11401363，No.11501345）; 高等学校博士学科点专项科研基金 (No.20130202110001）

The Model Checking Problem of Computing Tree Logic Based on Generalized Possibility Measures

LIANG Chang-jian^1,2, LI Yong-ming¹

1. School of Mathematics and Information Science, Shaanxi Normal University, Xi'an, Shaanxi 710119, China;
2. School of Mathematics and Statistics, Shangqiu Normal University, Shangqiu, Henan, 476000, China

Received:2016-04-11 Revised:2017-04-25 Online:2017-11-25 Published:2017-11-25
- Supported by:
- National Natural Science Foundation of China (No.11271237, No.11671244, No.11401363, No.11501345); Research Fund for the Doctoral Program of Higher Education of China (No.20130202110001)

摘要/Abstract

摘要： 本文首先分别给出了"约束可达"，"总是可达"这两个公式在广义可能性计算树逻辑（GPoCTL）中的另外两种等价形式；其次讨论了基于广义可能性测度的计算树逻辑的模型检测问题，将GPoCTL的模型检测问题规约为经典的CTL模型检测问题，利用截集的方法，给出了计算GPoCTL的模型检测问题的算法及其复杂度，并通过实例分析说明了这种算法的可行性；最后，研究了具有公平性假设的GPoCTL模型检测问题的计算复杂度，得到了与上面相似的结论.

关键词: 可能性理论, 计算树逻辑, 模型检测, 时间复杂性, 规约

Abstract: Firstly,two alternative equivalent forms of GPoCTL state formulas,"until","always",are given respectively.Secondly,it shows that the model checking problem of GPoCTL can be reduced to which of CTL,its algorithm is given through the method of cut set,and whose availability is explained with an example analysis,as a result,the time complexity of the algorithm is obtained.Finally,the properties of the GPoCTL model checking problem with fairness assumptions,which are similar to the GPoCTL,are studied by the similar method with GPoCTL.

Key words: possibility theory, computation tree logic, model checking, time complexity, reduction

中图分类号:

TP301.2

梁常建, 李永明. 广义可能性计算树逻辑的模型检测问题[J]. 电子学报, 2017, 45(11): 2641-2648.

LIANG Chang-jian, LI Yong-ming . The Model Checking Problem of Computing Tree Logic Based on Generalized Possibility Measures[J]. Acta Electronica Sinica, 2017, 45(11): 2641-2648.

参考文献

[1] 林惠民,张文辉.模型检测:理论,方法与应用[J].电子学报,2002,30(12):1907-1912. Lin H M,Zhang W H.Model checking:theories,Techniques and Applications[J].Acta Electronica Sinica,2002,30(12):1907-1912.(in Chinese)
[2] C Baier,J P Katoen.Principles of Model Checking[M].Cambridge,Massachusetts:MIT Press,2008.
[3] 林运国,雷红轩,李永明.量子马尔可夫链安全性模型检测[J].电子学报,2014,42(11):2191-2197. Lin Y G,Lei H X,Li.Model checking of safety property over quantum markov chain[J].Acta Electroni-ca Sinica,2014,42(11):2191-2197.(in Chinese)
[4] M Chechik,B Devereux,A Gurfinkel,et al,Multi-valued symbolic model-checking[J].ACM Transactions on Software Engineering Methodology,2004,12(4):1-38.
[5] M Chechik,A Gurfinkel,B Devereux,et al.Data structures for symbolic multi-valued model-checking[J].Formal Methods in System Design,2006,29(3):295-344.
[6] Pan H Y,Li Y M,Cao Y Z,Ma Z Y.Model checking computation tree logic over finite lattices[J].Theoretical Computer Science,2016,612:45-62.
[7] Pan H Y,Li Y M,Cao Y Z,Ma Z Y.Model checking fuzzy computation tree logic[J].Fuzzy Sets and Systems,2015,2612:60-77.
[8] D Dubois.Possibility theory and statistical reasoning[J].Computational Statistics and Data Analysis,2006,51:47-69.
[9] Li Y M,Li L.Model checking of linear-time properties based on possibility measure[J].IEEE Transactions on Fuzzy Systems,2013,21(5):842-854.
[10] Li Y M,Li Y N.Computation tree logic model checking based on possibility measures[J].Fuzzy Sets and Systems,2015,26(2):44-59.
[11] 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.
[12] Li Y M.Quantitative model checking of linear-time properties based on generalized possibility measures[DB/OL].http://arxiv.org/abs/1601.06504.
[13] 马占有,李永明.基于决策过程的广义可能性计算树逻辑模型检测[J].中国科学:信息科学,2016,46(11):1591-1607. Ma Z Y,Li Y M.Model checking generalized possibilistic computation tree logic based on decision processes[J].Science China Information Sciences,2016,46(11):1591-1607.(in Chinese)
[14] J Kleinberg,E Tardos.Algorithm Design[M].Addison-Wesley,MA,2005.
[15] 李永明.模糊计算理论[M].北京:科学出版社,2016. Li Y M.Theories of Computations[M].Beijing:Science Press,2016.

广义可能性计算树逻辑的模型检测问题

The Model Checking Problem of Computing Tree Logic Based on Generalized Possibility Measures

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics

[1]	王舜, 杜晔, 韩臻. 基于模块化Abstract-Refine算法框架的软件模型检测方法[J]. 电子学报, 2020, 48(5): 997-1002.
[2]	范艳焕, 李永明, 潘海玉. 不确定型模糊Kripke结构的计算树逻辑模型检测[J]. 电子学报, 2018, 46(1): 152-159.
[3]	梁常建, 李永明. 具有模糊时态的广义可能性线性时序逻辑的模型检测[J]. 电子学报, 2017, 45(12): 2971-2977.
[4]	朱维军, 周清雷, 李永亮. 以DNA为载体的线性时序逻辑模型检测[J]. 电子学报, 2016, 44(6): 1265-1271.
[5]	林运国, 雷红轩, 李永明. 量子马尔可夫链安全性模型检测[J]. 电子学报, 2014, 42(11): 2191-2197.
[6]	王昌晶, 薛锦云, 左正康. SRLtoRadl生成系统及其范畴论语义[J]. 电子学报, 2014, 42(1): 137-143.
[7]	刘志锋, 孙博, 周从华. 概率实时时态认知逻辑模型检测中抽象技术的研究[J]. 电子学报, 2013, 41(7): 1343-1351.
[8]	周从华, 孙博, 刘志锋, 葛云. 概率时态认知逻辑模型检测中三值抽象技术的研究[J]. 电子学报, 2012, 40(10): 2052-2061.
[9]	王曦;徐中伟. 基于启发式SCCs的广义Büchi 自动机判空检测算法[J]. 电子学报, 2012, 40(1): 95-102.
[10]	张广泉;戎玫;朱雪阳;何亚丽;石慧娟. 基于XYZ/ADL的Web服务组合描述与验证[J]. 电子学报, 2011, 39(3A): 86-93.
[11]	尹传龙;庄雷;王从银;. 实时模型检测中基于驻留环的精确加速[J]. 电子学报, 2011, 39(3): 489-493.
[12]	张广泉;戎玫;王 Sheng. 时间感知Web服务交互行为建模与失配检测方法研究[J]. 电子学报, 2011, 39(11): 2568-2575.
[13]	谢朝海;陶然;王越;李继勇. 原-对偶规约基与连续最小元[J]. 电子学报, 2008, 36(6): 1124-1129.
[14]	王雷;李吉;李博洋. 缓冲区溢出漏洞精确检测方法研究[J]. 电子学报, 2008, 36(11): 2200-2204.
[15]	谭佳, 孙艳春, 梅宏. ABC方法中体系结构风格建模的研究[J]. 电子学报, 2006, 34(5): 969-976.