Faster Algorithms for Markov Decision Processes with Low Treewidth

We consider two core algorithmic problems for probabilistic verification: the maximal end-component decomposition and the almost-sure reachability set computation for Markov decision processes (MDPs). For MDPs with treewidth k, we present two improved static algorithms for both the problems that run in time O(n · k2.38 · 2k) and O(m · log n · k), respectively, where n is the number of states and m is the number of edges, significantly improving the previous known O(n· k · √n· k) bound for low treewidth. We also present decremental algorithms for both problems for MDPs with constant treewidth that run in amortized logarithmic time, which is a huge improvement over the previously known algorithms that require amortized linear time.