@inproceedings{1f46160bbc4b4741b52c094c1fd0a897,
title = "Hitching a Ride to a Lasso: Massively Parallel On-The-Fly LTL Model Checking",
abstract = "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 LTL-checking algorithm is up to 150× 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.",
keywords = "automata-based verification, finite-state machines, GPU, LTL model checking, Temporal logic",
author = "Muhammad Osama and Anton Wijs",
year = "2024",
month = apr,
day = "5",
doi = "10.1007/978-3-031-57249-4_2",
language = "English",
isbn = "978-3-031-57248-7",
series = "Lecture Notes in Computer Science (LNCS)",
publisher = "Springer",
pages = "23--43",
editor = "Bernd Finkbeiner and Laura Kov{\'a}cs",
booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",
address = "Germany",
note = "30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2024, which was held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024 ; Conference date: 06-04-2024 Through 11-04-2024",
}