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 条

[1] Truly on-the-fly LTL model checking
Hammer, M
Knapp, A
Merz, S
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2005, 3440 : 191 - 205
[2] On-the-fly parallel model checking algorithm that is optimal for verification of weak LTL properties
Barnat, Jiri
Brim, Lubos
Rockai, Petr
SCIENCE OF COMPUTER PROGRAMMING, 2012, 77 (12) : 1272 - 1288
[3] A Time-Optimal On-the-Fly Parallel Algorithm for Model Checking of Weak LTL Properties
Barnat, Jiri
Brim, Lubos
Rockai, Petr
FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS, 2009, 5885 : 407 - 425
[4] Bounded Rational Search for On-the-Fly Model Checking of LTL Properties
Behjati, Razieh
Sirjani, Marjan
Ahmadabadi, Majid Nili
FUNDAMENTALS OF SOFTWARE ENGINEERING, 2010, 5961 : 292 - 307
[5] On-the-fly Probabilistic Model Checking
Latella, Diego
Loreti, Michele
Massink, Mieke
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2014, (166): : 45 - 59
[6] Self-Loop Aggregation Product - A New Hybrid Approach to On-the-Fly LTL Model Checking
Duret-Lutz, Alexandre
Klai, Kais
Poitrenaud, Denis
Thierry-Mieg, Yann
AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, 2011, 6996 : 336 - +
[7] On-the-Fly Model Checking with Neural MCTS
Xu, Ruiyang
Lieberherr, Karl
NASA FORMAL METHODS (NFM 2022), 2022, 13260 : 557 - 575
[8] Next heuristic for on-the-fly model checking
Alur, R
Wang, BY
CONCUR '99: CONCURRENCY THEORY, 1999, 1664 : 98 - 113
[9] On-the-fly model checking of RCTL formulas
Beer, I
Ben-David, S
Landver, A
COMPUTER AIDED VERIFICATION, 1998, 1427 : 184 - 194
[10] Scalable distributed on-the-fly symbolic model checking
Ben-David, S
Heyman, T
Grumberg, O
Schuster, A
FORMAL METHODS IN COMPUTER-AIDED DESIGN, PROCEEDINGS, 2000, 1954 : 390 - 404

← 1 2 3 4 5 →