Partial Order Reduction for Markov Decision Processes: A Survey

Marcus GrößerMarcus Größer, Christel BaierChristel Baier

DOI Link

Marcus Größer, Christel Baier
Partial Order Reduction for Markov Decision Processes: A Survey
Proc. of the 4th International Symposium on Formal Methods for Component and Objects (FMCO), volume 4111 of Lecture Notes in Computer Science, 408--427, 2005. Springer

Details
Bibtex

KurzfassungAbstract
In the past, several model checking algorithms have been proposed to verify probabilistic reactive systems. In contrast to the non-probabilistic setting where various techniques have been suggested and successfully applied to combat the state space-explosion problem in the context of model checking the techniques used for probabilistic systems have mainly concentrated on symbolic methods with variants of decision diagrams or abstraction methods. Only recently results have been published that give criteria on applying partial order reduction for verifying quantitative linear time properties as well as branching time properties for probabilistic systems. This paper summarizes the results that have been established so far about partial order reduction for Markov decision processes. We present the different reduction conditions and provide a comparison of the corresponding results.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

The final publication is available at Springer via http://dx.doi.org/10.1007/11804192_19.

@inproceedings{GB2005,
  author    = {Marcus Gr{\"{o}}{\ss}er and Christel Baier},
  title     = {Partial Order Reduction for Markov Decision Processes: A Survey},
  booktitle = {Proc. of the 4th International Symposium on Formal Methods for
               Component and Objects (FMCO)},
  series    = {Lecture Notes in Computer Science},
  volume    = {4111},
  publisher = {Springer},
  year      = {2005},
  pages     = {408--427},
  doi       = {10.1007/11804192_19}
}