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] UTP and Temporal Logic Model Checking
    Anderson, Hugh
    Ciobanu, Gabriel
    Freitas, Leo
    [J]. UNIFYING THEORIES OF PROGRAMMING, 2010, 5713 : 22 - +
  • [42] Revising Specifications with CTL Properties Using Bounded Model Checking
    Finger, Marcelo
    Wassermann, Renata
    [J]. ADVANCES IN ARTIFICIAL INTELLIGENCE - SBIA 2008, PROCEEDINGS, 2008, 5249 : 157 - 166
  • [43] Efficient Parallel CTL Model-Checking for Pushdown Systems
    Chen, Xinyu
    Wei, Hansheng
    Ye, Xin
    Hao, Li
    Huang, Yanhong
    Shi, Jianqi
    [J]. 2018 IEEE INT CONF ON PARALLEL & DISTRIBUTED PROCESSING WITH APPLICATIONS, UBIQUITOUS COMPUTING & COMMUNICATIONS, BIG DATA & CLOUD COMPUTING, SOCIAL COMPUTING & NETWORKING, SUSTAINABLE COMPUTING & COMMUNICATIONS, 2018, : 23 - 30
  • [44] Distributed CTL model checking using MapReduce: theory and practice
    Camilli, Carlo Bellettini Matteo
    Capra, Lorenzo
    Monga, Mattia
    [J]. CONCURRENCY AND COMPUTATION-PRACTICE & EXPERIENCE, 2016, 28 (11) : 3025 - 3041
  • [45] Symbolic systems, explicit properties: On hybrid approaches for LTL symbolic model checking
    Sebastiani R.
    Tonetta S.
    Vardi M.Y.
    [J]. International Journal on Software Tools for Technology Transfer, 2011, 13 (4) : 319 - 335
  • [46] Formal Verification of SDG via Symbolic Model Checking
    Ning, Ning
    Zhang, Jun
    Gao, Xiang-Yang
    Xue, Jing
    [J]. ICICTA: 2009 SECOND INTERNATIONAL CONFERENCE ON INTELLIGENT COMPUTATION TECHNOLOGY AND AUTOMATION, VOL IV, PROCEEDINGS, 2009, : 521 - 524
  • [47] Feasibility analysis for robustness quantification by symbolic model checking
    Souheib Baarir
    Cécile Braunstein
    Emmanuelle Encrenaz
    Jean-Michel Ilié
    Isabelle Mounier
    Denis Poitrenaud
    Sana Younes
    [J]. Formal Methods in System Design, 2011, 39 : 165 - 184
  • [48] Symbolic Model-Checking of Optimistic Replication Algorithms
    Boucheneb, Hanifa
    Imine, Abdessamad
    Najem, Manal
    [J]. INTEGRATED FORMAL METHODS, 2010, 6396 : 89 - +
  • [49] Feasibility analysis for robustness quantification by symbolic model checking
    Baarir, Souheib
    Braunstein, Cecile
    Encrenaz, Emmanuelle
    Ilie, Jean-Michel
    Mounier, Isabelle
    Poitrenaud, Denis
    Younes, Sana
    [J]. FORMAL METHODS IN SYSTEM DESIGN, 2011, 39 (02) : 165 - 184
  • [50] Symbolic Model Checking Commitment Protocols Using Reduction
    El-Menshawy, Mohamed
    Bentahar, Jamal
    Dssouli, Rachida
    [J]. DECLARATIVE AGENT LANGUAGES AND TECHNOLOGIES VIII (DALT), 2011, 6619 : 185 - 203
12345