Temporal Logic Model Checking via Probe Machine

被引：0
作者：
Zhu, Weijun [1 ]
Li, En [2 ]
Yang, Xiaoyu [2 ]
机构：
[1] Zhengzhou Univ, Sch Informat Engn, Zhengzhou, Peoples R China
[2] Zhengzhou Univ, Affiliated Hosp 2, Zhengzhou, Peoples R China
来源：
PROCEEDINGS OF 2020 IEEE 4TH INFORMATION TECHNOLOGY, NETWORKING, ELECTRONIC AND AUTOMATION CONTROL CONFERENCE (ITNEC 2020) | 2020年
基金：
中国国家自然科学基金;
关键词：
probe machine; linear temporal logic; model checking; MOLECULAR COMPUTATION;
D O I：
10.1109/itnec48623.2020.9084719
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
How to use a Probe Machine (PM) to Model Checking (MC) the linear Temporal Logic (LTL) formulas? This is an open issue. First, a data pool consisting of probes and data fibers are established. Second, some hybridizations are employed to connect the probes to the data fibers. At last, the MC results of the several basic constructs in LTL are gotten, according to some conditions of decision. As a result, a novel approach is pioneered to perform LTL model checking via PM.
引用
收藏
页码：623 / 626
页数：4
相关论文
共 50 条
[21]   Model Checking Self-Stabilising in Embedded Systems with Linear Temporal Logic [J].
Marah, Rim ;
EL Hibaoui, Abdelaaziz .
INTERNATIONAL JOURNAL OF ADVANCED COMPUTER SCIENCE AND APPLICATIONS, 2015, 6 (08) :256-261
[22]   A vertex centric parallel algorithm for linear temporal logic model checking in Pregel [J].
Xie, Miao ;
Yang, Qiusong ;
Zhai, Jian ;
Wang, Qing .
JOURNAL OF PARALLEL AND DISTRIBUTED COMPUTING, 2014, 74 (11) :3161-3174
[23]   Model checking open systems with alternating projection temporal logic [J].
Tian, Cong ;
Duan, Zhenhua .
THEORETICAL COMPUTER SCIENCE, 2019, 774 :65-81
[24]   Possibilistic Fuzzy Linear Temporal Logic and Its Model Checking [J].
Li, Yongming ;
Wei, Jielin .
IEEE TRANSACTIONS ON FUZZY SYSTEMS, 2021, 29 (07) :1899-1913
[25]   Model checking propositional projection temporal logic based on SPIN [J].
Tian, Cong ;
Duan, Zhenhua .
FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS, 2007, 4789 :246-265
[26]   Constraining Cycle Alternations in Model Checking for Interval Temporal Logic [J].
Molinari, Alberto ;
Montanari, Angelo ;
Peron, Adriano .
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2016, 322 :211-226
[27]   Automatic software model checking via constraint logic [J].
Flanagan, C .
SCIENCE OF COMPUTER PROGRAMMING, 2004, 50 (1-3) :253-270
[28]   Temporal Logics for Phylogenetic Analysis via Model Checking [J].
Blanco, Roberto ;
de Miguel Casado, Gregorio ;
Ignacio Requeno, Jose ;
Manuel Colom, Jose .
2010 IEEE INTERNATIONAL CONFERENCE ON BIOINFORMATICS AND BIOMEDICINE WORKSHOPS (BIBMW), 2010, :152-157
[29]   Temporal Logics for Phylogenetic Analysis via Model Checking [J].
Ignacio Requeno, Jose ;
de Miguel Casado, Gregorio ;
Blanco, Roberto ;
Manuel Colom, Jose .
IEEE-ACM TRANSACTIONS ON COMPUTATIONAL BIOLOGY AND BIOINFORMATICS, 2013, 10 (04) :1058-1070
[30]   Temporal logic to query semantic graphs using the model checking method [J].
Gueffaz, Mahdi ;
Rampacek, Sylvain ;
Nicolle, Christophe .
Journal of Software, 2012, 7 (07) :1462-1472
12345