Partial order reduction for probabilistic systems

In the past, several model checking algorithms have been proposed to verify probabilistic reactive systems. The techniques to combat the state-explosion problem have mainly concentrated on symbolic methods with variants of decision diagrams or abstraction methods. In this paper, we show how partial order reduction with a variant of Peled's ample set method can be applied in the context of LTL model checking for probabilistic systems modelled by Markov decision processes.