@inproceedings{9289df364dd94e64b263083dea744ccf,
title = "No Need to Be Stubborn: Partial-Order Reduction for GPU Model Checking Revisited",
abstract = "GPUexplore, a GPU-accelerated explicit-state LTL model checker, achieves significant speedups compared to sequential and multi-core CPU model checkers, but it is limited by the amount of memory available on GPUs. Partial-Order Reduction is a way to remedy this problem, by excluding unnecessary transitions and states from exploration. For this work, we implemented the ample and clustered-ample reduction techniques in GPUexplore. Experiments show that our implementations achieve reductions similar to the state-of-the-art Breadth-First Search configurations of multi-core LTSmin and sequential DiVinE and Spin without introducing significant computational overhead, even though LTSmin applies stubborn set reduction, which has often been reported as the most effective technique. At times, ample and cample reduction even speeds up exploration 4–100×.",
keywords = "Explicit state space exploration, Finite-state machines, GPU computing, LTL model checking, partial-order reduction",
author = "{van Spreuwel}, Rik and Anton Wijs",
year = "2024",
month = oct,
day = "30",
doi = "10.1007/978-3-031-75380-0_20",
language = "English",
isbn = "978-3-031-75379-4",
series = "Lecture Notes in Computer Science (LNCS)",
publisher = "Springer",
pages = "353--373",
editor = "Tiziana Margaria and Bernhard Steffen",
booktitle = "Leveraging Applications of Formal Methods, Verification and Validation. Specification and Verification",
address = "Germany",
note = "12th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2024, ISoLA 2024 ; Conference date: 27-10-2024 Through 31-10-2024",
}