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 条

[31] Satisfiability and Model Checking for One Parameterized Extension of Linear Temporal Logic [J].

Gnatenko, A. R. ;

Zakharov, V. A. .

AUTOMATIC CONTROL AND COMPUTER SCIENCES, 2022, 56 (07) :649-660

[32] Abstraction In Model Checking Real-Time Temporal Logic of Knowledge [J].

Zhou, CongHua ;

Sun, Bo .

JOURNAL OF COMPUTERS, 2012, 7 (02) :362-370

[33] Which fragments of the interval temporal logic HS are tractable in model checking? [J].

Bozzelli, Laura ;

Molinari, Alberto ;

Montanari, Angelo ;

Peron, Adriano ;

Sala, Pietro .

THEORETICAL COMPUTER SCIENCE, 2019, 764 :125-144

[34] Propositional projection temporal logic based distributed model checking method [J].

Shu X. ;

Wang C. ;

Wang Y. ;

Zhang L. .

Xi'an Dianzi Keji Daxue Xuebao/Journal of Xidian University, 2020, 47 (04) :39-47

[35] Efficient SMT-Based Model Checking for Signal Temporal Logic [J].

Lee, Jia ;

Yu, Geunyeol ;

Bae, Kyungmin .

2021 36TH IEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING ASE 2021, 2021, :343-354

[36] Satisfiability and Model Checking for One Parameterized Extension of Linear Temporal Logic [J].

A. R. Gnatenko ;

V. A. Zakharov .

Automatic Control and Computer Sciences, 2022, 56 :649-660

[37] Intrusion Detection Algorithm Based on Model Checking Interval Temporal Logic [J].

Zhu Weijun ;

Wang Zhongyong ;

Zhang Haibin .

CHINA COMMUNICATIONS, 2011, 8 (03) :66-72

[38] Undecidable Cases of Model Checking Probabilistic Temporal-Epistemic Logic [J].

Van Der Meyden, Ron ;

Patra, Manas K. .

ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2020, 21 (04)

[39] Complexity analysis of a unifying algorithm for model checking interval temporal logic [J].

Bozzelli, Laura ;

Montanari, Angelo ;

Peron, Adriano .

INFORMATION AND COMPUTATION, 2021, 280

[40] Generalized Possibilistic CTL* Model Checking with Fuzzy Temporal Logic Operators [J].

Mu, Chuanjiang ;

Liu, Wuniu ;

Li, Yongming .

THEORETICAL COMPUTER SCIENCE, NCTCS 2024, 2025, 2354 :81-94

← 1 2 3 4 5 →