Reduction Techniques for Model Checking Markov Decision Processes

Frank CiesinskiFrank Ciesinski, Christel BaierChristel Baier, Marcus GrößerMarcus Größer, Joachim KleinJoachim Klein

DOI Link

Frank Ciesinski, Christel Baier, Marcus Größer, Joachim Klein
Reduction Techniques for Model Checking Markov Decision Processes
Proc. of the 5th International Conference on Quantitative Evaluation of Systems (QEST), 45--54, 2008. IEEE Computer Society Press

Details
Bibtex

KurzfassungAbstract
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.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

@inproceedings{CBGK2008,
  author    = {Frank Ciesinski and Christel Baier and Marcus Gr{\"{o}}{\ss}er
               and Joachim Klein},
  title     = {Reduction Techniques for Model Checking Markov Decision Processes},
  booktitle = {Proc. of the 5th International Conference on Quantitative
               Evaluation of Systems (QEST)},
  publisher = {IEEE Computer Society Press},
  year      = {2008},
  pages     = {45--54},
  doi       = {10.1109/QEST.2008.45}
}