|
CPU and GPU MDP decomposition into Strongly Connected Components and Maximal End ComponentsThe provided decomposition tools can be used to decompose the graphs underlying Markov Decision Processes (MDPs) into Strongly Connected Components (SCCs) and Maximal End Components (MECs). The GPU tools work completely on an NVIDIA GPU with at least CUDA computation capability 2.0. CPU component decomposition is based on Tarjan's SCC decomposition algorithm, while GPU component decomposition is based on Forward-Backward BFS with trimming.Download links for both the tools and a set of models for experimentation are provided on this page. Due to the sizes of the graphs underlying the models, we cannot provide the graphs directly. Using the model checker PRISM, though, one can export the required graphs after loading the models (in the menu, choose Model->Export->Transition matrix->Plain text file). REQUIRED PACKAGES: CUDA driver + SDK. For the CPU tools: a C compiler.
|