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

• 学术论文 • 上一篇    下一篇

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

梁常建1,2, 李永明1   

  1. 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-jian1,2, LI Yong-ming1   

  1. 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)

摘要: 本文首先定义了具有模糊时态的广义可能性线性时序逻辑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

中图分类号: