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 条

[31] On-the-fly model checking for extended action-based probabilistic operators
Radu Mateescu
José Ignacio Requeno
International Journal on Software Tools for Technology Transfer, 2018, 20 : 563 - 587
[32] Markov regenerative processes solution and stochastic model checking: an on-the-fly approach
Donatelli, Susanna
PROCEEDINGS OF THE 12TH EAI INTERNATIONAL CONFERENCE ON PERFORMANCE EVALUATION METHODOLOGIES AND TOOLS (VALUETOOLS 2019), 2019, : 1 - 1
[33] On-the-fly model checking for extended action-based probabilistic operators
Mateescu, Radu
Ignacio Requeno, Jose
INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 2018, 20 (05) : 563 - 587
[34] Using On-The-Fly Model Checking to improve Constraint Programming for Dynamic Problems
Regin, Florian
De Maria, Elisabetta
2023 IEEE 35TH INTERNATIONAL CONFERENCE ON TOOLS WITH ARTIFICIAL INTELLIGENCE, ICTAI, 2023, : 393 - 398
[35] FBT: A tool for applying interval logic specifications to on-the-fly model checking
Hornos, MJ
JOURNAL OF UNIVERSAL COMPUTER SCIENCE, 2004, 10 (11) : 1498 - 1518
[36] On-the-fly Fluid Model Checking via Discrete Time Population Models
Latella, Diego
Loreti, Michele
Massink, Mieke
COMPUTER PERFORMANCE ENGINEERING, 2015, 9272 : 193 - 207
[37] LTL Model Checking of Parallel Programs with Under-Approximated TSO Memory Model
Barnat, Jiri
Brim, Lubos
Havel, Vojtech
2013 13TH INTERNATIONAL CONFERENCE ON APPLICATION OF CONCURRENCY TO SYSTEM DESIGN (ACSD 2013), 2013, : 51 - 59
[38] Hybrid Parallel Model Checking of Hybrid LTL on Hybrid State Space Representation
Klai, Kais
Abid, Chiheb Ameur
Arias, Jaime
Evangelista, Sami
VERIFICATION AND EVALUATION OF COMPUTER AND COMMUNICATION SYSTEMS (VECOS 2021), 2022, 13187 : 27 - 42
[39] On-the-fly model checking for C programs with extended CADP in FMICS-jETI
del Mar Gallardo, Maria
Merino, Pedro
Sanan, David
Joubert, Christophe
12TH IEEE INTERNATIONAL CONFERENCE ON ENGINEERING COMPLEX COMPUTER SYSTEMS, PROCEEDINGS, 2007, : 321 - +
[40] Many-core on-the-fly model checking of safety properties using GPUs
Wijs, Anton
Bosnacki, Dragan
INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 2016, 18 (02) : 169 - 185

← 1 2 3 4 5 →