IntervalMDP.jl: Accelerated Value Iteration for Interval Markov Decision Processes

TL;DR

IntervalMDP.jl addresses efficient analysis of interval Markov Decision Processes by enabling robust value iteration on IMDPs through CPU multi-threading and CUDA GPU acceleration. The framework interoperates with established formats (PRISM, bmdp-tool) and uses NetCDF/JSON storage, while employing bitonic sort and O-maximization to accelerate per-state linear programs. Empirical results show substantial performance gains: CPU speedups of $2$-$4$ times on average and GPU speedups of orders of magnitude for large models, with lower memory consumption than competing tools. The platform enables scalable verification and policy synthesis for IMDPs and lays groundwork for extensions to temporal logics.

Abstract

In this paper, we present IntervalMDP.jl, a Julia package for probabilistic analysis of interval Markov Decision Processes (IMDPs). IntervalMDP.jl facilitates the synthesis of optimal strategies and verification of IMDPs against reachability specifications and discounted reward properties. The library supports sparse matrices and is compatible with data formats from common tools for the analysis of probabilistic models, such as PRISM. A key feature of IntervalMDP.jl is that it presents both a multi-threaded CPU and a GPU-accelerated implementation of value iteration algorithms for IMDPs. In particular, IntervalMDP.jl takes advantage of the Julia type system and the inherently parallelizable nature of value iteration to improve the efficiency of performing analysis of IMDPs. On a set of examples, we show that IntervalMDP.jl substantially outperforms existing tools for verification and strategy synthesis for IMDPs in both computation time and memory consumption.

Figures (4)

• Figure 1: An example of a 3-state where state $q_3$ is a sink state.
• Figure 2: Bitonic sorting network structure in $\log_2(n)$ major rounds, each of which is up to $\log_2(n)$ minor rounds. Each arrow represents a comparison and points towards the larger element. After each major round, subsets of increasing size are bitonic (increasing order, then decreasing of the same size).
• Figure 3: Cumulative sum as a tree-reduction. This tree reduction has a latency of $O(\log_2(n))$ as opposed to $O(n)$ of a traditional iterative algorithm.
• Figure 4: Computation time of IntervalMDP.jl compared against bmdp-tool and PRISM on 35 of varying sizes.