--- _id: '8728' abstract: - lang: eng text: 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 O((n+m)⋅t2) time, given a tree decomposition of the MC with width t. Our results also imply a bound of O(κ⋅(n+m)⋅t2) 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. alternative_title: - LNCS article_processing_charge: No author: - first_name: Ali full_name: Asadi, Ali last_name: Asadi - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Amir Kafshdar full_name: Goharshady, Amir Kafshdar id: 391365CE-F248-11E8-B48F-1D18A9856A87 last_name: Goharshady orcid: 0000-0003-1702-6584 - first_name: Kiarash full_name: Mohammadi, Kiarash last_name: Mohammadi - first_name: Andreas full_name: Pavlogiannis, Andreas id: 49704004-F248-11E8-B48F-1D18A9856A87 last_name: Pavlogiannis orcid: 0000-0002-8943-0722 citation: ama: 'Asadi A, Chatterjee K, Goharshady AK, Mohammadi K, Pavlogiannis A. Faster algorithms for quantitative analysis of MCs and MDPs with small treewidth. In: Automated Technology for Verification and Analysis. Vol 12302. Springer Nature; 2020:253-270. doi:10.1007/978-3-030-59152-6_14' apa: 'Asadi, A., Chatterjee, K., Goharshady, A. K., Mohammadi, K., & Pavlogiannis, A. (2020). Faster algorithms for quantitative analysis of MCs and MDPs with small treewidth. In Automated Technology for Verification and Analysis (Vol. 12302, pp. 253–270). Hanoi, Vietnam: Springer Nature. https://doi.org/10.1007/978-3-030-59152-6_14' chicago: Asadi, Ali, Krishnendu Chatterjee, Amir Kafshdar Goharshady, Kiarash Mohammadi, and Andreas Pavlogiannis. “Faster Algorithms for Quantitative Analysis of MCs and MDPs with Small Treewidth.” In Automated Technology for Verification and Analysis, 12302:253–70. Springer Nature, 2020. https://doi.org/10.1007/978-3-030-59152-6_14. ieee: A. Asadi, K. Chatterjee, A. K. Goharshady, K. Mohammadi, and A. Pavlogiannis, “Faster algorithms for quantitative analysis of MCs and MDPs with small treewidth,” in Automated Technology for Verification and Analysis, Hanoi, Vietnam, 2020, vol. 12302, pp. 253–270. ista: 'Asadi A, Chatterjee K, Goharshady AK, Mohammadi K, Pavlogiannis A. 2020. Faster algorithms for quantitative analysis of MCs and MDPs with small treewidth. Automated Technology for Verification and Analysis. ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 12302, 253–270.' mla: Asadi, Ali, et al. “Faster Algorithms for Quantitative Analysis of MCs and MDPs with Small Treewidth.” Automated Technology for Verification and Analysis, vol. 12302, Springer Nature, 2020, pp. 253–70, doi:10.1007/978-3-030-59152-6_14. short: A. Asadi, K. Chatterjee, A.K. Goharshady, K. Mohammadi, A. Pavlogiannis, in:, Automated Technology for Verification and Analysis, Springer Nature, 2020, pp. 253–270. conference: end_date: 2020-10-23 location: Hanoi, Vietnam name: 'ATVA: Automated Technology for Verification and Analysis' start_date: 2020-10-19 date_created: 2020-11-06T07:30:05Z date_published: 2020-10-12T00:00:00Z date_updated: 2024-03-28T23:30:34Z day: '12' ddc: - '000' department: - _id: KrCh doi: 10.1007/978-3-030-59152-6_14 external_id: isi: - '000723555700014' file: - access_level: open_access checksum: ae83f27e5b189d5abc2e7514f1b7e1b5 content_type: application/pdf creator: dernst date_created: 2020-11-06T07:41:03Z date_updated: 2020-11-06T07:41:03Z file_id: '8729' file_name: 2020_LNCS_ATVA_Asadi_accepted.pdf file_size: 726648 relation: main_file success: 1 file_date_updated: 2020-11-06T07:41:03Z has_accepted_license: '1' intvolume: ' 12302' isi: 1 language: - iso: eng month: '10' oa: 1 oa_version: Submitted Version page: 253-270 project: - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 25892FC0-B435-11E9-9278-68D0E5697425 grant_number: ICT15-003 name: Efficient Algorithms for Computer Aided Verification - _id: 267066CE-B435-11E9-9278-68D0E5697425 name: Quantitative Analysis of Probablistic Systems with a focus on Crypto-currencies publication: Automated Technology for Verification and Analysis publication_identifier: eisbn: - '9783030591526' eissn: - 1611-3349 isbn: - '9783030591519' issn: - 0302-9743 publication_status: published publisher: Springer Nature quality_controlled: '1' related_material: record: - id: '8934' relation: dissertation_contains status: public scopus_import: '1' status: public title: Faster algorithms for quantitative analysis of MCs and MDPs with small treewidth type: conference user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1 volume: 12302 year: '2020' ...