Samenvatting
So far, existing probabilistic model checkers have been programmed to run on a CPU. While earlier work has accelerated some procedures of model checking with GPUs, such as matrix-vector multiplication for probabilistic model checking, we are the first to construct an end-to-end GPU-accelerated probabilistic model checker, where every step of the model checking process, from constructing a Discrete-Time Markov Chain to the verification of a Probabilistic Computation Tree Logic (PCTL) formula, occurs on the GPU, and where all relevant data is located in GPU memory. In this paper, we discuss the challenges imposed by the GPU architecture and memory constraints and how we overcame them, present intermediate performance results for a supported fragment of PCTL, and discuss the challenges that remain to support full PCTL property checking.
Originele taal-2 | Engels |
---|---|
Titel | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
Uitgeverij | Springer |
Pagina's | 314-337 |
Aantal pagina's | 24 |
DOI's | |
Status | Gepubliceerd - 2025 |
Publicatie series
Naam | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|
Volume | 15261 LNCS |
ISSN van geprinte versie | 0302-9743 |
ISSN van elektronische versie | 1611-3349 |
Bibliografische nota
Publisher Copyright:© The Author(s), under exclusive license to Springer Nature Switzerland AG 2025.