  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 \cdot k^{2.38} \cdot 2^k)$ and $O(m \cdot \log n \cdot k)$,
respectively, where $n$ is the number of states and $m$ is the number of edges,
significantly improving the previous known $O(n\cdot k \cdot \sqrt{n\cdot 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.

Data Structures and Algorithms;Logic in Computer Science