CTL Symbolic Model Checking Based on Fuzzy Logic

被引：0
|
作者：
Nie, Pengzhan [1 ]
Jiang, Jiulei [2 ]
Ma, Zhanyou [1 ]
机构：
[1] North Minzu Univ, Coll Comp Sci & Engn, Yinchuan, Ningxia, Peoples R China
[2] Changshu Inst Technol, Sch Comp Sci & Engn, Suzhou 215500, Peoples R China
来源：
2020 IEEE INTL CONF ON DEPENDABLE, AUTONOMIC AND SECURE COMPUTING, INTL CONF ON PERVASIVE INTELLIGENCE AND COMPUTING, INTL CONF ON CLOUD AND BIG DATA COMPUTING, INTL CONF ON CYBER SCIENCE AND TECHNOLOGY CONGRESS (DASC/PICOM/CBDCOM/CYBERSCITECH) | 2020年
关键词：
fuzzy logic; symbolic model checking; MTBDD; CTL;
D O I：
10.1109/DASC-PICom-CBDCom-CyberSciTech49142.2020.00074
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
The problem of state space explosion is often encountered in model checking, and the fuzzy uncertainty information in the system also needs to be processed. We have proposed a new calculation method of model checking. Unlike the classical symbolic model checking, CTL based on fuzzy logic is symbolized, and quasi-Boolean functions that can be represented by multiple terminal binary decision diagrams (MTBDD) are used to represent system models and attribute specifications. Combining the operation rules between quasi-Boolean functions with classic symbol model checking formulas and verifying them, a quasiBoolean function formula is finally obtained. By putting the state code into the formula, the corresponding probability value can be obtained.
引用
收藏
页码：380 / 385
页数：6
相关论文
共 50 条
  • [41] Bounded Model Checking of CTL
    Zhi-Hong Tao
    Cong-Hua Zhou
    Zhong Chen
    Li-Fu Wang
    Journal of Computer Science and Technology, 2007, 22 : 39 - 43
  • [42] Symbolic model checking
    McMillan, KL
    VERIFICATION OF DIGITAL AND HYBRID SYSTEM, 2000, 170 : 117 - 137
  • [43] Exploiting Asymmetry in Logic Puzzles: Using ZDDs for Symbolic Model Checking Dynamic Epistemic Logic
    Miedema, Daniel
    Gattinger, Malvin
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2023, (379): : 407 - 420
  • [44] Planning in Real-Time Domains with Timed CTL Goals via Symbolic Model Checking
    Stoehr, Daniel
    Glesner, Sabine
    2013 INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING (TASE), 2013, : 7 - 14
  • [45] Using symbolic CTL model checking to verify the railway stations of Hoorn-Kersenboogerd and Heerhugowaard
    Eisner C.
    International Journal on Software Tools for Technology Transfer, 2002, 4 (1) : 107 - 124
  • [46] Possibilistic Fuzzy Linear Temporal Logic and Its Model Checking
    Li, Yongming
    Wei, Jielin
    IEEE TRANSACTIONS ON FUZZY SYSTEMS, 2021, 29 (07) : 1899 - 1913
  • [47] CTL Model Checking Based on Binary Classification of Machine Learning
    Zhu, Weijun
    Wu, Huanmei
    INTERNATIONAL ARAB JOURNAL OF INFORMATION TECHNOLOGY, 2022, 19 (02) : 249 - 260
  • [48] Debugging Smart Contract’s Business Logic Using Symbolic Model Checking
    E. Shishkin
    Programming and Computer Software, 2019, 45 : 590 - 599
  • [49] Symbolic model checking for Dynamic Epistemic Logic-S5 and beyond
    van Benthem, Johan
    van Eijck, Jan
    Gattinger, Malvin
    Su, Kaile
    JOURNAL OF LOGIC AND COMPUTATION, 2018, 28 (02) : 367 - 402
  • [50] Fully symbolic unbounded model checking for Alternating-time Temporal Logic
    Kacprzak, M
    Penczek, W
    AUTONOMOUS AGENTS AND MULTI-AGENT SYSTEMS, 2005, 11 (01) : 69 - 89
12345