2020/04/19 by Ali Al Asadi, Asadi, Ali, Krishnendu Chatterjee +8
Computer Science · #Advanced Software Engineering Methodologies #Formal Methods in Verification #Bayesian Modeling and Causal Inference
paper · pdf · doi:10.48550/arxiv.2004.08828
Discrete-time Markov Chains (MCs) and Markov Decision Processes (MDPs) are\ntwo standard formalisms in system analysis. Their main associated quantitative\nobjectives are hitting probabilities, discounted sum, and mean payoff. Although\nthere are many techniques for computing these objectives in general MCs/MDPs,\nthey have not been thoroughly studied in terms of parameterized algorithms,\nparticularly when treewidth is used as the parameter. This is in sharp contrast\nto qualitative objectives for MCs, MDPs and graph games, for which\ntreewidth-based algorithms yield significant complexity improvements.\n In this work, we show that treewidth can also be used to obtain faster\nalgorithms for the quantitative problems. For an MC with n states and m\ntransitions, we show that each of the classical quantitative objectives can be\ncomputed in O((n+m)\⋅ t2) time, given a tree decomposition of the MC that\nhas width t. Our results also imply a bound of O(\κ\⋅ (n+m)\⋅\nt2) for each objective on MDPs, where \κ is the number of\nstrategy-iteration refinements required for the given input and objective.\nFinally, we make an experimental evaluation of our new algorithms on\nlow-treewidth MCs and MDPs obtained from the DaCapo benchmark suite. Our\nexperimental results show that on MCs and MDPs with small treewidth, our\nalgorithms outperform existing well-established methods by one or more orders\nof magnitude.\n