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 条
[41]   SMT-based robust model checking for signal temporal logic [J].
Lee, Jia ;
Yu, Geunyeol ;
Bae, Kyungmin .
SCIENCE OF COMPUTER PROGRAMMING, 2025, 246
[42]   Temporal Logic Trees for Model Checking and Control Synthesis of Uncertain Discrete-Time Systems [J].
Gao, Yulong ;
Abate, Alessandro ;
Jiang, Frank J. ;
Giacobbe, Mirco ;
Xie, Lihua ;
Johansson, Karl Henrik .
IEEE TRANSACTIONS ON AUTOMATIC CONTROL, 2022, 67 (10) :5071-5086
[43]   On-the-fly unfolding with optimal exploration for linear temporal logic model checking of concurrent software and systems [J].
Li, Shuo ;
Zheng, Li'ao ;
Yang, Ru ;
Ding, Zhijun .
AUTOMATED SOFTWARE ENGINEERING, 2025, 32 (02)
[44]   Model checking linear temporal logic of rewriting formulas under localized fairness [J].
Bae, Kyungmin ;
Meseguer, Jose .
SCIENCE OF COMPUTER PROGRAMMING, 2015, 99 :193-234
[45]   Model Checking Temporal Aspects of Inconsistent Concurrent Systems Based on Paraconsistent Logic [J].
Chen, Donghuo ;
Wu, Jinzhao .
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2006, 157 (01) :23-38
[46]   Interval vs. Point Temporal Logic Model Checking: An Expressiveness Comparison [J].
Bozzelli, Laura ;
Molinari, Alberto ;
Montanari, Angelo ;
Peron, Adriano ;
Sala, Pietro .
ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2019, 20 (01)
[47]   Model Checking of Fuzzy Linear Temporal Logic Based on Generalized Possibility Measures [J].
Liang C.-J. ;
Li Y.-M. .
Tien Tzu Hsueh Pao/Acta Electronica Sinica, 2017, 45 (12) :2971-2977
[48]   A Foundation for Flow-Based Program Matching Using Temporal Logic and Model Checking [J].
Brunel, Julien ;
Doligez, Damien ;
Hansen, Rene Rydhof ;
Lawall, Julia L. ;
Muller, Gilles .
ACM SIGPLAN NOTICES, 2009, 44 (01) :114-126
[49]   Exploiting symmetry in linear time temporal logic model checking:: One step beyond [J].
Ajami, K ;
Haddad, S ;
Ilié, JM .
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, 1998, 1384 :52-67
[50]   Explaining Temporal Logic Model Checking Counterexamples Through the Use of Structured Natural Language [J].
Ferreira Moreira, Ezequiel Jose Veloso ;
Campo, Jose Creissac .
ENGINEERING INTERACTIVE COMPUTER SYSTEMS, EICS 2023 INTERNATIONAL WORKSHOPS AND DOCTORAL CONSORTIUM, 2024, 14517 :179-197
12345