Reduction Techniques for Model Checking Markov Decision Processes

Publikation: Beitrag in Buch/Konferenzbericht/Sammelband/GutachtenBeitrag in KonferenzbandBeigetragenBegutachtung

Beitragende

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

OriginalspracheEnglisch
TitelQEST'08: Proceedings of the 2008 Fifth International Conference on Quantitative Evaluation of Systems
Herausgeber (Verlag)IEEE Computer Society, Washington
Seiten45-54
Seitenumfang10
ISBN (Print)978-0-7695-3360-5
PublikationsstatusVeröffentlicht - 14 Sept. 2008
Peer-Review-StatusJa

Konferenz

Titel5th International Conference on the Quantitative Evaluation of SysTems
KurztitelQEST'08
Veranstaltungsnummer
Dauer14 - 17 September 2008
Webseite
BekanntheitsgradInternationale Veranstaltung
Ort
StadtSt Malo
LandFrankreich

Externe IDs

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

Schlagworte