Partial Order Reduction for Markov Decision Processes: A Survey.

Autor: Boer, Frank S., Bonsangue, Marcello M., Graf, Susanne, Roever, Willem-Paul, Groesser, Marcus, Baier, Christel
Zdroj: Formal Methods for Components & Objects (9783540367499); 2006, p408-427, 20p
Abstrakt: 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. [ABSTRACT FROM AUTHOR]
Databáze: Complementary Index