In this thesis, we address the issue of reduction techniques for probabilistic model checking to increase the efficiency of the qualitative/quantitative analysis of probabilistic systemsrnagainst temporal logics. We extend the concept of Partial Order Reduction to Markov decision processes both in the case of linear time as well as branching time probabilistic model checking.rnWe also introduce and study a new class of omega-automata, namely probabilistic omega-automata. We especially focus on probabilistic Büchi automata and show a variety of interesting results.