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

被引：0

作者：

Liang C.-J. ^{[1
,2
]}

Li Y.-M. ^{[1
]}

机构：

[1] School of Mathematics and Information Science, Shaanxi Normal University, Xi'an, 710119, Shaanxi

[2] School of Mathematics and Statistics, Shangqiu Normal University, Shangqiu, 476000, Henan

来源：

Tien Tzu Hsueh Pao/Acta Electronica Sinica | 2017年 / 45卷 / 12期

关键词：

Fuzzy time temporal; Linear temporal logic; Possibility property; Threshold model checking; Time complexity;

D O I：

10.3969/j.issn.0372-2112.2017.12.020

中图分类号：

学科分类号：

摘要：

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. © 2017, Chinese Institute of Electronics. All right reserved.

引用

页码：2971 / 2977

页数：6

共 14 条

[1]

Baier C., Katoen J.P., Principles of Model Checking, (2008)

[2]

Lin H.M., Zhang W.H., Model checking: theories, Techniques and Applications, Acta Electronica Sinica, 30, 12, pp. 1907-1912, (2002)

[3]

Lin Y.G., Lei H.X., Li Y.M., Model checking of safety property over quantum Markov chain, Acta Electronica Sinica, 42, 11, pp. 2191-2197, (2014)

[4]

Chechik M., Gurfinkel A., Devereux B., Et al., Data structures for symbolic multi-valued model-checking, Formal Methods in System Design, 29, 3, pp. 295-344, (2006)

[5]

Li Y.M., Droste M., Lei L.H., Model checking of linear-time properties in multi-valued systems, Information Sciencses, 377, 1, pp. 51-74, (2017)

[6]

Pan H.Y., Li Y.M., Cao Y.Z., Ma Z.Y., Model checking fuzzy computation tree logic, Fuzzy Sets and Systems, 262, C, pp. 60-77, (2015)

[7]

Almagor S., Boker U., Kupferman O., Formalizing and reasoning about quality, The 40th International Colloquium on Automata, Languages and Programming (ICALP), pp. 15-27, (2013)

[8]

Pan H.Y., Li Y.M., Cao Y.Z., Ma Z.Y., Model checking computation tree logic over finite lattices, Theoretical Computer Science, 612, 1, pp. 45-62, (2016)

[9]

Dubois D., Possibility theory and statistical reasoning, Computational Statistics and Data Analysis, 51, 1, pp. 47-69, (2006)

[10]

Li Y.M., Li L., Model checking of linear-time properties based on possibility measure, IEEE Transactions on Fuzzy Systems, 21, 5, pp. 842-854, (2013)

← 1 2 →