Quantitative Computation Tree Logic Model Checking Based on Generalized Possibility Measures

被引：52

作者：

Li, Yongming ^{[1
]}

Ma, Zhanyou ^{[1
,2
]}

机构：

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

[2] Beifang Univ Nationalities, Yinchuan 7500021, Peoples R China

来源：

IEEE TRANSACTIONS ON FUZZY SYSTEMS | 2015年 / 23卷 / 06期

基金：

美国国家科学基金会;

关键词：

Generalized possibilistic computation tree logic (GPoCTL); generalized possibilistic Kripke structure (GPKS); model checking; possibility theory; quantitative property;

D O I：

10.1109/TFUZZ.2015.2396537

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

We study generalized possibilistic computation tree logic (GPoCTL) model checking in this paper, which is an extension of possibilistic computation logic model checking introduced by Li et al. (2014). The system is modeled by generalized possibilistic Kripke structures, and the verifying property is specified by a GPoCTL formula. Based on generalized possibility measures and generalized necessity measures, the method of GPoCTL model checking is discussed, and the corresponding algorithm and its complexity are shown in detail. Furthermore, the comparison between possibilistic computation tree logic and GPoCTL is given. Finally, a thermostat example is given to illustrate the GPoCTL model-checking method.

引用

页码：2034 / 2047

页数：14

共 50 条

[1] Computation tree logic model checking based on possibility measures
Li, Yongming
Li, Yali
Ma, Zhanyou
FUZZY SETS AND SYSTEMS, 2015, 262 : 44 - 59
[2] Generalized possibility computation tree logic with frequency and its model checking
He, Qing
Liu, Wuniu
Li, Yongming
INTERNATIONAL JOURNAL OF APPROXIMATE REASONING, 2024, 173
[3] Computation tree logic model checking based on multi-valued possibility measures
Li, Yongming
Lei, Lihui
Li, Sanjiang
INFORMATION SCIENCES, 2019, 485 : 87 - 113
[4] Quantitative μ-Calculus Model Checking Algorithm Based on Generalized Possibility Measures
Zhang, Panqing
Jiang, Jiulei
Ma, Zhanyou
Zhu, Heng
IEEE 17TH INT CONF ON DEPENDABLE, AUTONOM AND SECURE COMP / IEEE 17TH INT CONF ON PERVAS INTELLIGENCE AND COMP / IEEE 5TH INT CONF ON CLOUD AND BIG DATA COMP / IEEE 4TH CYBER SCIENCE AND TECHNOLOGY CONGRESS (DASC/PICOM/CBDCOM/CYBERSCITECH), 2019, : 449 - 453
[5] 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
[6] Quantitative model checking of linear-time properties based on generalized possibility measures
Li, Yongming
FUZZY SETS AND SYSTEMS, 2017, 320 : 17 - 39
[7] Model checking quantified computation tree logic
Rensink, Arend
CONCUR 2006 - CONCURRENCY THEORY, PROCEEDINGS, 2006, 4137 : 110 - 125
[8] Model checking fuzzy computation tree logic
Pan, Haiyu
Li, Yongming
Cao, Yongzhi
Ma, Zhanyou
FUZZY SETS AND SYSTEMS, 2015, 262 : 60 - 77
[9] VECTORIZED MODEL CHECKING FOR COMPUTATION TREE LOGIC
HIRAISHI, H
MEKI, S
HAMAGUCHI, K
LECTURE NOTES IN COMPUTER SCIENCE, 1991, 531 : 44 - 53
[10] Incremental model checking for fuzzy computation tree logic
Pan, Haiyu
Zhou, Jie
Lin, Yuming
Cao, Yongzhi
FUZZY SETS AND SYSTEMS, 2025, 500

← 1 2 3 4 5 →