---
_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: 2025-06-02T08:53:43Z
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'
...