Hitching a Ride to a Lasso: Massively Parallel On-The-Fly LTL Model Checking

被引：1

作者：

Osama, Muhammad ^{[1
,2
]}

Wijs, Anton ^{[2
]}

机构：

[1] Leiden Univ, Leiden Inst Adv Comp Sci LIACS, Leiden, Netherlands

[2] Eindhoven Univ Technol, Eindhoven, Netherlands

来源：

TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PT II, TACAS 2024 | 2024年 / 14571卷

关键词：

Temporal logic; LTL model checking; automata-based verification; finite-state machines; GPU; PARTIAL-ORDER REDUCTION; ALGORITHMS; GENERATION;

D O I：

10.1007/978-3-031-57249-4_2

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

The need for massively parallel algorithms, suitable to exploit the computational power of hardware such as graphics processing units, is ever increasing. In this paper, we propose a new algorithm for the on-the-fly verification of Linear-Time Temporal Logic (LTL) formulae [45] that is aimed at running on such devices. We prove its correctness and termination guarantee, and experimentally compare a GPU implementation with state-of-the-art LTL model checkers. Our new GPU LTLchecking algorithm is up to 150x faster on proving the correctness of a system than LTSmin running on a 32-core high-end CPU, and is more economic in using the available memory.

引用

页码：23 / 43

页数：21

共 50 条

[21] On-the-fly TCTL model checking for time Petri nets
Hadjidj, Rachid
Boucheneb, Hanifa
THEORETICAL COMPUTER SCIENCE, 2009, 410 (42) : 4241 - 4261
[22] On-the-fly model checking under fairness that exploits symmetry
Gyuris, V
Sistla, AP
COMPUTER AIDED VERIFICATION, 1997, 1254 : 232 - 243
[23] Combining partial order reductions with on-the-fly model-checking
Peled, D
FORMAL METHODS IN SYSTEM DESIGN, 1996, 8 (01) : 39 - 64
[24] On-the-fly techniques for game-based software model checking
Bakewell, Adam
Ghica, Dan R.
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, 2008, 4963 : 78 - 92
[25] On-the-fly model checking of fair non-repudiation Protocols
Li, Guoqiang
Ogawa, Mizuhito
AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, PROCEEDINGS, 2007, 4762 : 511 - +
[26] On-the-fly symbolic model checking for real-time systems
Bouajjani, A
Tripakis, S
Yovine, S
18TH IEEE REAL-TIME SYSTEMS SYMPOSIUM, PROCEEDINGS, 1997, : 25 - 34
[27] Fast on-the-fly parametric real-time model checking
Zhang, DZ
Cleaveland, R
RTSS 2005: 26TH IEEE INTERNATIONAL REAL-TIME SYSTEMS SYMPOSIUM, PROCEEDINGS, 2005, : 157 - 166
[28] From Distributed Memory Cycle Detection to Parallel LTL Model Checking
Barnat, J.
Brim, L.
Chaloupka, J.
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2005, 133 : 21 - 39
[29] Parallel Nested Depth-First Searches for LTL Model Checking
Evangelista, Sami
Petrucci, Laure
Youcef, Samir
AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, 2011, 6996 : 381 - 396
[30] Parallel breadth-first search LTL model-checking
Barnat, J
Brim, L
Chaloupka, J
18TH IEEE INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING, PROCEEDINGS, 2003, : 106 - 115

← 1 2 3 4 5 →