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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

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

  • Jan Heemstra,
  • Muhammad Osama,
  • Anton Wijs

摘要

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.