Towards End-to-End GPU Acceleration of PCTL Model Checking

Jan Heemstra; Muhammad Osama; Anton Wijs

doi:10.1007/978-3-031-75775-4_14

Towards End-to-End GPU Acceleration of PCTL Model Checking

Jan Heemstra
, Muhammad Osama
, Anton Wijs (Corresponding author)

Research output: Chapter in Book/Report/Conference proceeding › Chapter › Academic › peer-review

1 Citation (Scopus)

2 Downloads (Pure)

Abstract

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.

Original language	English
Title of host publication	Principles of Verification: Cycling the Probabilistic Landscape
Subtitle of host publication	Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday
Editors	Nils Jansen, Sebastian Junges, Benjamin Lucien Kaminski, Chrisoph Matheja, Thomas Noll, Tim Quatmann, Mariëlle Stoelinga, Matthias Volk
Publisher	Springer
Chapter	14
Pages	314-337
Number of pages	24
Volume	2
ISBN (Electronic)	978-3-031-75775-4
ISBN (Print)	978-3-031-75774-7
DOIs	https://doi.org/10.1007/978-3-031-75775-4_14
Publication status	Published - 2025

Publication series

Name	Lecture Notes in Computer Science
Volume	15261 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Bibliographical note

Publisher Copyright:
© The Author(s), under exclusive license to Springer Nature Switzerland AG 2025.

Keywords

Discrete-Time Markov Chains
GPU
PCTL model checking
probabilistic model checking
Temporal logic

Access to Document

10.1007/978-3-031-75775-4_14

Cite this

Heemstra, J., Osama, M., & Wijs, A. (2025). Towards End-to-End GPU Acceleration of PCTL Model Checking. In N. Jansen, S. Junges, B. L. Kaminski, C. Matheja, T. Noll, T. Quatmann, M. Stoelinga, & M. Volk (Eds.), Principles of Verification: Cycling the Probabilistic Landscape: Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday (Vol. 2, pp. 314-337). (Lecture Notes in Computer Science; Vol. 15261 LNCS). Springer. https://doi.org/10.1007/978-3-031-75775-4_14

Heemstra, Jan ; Osama, Muhammad ; Wijs, Anton. / Towards End-to-End GPU Acceleration of PCTL Model Checking. Principles of Verification: Cycling the Probabilistic Landscape: Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday. editor / Nils Jansen ; Sebastian Junges ; Benjamin Lucien Kaminski ; Chrisoph Matheja ; Thomas Noll ; Tim Quatmann ; Mariëlle Stoelinga ; Matthias Volk. Vol. 2 Springer, 2025. pp. 314-337 (Lecture Notes in Computer Science).

@inbook{85bf9ef91f2548f5ab31af6cb5ac9a07,

title = "Towards End-to-End GPU Acceleration of PCTL Model Checking",

abstract = "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.",

keywords = "Discrete-Time Markov Chains, GPU, PCTL model checking, probabilistic model checking, Temporal logic",

author = "Jan Heemstra and Muhammad Osama and Anton Wijs",

note = "Publisher Copyright: {\textcopyright} The Author(s), under exclusive license to Springer Nature Switzerland AG 2025.",

year = "2025",

doi = "10.1007/978-3-031-75775-4\_14",

language = "English",

isbn = "978-3-031-75774-7",

volume = "2",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "314--337",

editor = "Nils Jansen and Sebastian Junges and Kaminski, \{Benjamin Lucien\} and Chrisoph Matheja and Thomas Noll and Tim Quatmann and Mari{\"e}lle Stoelinga and Matthias Volk",

booktitle = "Principles of Verification: Cycling the Probabilistic Landscape",

address = "Germany",

}

Heemstra, J, Osama, M & Wijs, A 2025, Towards End-to-End GPU Acceleration of PCTL Model Checking. in N Jansen, S Junges, BL Kaminski, C Matheja, T Noll, T Quatmann, M Stoelinga & M Volk (eds), Principles of Verification: Cycling the Probabilistic Landscape: Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday. vol. 2, Lecture Notes in Computer Science, vol. 15261 LNCS, Springer, pp. 314-337. https://doi.org/10.1007/978-3-031-75775-4_14

Towards End-to-End GPU Acceleration of PCTL Model Checking. / Heemstra, Jan; Osama, Muhammad; Wijs, Anton (Corresponding author).
Principles of Verification: Cycling the Probabilistic Landscape: Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday. ed. / Nils Jansen; Sebastian Junges; Benjamin Lucien Kaminski; Chrisoph Matheja; Thomas Noll; Tim Quatmann; Mariëlle Stoelinga; Matthias Volk. Vol. 2 Springer, 2025. p. 314-337 (Lecture Notes in Computer Science; Vol. 15261 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Chapter › Academic › peer-review

TY - CHAP

T1 - Towards End-to-End GPU Acceleration of PCTL Model Checking

AU - Heemstra, Jan

AU - Osama, Muhammad

AU - Wijs, Anton

N1 - Publisher Copyright: © The Author(s), under exclusive license to Springer Nature Switzerland AG 2025.

PY - 2025

Y1 - 2025

N2 - 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.

AB - 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.

KW - Discrete-Time Markov Chains

KW - GPU

KW - PCTL model checking

KW - probabilistic model checking

KW - Temporal logic

UR - https://www.scopus.com/pages/publications/85211098156

U2 - 10.1007/978-3-031-75775-4_14

DO - 10.1007/978-3-031-75775-4_14

M3 - Chapter

AN - SCOPUS:85211098156

SN - 978-3-031-75774-7

VL - 2

T3 - Lecture Notes in Computer Science

SP - 314

EP - 337

BT - Principles of Verification: Cycling the Probabilistic Landscape

A2 - Jansen, Nils

A2 - Junges, Sebastian

A2 - Kaminski, Benjamin Lucien

A2 - Matheja, Chrisoph

A2 - Noll, Thomas

A2 - Quatmann, Tim

A2 - Stoelinga, Mariëlle

A2 - Volk, Matthias

PB - Springer

ER -

Heemstra J, Osama M, Wijs A. Towards End-to-End GPU Acceleration of PCTL Model Checking. In Jansen N, Junges S, Kaminski BL, Matheja C, Noll T, Quatmann T, Stoelinga M, Volk M, editors, Principles of Verification: Cycling the Probabilistic Landscape: Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday. Vol. 2. Springer. 2025. p. 314-337. (Lecture Notes in Computer Science). doi: 10.1007/978-3-031-75775-4_14