Towards End-to-End GPU Acceleration of PCTL Model Checking
摘要
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.