Possibilistic Fuzzy Linear Temporal Logic and Its Model Checking

被引：18

作者：

Li, Yongming ^{[1
]}

Wei, Jielin ^{[1
]}

机构：

[1] Shaanxi Normal Univ, Coll Comp Sci, Xian 710119, Peoples R China

来源：

IEEE TRANSACTIONS ON FUZZY SYSTEMS | 2021年 / 29卷 / 07期

基金：

美国国家科学基金会;

关键词：

Model checking; Atmospheric measurements; Particle measurements; Semantics; Possibility theory; Time complexity; Computational modeling; Fuzzy temporal operator; generalized possibility measure; linear temporal logic (LTL); model checking; TIME PROPERTIES;

D O I：

10.1109/TFUZZ.2020.2988848

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

Based on the Kripke structure, linear temporal logic and generalized possibility measure, this article studies the model checking problems of generalized possibilistic fuzzy linear temporal logic (GPoFTL). The generalized possibilistic Kripke structure is introduced to describe the system model. The syntax of GPoFTL, which includes fuzzy temporal operators such as ``soon'', ``presently'', ``gradually'', ``within'', ``last'', ``nearly always'', ``almost alwayss'', ``in the long distant future'', ``in the middle of'', ``nearly until'' and ``almost until'', and its language semantics and path semantics under generalized possibility measure are given. Next, we explain the semantics of fuzzy temporal operators through some examples and prove that GPoFTL is an extension of generalized possibilistic linear temporal logic in fuzzy time temporal logic. Furthermore, the GPoFTL model checking algorithm is given by explicit calculation formulas one by one for any GPoFTL formula involving fuzzy temporal operators using fuzzy matrix operations. Last, the algorithm of necessary threshold model checking of GPoFTL is studied using automata theory and its time complexity is discussed.

引用

页码：1899 / 1913

页数：15

共 50 条

[1] Model Checking of Fuzzy Linear Temporal Logic Based on Generalized Possibility Measures
Liang C.-J.
Li Y.-M.
Tien Tzu Hsueh Pao/Acta Electronica Sinica, 2017, 45 (12): : 2971 - 2977
[2] Linear Temporal Logic Symbolic Model Checking
Rozier, Kristin Y.
COMPUTER SCIENCE REVIEW, 2011, 5 (02) : 163 - 203
[3] Model Checking General Linear Temporal Logic
French, Tim
McCabe-Dansted, John
Reynolds, Mark
AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS (TABLEAUX 2013), 2013, 8123 : 119 - 133
[4] Query Checking for Linear Temporal Logic
Huang, Samuel
Cleaveland, Rance
CRITICAL SYSTEMS: FORMAL METHODS AND AUTOMATED VERIFICATION (FMICS-AVOCS 2017), 2017, 10471 : 34 - 48
[5] Temporal logic model checking
Clarke, EM
LOGIC PROGRAMMING - PROCEEDINGS OF THE 1997 INTERNATIONAL SYMPOSIUM, 1997, : 3 - 3
[6] Temporal logic and model checking
McMillan, KL
VERIFICATION OF DIGITAL AND HYBRID SYSTEM, 2000, 170 : 36 - 54
[7] A Probabilistic Temporal Logic with Frequency Operators and Its Model Checking
Tomita, Takashi
Hagihara, Shigeki
Yonezaki, Naoki
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2011, (73): : 79 - 93
[8] Satisfiability and Model Checking for One Parameterized Extension of Linear Temporal Logic
Gnatenko, A. R.
Zakharov, V. A.
AUTOMATIC CONTROL AND COMPUTER SCIENCES, 2022, 56 (07) : 649 - 660
[9] ONLINE MODEL-CHECKING FOR FINITE LINEAR TEMPORAL LOGIC SPECIFICATIONS
JARD, C
JERON, T
LECTURE NOTES IN COMPUTER SCIENCE, 1990, 407 : 189 - 196
[10] Satisfiability and Model Checking for One Parameterized Extension of Linear Temporal Logic
A. R. Gnatenko
V. A. Zakharov
Automatic Control and Computer Sciences, 2022, 56 : 649 - 660

← 1 2 3 4 5 →