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 条
  • [1] Symbolic checking of Fuzzy CTL on Fuzzy Program Graph
    Ebrahimi, Masoud
    Sotudeh, Gholamreza
    Movaghar, Ali
    ACTA INFORMATICA, 2019, 56 (01) : 1 - 33
  • [2] Symbolic checking of Fuzzy CTL on Fuzzy Program Graph
    Masoud Ebrahimi
    Gholamreza Sotudeh
    Ali Movaghar
    Acta Informatica, 2019, 56 : 1 - 33
  • [3] Symbolic guided search for CTL model checking
    Bloem, R
    Ravi, K
    Somenzi, F
    37TH DESIGN AUTOMATION CONFERENCE, PROCEEDINGS 2000, 2000, : 29 - 34
  • [4] Structural symbolic CTL model checking of asynchronous systems
    Ciardo, G
    Siminiceanu, R
    COMPUTER AIDED VERIFICATION, 2003, 2725 : 40 - 53
  • [5] Graded-CTL: Satisfiability and Symbolic Model Checking
    Ferrante, Alessandro
    Napoli, Margherita
    Parente, Mimmo
    FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS, 2009, 5885 : 306 - +
  • [6] Symbolic Model Checking Epistemic Strategy Logic
    Huang, Xiaowei
    Van der Meyden, Ron
    PROCEEDINGS OF THE TWENTY-EIGHTH AAAI CONFERENCE ON ARTIFICIAL INTELLIGENCE, 2014, : 1426 - 1432
  • [7] Symbolic Model Checking for Dynamic Epistemic Logic
    van Benthem, Johan
    van Eijck, Jan
    Gattinger, Malvin
    Su, Kaile
    LOGIC, RATIONALITY, AND INTERACTION (LORI 2015), 2015, 9394 : 366 - 378
  • [8] Linear Temporal Logic Symbolic Model Checking
    Rozier, Kristin Y.
    COMPUTER SCIENCE REVIEW, 2011, 5 (02) : 163 - 203
  • [9] CTL Model Checking based on Giraph
    Duan, Tingyin
    Zhou, Qinglei
    Pan, Shan
    Zhu, Weijun
    PROCEEDINGS OF THE 2016 5TH INTERNATIONAL CONFERENCE ON ADVANCED MATERIALS AND COMPUTER SCIENCE, 2016, 80 : 652 - 657
  • [10] Symbolic CTL Model Checking of Asynchronous Systems Using Constrained Saturation
    Zhao, Yang
    Ciardo, Gianfranco
    AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, PROCEEDINGS, 2009, 5799 : 368 - 381
12345