Reduction Techniques for Model Checking Markov Decision Processes

Research output: Contribution to book/Conference proceedings/Anthology/ReportConference contributionContributedpeer-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 languageEnglish
Title of host publicationQEST'08: Proceedings of the 2008 Fifth International Conference on Quantitative Evaluation of Systems
PublisherIEEE Computer Society, Washington
Pages45-54
Number of pages10
ISBN (print)978-0-7695-3360-5
Publication statusPublished - 14 Sept 2008
Peer-reviewedYes

Conference

Title5th International Conference on the Quantitative Evaluation of SysTems
Abbreviated titleQEST'08
Conference number
Duration14 - 17 September 2008
Website
Degree of recognitionInternational event
Location
CitySt Malo
CountryFrance

External IDs

Scopus 56649116055
ORCID /0000-0002-5321-9343/work/205988094

Keywords