GPUexploresc prob: Markov Chain State Space Construction and Verification with GPUs

Abstract

Abstract GPUexplore $$^{\textsc {prob}}$$ P R O B is an extension of GPUexplore that constructs state spaces of Markov Chains and performs probabilistic model checking entirely on a GPU. It can construct the state space of a Discrete-Time Markov Chain and verify that it satisfies a given Probabilistic Computation-Tree Logic formula. We present the tool, and experimentally compare with Storm, demonstrating its effectiveness.