Symbolic Model Checking of Probabilistic Processes Using MTBDDs and the Kronecker Representation