|
Title
|
|
|
|
Graph-based reductions for parametric and weighted MDPs
|
|
|
Author
|
|
|
|
|
|
|
Abstract
|
|
|
|
| We study the complexity of reductions for weighted reachability in parametric Markov decision processes. That is, we say a state p is never worse than q if for all valuations of the polynomial indeterminates it is the case that the maximal expected weight that can be reached from p is greater than the same value from q. In terms of computational complexity, we establish that determining whether p is never worse than q is -complete. On the positive side, we give a polynomial-time algorithm to compute the equivalence classes of the order we study for Markov chains. Additionally, we describe and implement two inference rules to under-approximate the never-worse relation and empirically show that it can be used as an efficient preprocessing step for the analysis of large Markov decision processes. |
|
|
|
Language
|
|
|
|
English
|
|
|
Source (journal)
|
|
|
|
Lecture notes in computer science. - Berlin, 1973, currens
|
|
|
Source (book)
|
|
|
|
Automated Technology for Verification and Analysis : 21st International Symposium, ATVA 2023, Singapore, October 24–27, 2023
|
|
|
Source (series)
|
|
|
|
Lecture notes in computer science ; 14215
|
|
|
Publication
|
|
|
|
Berlin
:
Springer
,
2023
|
|
|
ISBN
|
|
|
|
978-3-031-45328-1
|
|
|
DOI
|
|
|
|
10.1007/978-3-031-45329-8_7
|
|
|
Volume/pages
|
|
|
|
p. 137-157
|
|
|
Full text (Publisher's DOI)
|
|
|
|
|
|