Reduction Techniques for Model Checking Markov Decision Processes
Research output: Contribution to book/Conference proceedings/Anthology/Report › Conference contribution › Contributed › peer-review
Contributors
Abstract
The quantitative analysis of a randomized system, modeled by a Markov decision process, against an LTL formula can be performed by a combination of graph algorithms, automata-theoretic concepts and numerical methods to compute maximal or minimal reachability probabilities. In this paper, we present various reduction techniques that serve to improve the performance of the quantitative analysis, and report on their implementation on the top of the probabilistic model checker \LiQuor. Although our techniques are purely heuristic and cannot improve the worst-case time complexity of standard algorithms for the quantitative analysis, a series of examples illustrates that the proposed methods can yield a major speed-up.
Details
| Original language | English |
|---|---|
| Title of host publication | QEST'08: Proceedings of the 2008 Fifth International Conference on Quantitative Evaluation of Systems |
| Publisher | IEEE Computer Society, Washington |
| Pages | 45-54 |
| Number of pages | 10 |
| ISBN (print) | 978-0-7695-3360-5 |
| Publication status | Published - 14 Sept 2008 |
| Peer-reviewed | Yes |
Conference
| Title | 5th International Conference on the Quantitative Evaluation of SysTems |
|---|---|
| Abbreviated title | QEST'08 |
| Conference number | |
| Duration | 14 - 17 September 2008 |
| Website | |
| Degree of recognition | International event |
| Location | |
| City | St Malo |
| Country | France |
External IDs
| Scopus | 56649116055 |
|---|---|
| ORCID | /0000-0002-5321-9343/work/205988094 |