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

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

作　　者：梁常建[1,2] 李永明 

机构地区：[1]陕西师范大学数学与信息科学学院,陕西西安710119 [2]商丘师范学院数学与统计学院,河南商丘476000

出　　处：《电子学报》2017年第12期2971-2977,共7页Acta Electronica Sinica

基　　金：国家自然科学基金(No.11271237;No.11671244;No.11401363;No.11501345);高等学校博士学科点专项科研基金项目(No.20130202110001)

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

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

分 类 号：TP301.2[自动化与计算机技术—计算机系统结构]