Faster Algorithms for Quantitative Analysis of MCs and MDPs with Small Treewidth

TY - GEN

T1 - Faster Algorithms for Quantitative Analysis of MCs and MDPs with Small Treewidth

AU - Asadi, Ali

AU - Chatterjee, Krishnendu

AU - Goharshady, Amir Kafshdar

AU - Mohammadi, Kiarash

AU - Pavlogiannis, Andreas

N1 - Conference code: 18

PY - 2020

Y1 - 2020

N2 - Discrete-time Markov Chains (MCs) and Markov Decision Processes (MDPs) are two standard formalisms in system analysis. Their main associated quantitative objectives are hitting probabilities, discounted sum, and mean payoff. Although there are many techniques for computing these objectives in general MCs/MDPs, they have not been thoroughly studied in terms of parameterized algorithms, particularly when treewidth is used as the parameter. This is in sharp contrast to qualitative objectives for MCs, MDPs and graph games, for which treewidth-based algorithms yield significant complexity improvements. In this work, we show that treewidth can also be used to obtain faster algorithms for the quantitative problems. For an MC with n states and m transitions, we show that each of the classical quantitative objectives can be computed in time, given a tree decomposition of the MC with width t. Our results also imply a bound of for each objective on MDPs, where is the number of strategy-iteration refinements required for the given input and objective. Finally, we make an experimental evaluation of our new algorithms on low-treewidth MCs and MDPs obtained from the DaCapo benchmark suite. Our experiments show that on low-treewidth MCs and MDPs, our algorithms outperform existing well-established methods by one or more orders of magnitude.

AB - Discrete-time Markov Chains (MCs) and Markov Decision Processes (MDPs) are two standard formalisms in system analysis. Their main associated quantitative objectives are hitting probabilities, discounted sum, and mean payoff. Although there are many techniques for computing these objectives in general MCs/MDPs, they have not been thoroughly studied in terms of parameterized algorithms, particularly when treewidth is used as the parameter. This is in sharp contrast to qualitative objectives for MCs, MDPs and graph games, for which treewidth-based algorithms yield significant complexity improvements. In this work, we show that treewidth can also be used to obtain faster algorithms for the quantitative problems. For an MC with n states and m transitions, we show that each of the classical quantitative objectives can be computed in time, given a tree decomposition of the MC with width t. Our results also imply a bound of for each objective on MDPs, where is the number of strategy-iteration refinements required for the given input and objective. Finally, we make an experimental evaluation of our new algorithms on low-treewidth MCs and MDPs obtained from the DaCapo benchmark suite. Our experiments show that on low-treewidth MCs and MDPs, our algorithms outperform existing well-established methods by one or more orders of magnitude.

KW - Markov Chains

KW - Markov Decision Processes

KW - Treewidth

U2 - 10.1007/978-3-030-59152-6_14

DO - 10.1007/978-3-030-59152-6_14

M3 - Article in proceedings

SN - 978-3-030-59151-9

T3 - Lecture Notes in Computer Science

SP - 253

EP - 270

BT - Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Proceedings

A2 - Van Hung, Dang

A2 - Sokolsky, Oleg

PB - Springer

CY - Cham

T2 - International Symposium on Automated Technology for Verification and Analysis

Y2 - 19 October 2020 through 23 October 2020

ER -