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
基金
美国国家科学基金会;
关键词
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 条
  • [31] An Automata-Theoretic Approach to L-valued Computation Tree Logic Model Checking
    WEI Xiujuan
    LI Yongming
    Chinese Journal of Electronics, 2019, 28 (02) : 309 - 315
  • [32] Bounded Model Checking for Weighted Interpreted Systems and for Flat Weighted Epistemic Computation Tree Logic
    Wozna-Szczesniak, Bozena
    Szczesniak, Ireneusz
    Zbrzezny, Agnieszka M.
    Zbrzezny, Andrzej
    PRIMA 2014: PRINCIPLES AND PRACTICE OF MULTI-AGENT SYSTEMS, 2014, 8861 : 107 - 115
  • [33] Inconsistency-tolerant Hierarchical Probabilistic Computation Tree Logic and Its Application to Model Checking
    Kamide, Norihiro
    Yamamoto, Noriko
    ICAART: PROCEEDINGS OF THE 13TH INTERNATIONAL CONFERENCE ON AGENTS AND ARTIFICIAL INTELLIGENCE - VOL 2, 2021, : 490 - 499
  • [34] Model Checking Quantitative Linear Time Logic
    Faella, Marco
    Legay, Axel
    Stoelinga, Marielle
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2008, 220 (03) : 61 - 77
  • [35] Cache Timing Side-Channel Vulnerability Checking with Computation Tree Logic
    Deng, Shuwen
    Xiong, Wenjie
    Szefer, Jakub
    PROCEEDINGS OF THE 7TH INTERNATIONAL WORKSHOP ON HARDWARE AND ARCHITECTURAL SUPPORT FOR SECURITY AND PRIVACY (HASP '18), 2018,
  • [36] Efficient computation of exact solutions for quantitative model checking
    Giro, Sergio
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2012, (85): : 17 - 32
  • [37] Model Checking Computation Tree Logic over Multi-Valued Decision Processes and Its Reduction Techniques
    Wuniu LIU
    Junmei WANG
    Qing HE
    Yongming LI
    Chinese Journal of Electronics, 2024, 33 (06) : 1399 - 1411
  • [38] Model Checking Computation Tree Logic Over Multi-Valued Decision Processes and Its Reduction Techniques
    Liu, Wuniu
    Wang, Junmei
    He, Qing
    Li, Yongming
    CHINESE JOURNAL OF ELECTRONICS, 2024, 33 (06) : 1399 - 1411
  • [39] Computation Tree Logic Model Checking over Possibilistic Decision Processes Under Finite-Memory Scheduler
    Liu, Wuniu
    He, Qing
    Li, Yongming
    THEORETICAL COMPUTER SCIENCE, NCTCS 2021, 2021, 1494 : 75 - 88
  • [40] Model checking for multi-valued computation tree logics
    Konikowska, B
    Penczek, W
    BEYOND TWO: THEORY AND APPLICATIONS OF MULTIPLE-VALUED LOGIC, 2003, 114 : 193 - 210