Faster algorithms for Markov decision processes with low treewidth Conference Paper


Author(s): Chatterjee, Krishnendu; Ła̧cki, Jakub
Title: Faster algorithms for Markov decision processes with low treewidth
Title Series: LNCS
Affiliation IST Austria
Abstract: 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·k 2.38·2k ) and O(m·logn· 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.
Conference Title: CAV: Computer Aided Verification
Volume: 8044
Conference Dates: July 13-19, 2013
Conference Location: Saint Petersburg, Russia
Publisher: Springer  
Date Published: 2013-07-01
Start Page: 543
End Page: 558
URL:
DOI: 10.1007/978-3-642-39799-8_36
Notes: The authors would like to thank Monika Henzinger for several interesting discussions on related topics. The research was supported by FWF Grant No P23499-N23,FWF NFN Grant No S11407-N23(RiSE), ERC Startgrant (279307: Graph Games), and Microsoft faculty fellows award. Jakub Łącki is a recipient of the Google Europe Fellowship in Graph Algorithms, and this research is supported in part by this Google Fellowship.
Open access: yes (repository)