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] A vertex centric parallel algorithm for linear temporal logic model checking in Pregel
    Xie, Miao
    Yang, Qiusong
    Zhai, Jian
    Wang, Qing
    JOURNAL OF PARALLEL AND DISTRIBUTED COMPUTING, 2014, 74 (11) : 3161 - 3174
  • [22] Model checking open systems with alternating projection temporal logic
    Tian, Cong
    Duan, Zhenhua
    THEORETICAL COMPUTER SCIENCE, 2019, 774 : 65 - 81
  • [23] Possibilistic Fuzzy Linear Temporal Logic and Its Model Checking
    Li, Yongming
    Wei, Jielin
    IEEE TRANSACTIONS ON FUZZY SYSTEMS, 2021, 29 (07) : 1899 - 1913
  • [24] Model checking propositional projection temporal logic based on SPIN
    Tian, Cong
    Duan, Zhenhua
    FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS, 2007, 4789 : 246 - 265
  • [25] Constraining Cycle Alternations in Model Checking for Interval Temporal Logic
    Molinari, Alberto
    Montanari, Angelo
    Peron, Adriano
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2016, 322 (322) : 211 - 226
  • [26] Automatic software model checking via constraint logic
    Flanagan, C
    SCIENCE OF COMPUTER PROGRAMMING, 2004, 50 (1-3) : 253 - 270
  • [27] Temporal Logics for Phylogenetic Analysis via Model Checking
    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
  • [28] Temporal Logics for Phylogenetic Analysis via Model Checking
    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
  • [29] Temporal logic to query semantic graphs using the model checking method
    Gueffaz, Mahdi
    Rampacek, Sylvain
    Nicolle, Christophe
    Journal of Software, 2012, 7 (07) : 1462 - 1472
  • [30] Which fragments of the interval temporal logic HS are tractable in model checking?
    Bozzelli, Laura
    Molinari, Alberto
    Montanari, Angelo
    Peron, Adriano
    Sala, Pietro
    THEORETICAL COMPUTER SCIENCE, 2019, 764 : 125 - 144
12345