Hitching a Ride to a Lasso: Massively Parallel On-The-Fly LTL Model Checking.
International Conference on Tools and Algorithms for Construction and Analysis of Systems(2024)
摘要
AbstractThe 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$$\times $$ × 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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要