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