In this thesis we present a compositional technique, called the quotient technique, for verification of probabilistic transition systems. The quotient technique is a promising method for avoiding the state explosion problem, arising from the many possible combinations of component states. The technique works by gradually removing components from the system, while transforming the specification accordingly. We present the theory of probabilistic alternating transition systems, system which can have both non-deterministic and probabilistic behavior, and allow these systems to have both synchronous and asynchronous behavior. We furthermore present a probabilistic modal logic, \logic, for which we define the quotient technique. This leads to an extension of the logic, a so called general modality, which we explore in detail in order apply simplification heuristics to the formulas. The correctness of the quotient technique is justified in a formal proof, and the very important aspect of simplification of quotiented formulas is studied. We implement the technique in Moscow ML, and explain included elements of the implementation in the report. Finally we run tests on the implementation, to evaluate the effectiveness of the quotient technique.