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 条

[31] Bounded saturation-based CTL model checking
Voeroes, Andras
Darvas, Daniel
Bartha, Tamas
PROCEEDINGS OF THE ESTONIAN ACADEMY OF SCIENCES, 2013, 62 (01) : 59 - 70
[32] Tearing based automatic abstraction for CTL model checking
Lee, W
Pardo, A
Jang, JY
Hachtel, G
Somenzi, F
1996 IEEE/ACM INTERNATIONAL CONFERENCE ON COMPUTER-AIDED DESIGN - DIGEST OF TECHNICAL PAPERS, 1996, : 76 - 81
[33] Symbolic computation tree logic model checking of time Petri nets
Okawa, Yasukichi
Yoneda, Tomohiro
Electronics and Communications in Japan, Part III: Fundamental Electronic Science (English translation of Denshi Tsushin Gakkai Ronbunshi), 1997, 80 (04): : 11 - 20
[34] Symbolic model checking of Verilog programs with the propositional projection temporal logic
Pang, Tao
Duan, Zhenhua
Liu, Xiaofang
Xi'an Dianzi Keji Daxue Xuebao/Journal of Xidian University, 2014, 41 (02): : 79 - 84
[35] Model Checking for Symbolic-Heap Separation Logic with Inductive Predicates
Brotherston, James
Gorogiannis, Nikos
Kanovich, Max
Rowe, Reuben
ACM SIGPLAN NOTICES, 2016, 51 (01) : 84 - 96
[36] Application of symbolic and bounded model checking to the verification of logic control systems
Loeis, Kingliana
Younis, Mohammed Bani
Frey, Georg
ETFA 2005: 10TH IEEE INTERNATIONAL CONFERENCE ON EMERGING TECHNOLOGIES AND FACTORY AUTOMATION, VOL 1, PTS 1 AND 2, PROCEEDINGS, 2005, : 247 - 250
[37] CTL model checking based on forward state traversal
Iwashita, H
Nakata, T
Hirose, F
1996 IEEE/ACM INTERNATIONAL CONFERENCE ON COMPUTER-AIDED DESIGN - DIGEST OF TECHNICAL PAPERS, 1996, : 82 - 87
[38] Symbolic computation tree logic model checking of time Petri nets
Okawa, Y
Yoneda, T
ELECTRONICS AND COMMUNICATIONS IN JAPAN PART III-FUNDAMENTAL ELECTRONIC SCIENCE, 1997, 80 (04): : 11 - 20
[39] Model Checking for Graded CTL
Ferrante, Alessandro
Napoli, Margherita
Parente, Mimmo
FUNDAMENTA INFORMATICAE, 2009, 96 (03) : 323 - 339
[40] Bounded model checking of CTL
Tao, Zhi-Hong
Zhou, Cong-Hua
Chen, Zhong
Wang, Li-Fu
JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY, 2007, 22 (01) : 39 - 43

← 1 2 3 4 5 →