具有模糊时态的广义可能性线性时序逻辑的模型检测

doi:10.3969/j.issn.0372-2112.2017.12.020

电子学报 ›› 2017, Vol. 45 ›› Issue (12): 2971-2977.DOI: 10.3969/j.issn.0372-2112.2017.12.020

具有模糊时态的广义可能性线性时序逻辑的模型检测

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

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

收稿日期:2016-12-11 修回日期:2017-03-23 出版日期:2017-12-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）

Model Checking of Fuzzy Linear Temporal 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-12-11 Revised:2017-03-23 Online:2017-12-25 Published:2017-12-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

摘要： 本文首先定义了具有模糊时态的广义可能性线性时序逻辑GPoFLTL（Generalized Possibilistic Fuzzy Linear Tempora Logic）的语构以及基于路径和基于语言的两种语义解释，证明了GPoFLTL在模糊时态方面对GPoLTL（Generalized Possibilistic Linear Tempora Logic）进行了扩张，并通过实例说明了GPoFLTL比GPoLTL具有更强的表达能力；其次在广义可能性测度下通过模糊矩阵运算讨论了"不久"，"几乎总是"等几类模糊时态性质的模型检测问题；最后研究了模糊时态性质的必要性阈值模型检测问题，给出了基于自动机的GPoFLTL的阈值模型检测算法及算法的复杂度.

关键词: 模糊时态, 可能性性质, 线性时序逻辑, 时间复杂度, 阈值模型检测

Abstract: In this paper,firstly,the syntax and semantics of GPoFLTL(Generalized Possibilistic Fuzzy Linear Tempora Logic)are given,especially,both the path and language semantics of GPoFLTL are discussed.It is shown that GPoFLTL is the extension to GPoLTL(Generalized Possibilistic Linear Tempora Logic) with respect to fuzzy time,and that GPoFLTL has the stronger expression power than GPoLTL illustrated by some examples.Secondly,GPoFLTL model checking based on the generalized possibility measures is discussed using fuzzy matrix operator,which includes some fuzzy time temporal,"Soon","Nearly always",etc.Finally,the necessity threshold model checking problem of fuzzy linear time properties with fuzzy time temporal is studied; furthermore,the algorithm of the necessity threshold model checking of GPoFLTL based on automata method is given,and the time complexity of this method is proved.

Key words: fuzzy time temporal, possibility property, linear temporal logic, time complexity, threshold model checking

中图分类号:

TP301.2

梁常建, 李永明. 具有模糊时态的广义可能性线性时序逻辑的模型检测[J]. 电子学报, 2017, 45(12): 2971-2977.

LIANG Chang-jian, LI Yong-ming . Model Checking of Fuzzy Linear Temporal Logic Based on Generalized Possibility Measures[J]. Acta Electronica Sinica, 2017, 45(12): 2971-2977.

参考文献

[1] C Baier,J P Katoen.Principles of Model Checking[M].Cambridge,Massachusetts:MIT Press,2008.
[2] 林惠民,张文辉.模型检测:理论,方法与应用[J].电子学报,2002,30(12):1907-1912. H M Lin,W H Zhang.Model checking:theories,Techniques and Applications[J].Acta Electronica Sinica,2002,30(12):1907-1912.(in Chinese)
[3] 林运国,雷红轩,李永明.量子马尔可夫链安全性模型检测[J].电子学报,2014,42(11):2191-2197. Lin Y G,Lei H X,Li Y M.Model checking of safety property over quantum Markov chain[J].Acta Electronica Sinica,2014,42(11):2191-2197.(in Chinese)
[4] 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.
[5] Y M Li,M Droste,L H Lei.Model checking of linear-time properties in multi-valued systems[J].Information Sciencses,2017,377(1):51-74.
[6] H Y Pan,Y M Li,Y Z Cao,Z Y Ma.Model checking fuzzy computation tree logic[J].Fuzzy Sets and Systems,2015,262(C):60-77.
[7] S Almagor,U Boker,O Kupferman.Formalizing and reasoning about quality[A].The 40th International Colloquium on Automata,Languages and Programming (ICALP)[C].Riga,Latvia:Springer, 2013.15-27.
[8] H Y Pan,Y M Li,Y Z Cao,Z Y Ma.Model checking computation tree logic over finite lattices[J].Theoretical Computer Science,2016,612(1):45-62.
[9] D Dubois.Possibility theory and statistical reasoning[J].Computational Statistics and Data Analysis,2006,51(1):47-69.
[10] Y M Li,L Li.Model checking of linear-time properties based on possibility measure[J].IEEE Transactions on Fuzzy Systems,2013,21(5):842-854.
[11] Y M Li,Y N Li.Computation tree logic model checking based on possibility measures[J].Fuzzy Sets and Systems,2015,26(2):44-59.
[12] Y M Li,Z Y Ma,Quantitative computation tree logic model checking based on generalized possibility measures[J].IEEE Transactions on Fuzzy Systems,2015,23(6):2034-2047.
[13] Y M Li.Quantitative model checking of linear-time properties based on generalized possibility measures[J].Fuzzy Sets and Systems,2017,320(1):17-39.
[14] A Frigeri,L Pasquale,P Spoletini.Fuzzy time in linear temporal logic[J].ACM Transactions on Computational Logic,2014,15(4):1-22.

具有模糊时态的广义可能性线性时序逻辑的模型检测

Model Checking of Fuzzy Linear Temporal Logic Based on Generalized Possibility Measures

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 11

编辑推荐

Metrics

[1]	李鹏, 闵慧, 罗爱静. 基于动态图的PPI网络构建和复合物挖掘算法研究[J]. 电子学报, 2021, 49(8): 1489-1497.
[2]	王宁远, 刘亮, 陈东, 刘欢, 郝时光. 低轨巨星座多品类业务流低复杂度分段路由方法[J]. 电子学报, 2021, 49(11): 2124-2132.
[3]	刘剑锋, 孙力帆, 普杰信, 何子述, 王燕玲. 基于刚性约束的双移动机器人协同定位[J]. 电子学报, 2020, 48(9): 1777-1785.
[4]	范艳焕, 李永明. 模糊线性时序逻辑的可实现性[J]. 电子学报, 2018, 46(2): 341-346.
[5]	曹政才, 林诚然, 黄冉. 带等待时间约束并行机调度问题的Copula分布估计算法[J]. 电子学报, 2017, 45(12): 2949-2956.
[6]	朱维军, 周清雷, 李永亮. 以DNA为载体的线性时序逻辑模型检测[J]. 电子学报, 2016, 44(6): 1265-1271.
[7]	李仲生, 李仁发, 蔡则苏, 赵乘麟. 稀疏表示下的非监督显著对象提取[J]. 电子学报, 2012, 40(6): 1097-1102.
[8]	钱鹏江;王士同;邓赵红;徐华. 基于最小包含球的大数据集快速谱聚类算法[J]. 电子学报, 2010, 38(9): 2035-2041.
[9]	冯毅;易江芳;刘丹;佟冬;程旭. 面向SoC系统芯片中跨时钟域设计的模型检验方法[J]. 电子学报, 2008, 36(5): 886-892.
[10]	蒋廷耀;李庆华. 多播路由算法MPH的时间复杂度研究[J]. 电子学报, 2004, 32(10): 1706-1708.
[11]	吴湛击, 吴伟陵. 随机排序的优化算法[J]. 电子学报, 2000, 28(S1): 76-79.