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 条
  • [1] A Fully Parallel Approach of Model Checking Via Probe Machine
    Wang, Dong
    Liu, Jing
    Sun, Haiying
    Xu, Jin
    Kang, Jiexiang
    INTERNATIONAL JOURNAL OF SOFTWARE ENGINEERING AND KNOWLEDGE ENGINEERING, 2021, 31 (11N12) : 1761 - 1781
  • [2] CTL Model Checking based on Probe Machine
    Zhu, Weijun
    Liu, Yichen
    Li, En
    PROCEEDINGS OF 2019 IEEE 10TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND SERVICE SCIENCE (ICSESS 2019), 2019, : 518 - 522
  • [3] Model checking distributed temporal logic
    Dionisio, Francisco
    Ramos, Jaime
    Subtil, Fernando
    Vigano, Luca
    LOGIC JOURNAL OF THE IGPL, 2024,
  • [4] Symmetry in temporal logic model checking
    Miller, Alice
    Donaldson, Alastair
    Calder, Muffy
    ACM COMPUTING SURVEYS, 2006, 38 (03) : 2
  • [5] Temporal Logic and Model Checking for Operator Precedence Languages
    Chiari, Michele
    Mandrioli, Dino
    Pradella, Matteo
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2018, (277): : 161 - 175
  • [6] Bounded model checking distributed temporal logic
    Peres, Augusto
    Ramos, Jaime
    Dionisio, Francisco
    JOURNAL OF LOGIC AND COMPUTATION, 2023, 33 (05) : 1022 - 1059
  • [7] Exploiting symmetry in temporal logic model checking
    Clarke, EM
    Enders, R
    Filkorn, T
    Jha, S
    FORMAL METHODS IN SYSTEM DESIGN, 1996, 9 (1-2) : 77 - 104
  • [8] Coverage metrics for temporal logic model checking*
    Hana Chockler
    Orna Kupferman
    Moshe Y. Vardi
    Formal Methods in System Design, 2006, 28 : 189 - 212
  • [9] Operator precedence temporal logic and model checking
    Chiari, Michele
    Mandrioli, Dino
    Pradella, Matteo
    THEORETICAL COMPUTER SCIENCE, 2020, 848 : 47 - 81
  • [10] Decidability of model checking with the temporal logic EF
    Mayr, R
    THEORETICAL COMPUTER SCIENCE, 2001, 256 (1-2) : 31 - 62