Automatic Verification of Real-time Systems with Discrete Probability Distributions